Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

بناءً على الورقة المقدمة، إليك ملخص تقني مفصل للتحقق الرسمي من المتباينة الأيزوبريمترية (المساوية للمحيط) الكلاسيكية في الحالة ثنائية الأبعاد.

1. بيان المسألة

تتناول الورقة المتباينة الأيزبريمترية (Isoperimetric Inequality) في المستوى الإقليدي. تنص المبرهنة على أنه لأي منحنى مغلق بسيط $C$ محيطه $L$ ومساحته المحصورة $A$، فإن المتباينة $L^2 \geq 4\pi A$ تتحقق. ويتحقق التساوي إذا وفقط إذا كان المنحنى عبارة عن دائرة.

بينما تعد هذه النتيجة مبرهنة كلاسيكية ذات براهين معروفة، تركز الورقة على التحقق الرسمي (formal verification) لبرهان تحليلي محدد لـ أدولف هيرتز (Adolf Hurwitz, 1902) باستخدام مساعد الإثبات Lean 4 ومكتبته الرياضية Mathlib. والهدف هو إزالة "الفجوات" التي توجد غالبًا في البراهين الموجودة في الكتب الدراسية (مثل التبادل غير المبرر بين النهايات والتكاملات) من خلال تقديم اشتقاق منطقي خطوة بخطوة يتم التحقق منه آليًا.

2. المنهجية

يتبع التحقق الرسمي نهج هيرتز التحليلي، الذي يختزل المسألة الهندسية إلى متباينة تتضمن سلاسل فوريه. ينقسم العمل إلى مرحلتين متمايزتين:

المرحلة الأولى: الأسس التحليلية لفوريه

قبل معالجة المنحنى، قام المؤلفون بصياغة الأدوات اللازمة من التحليل التوافقي ضمن Mathlib:

• علاقات التعامد (Orthogonality Relations): صياغة تعامد الدوال المثلثية ($\sin(nx), \cos(nx)$) على الفترة $[-\pi, \pi]$.
• نظرية التقارب (Convergence Theory): إثبات التقارب المنتظم لمجموعات فوريه الجزئية باستخدام اختبار فاييرشتراس (Weierstrass M-test). كان هذا أمرًا حاسمًا لضمان الحفاظ على خصائص مثل الاستمرارية والقابلية للتكامل في النهاية.
• الاشتقاق حدًا بحد (Term-by-Term Differentiation): إثبات الشروط التي يمكن بموجبها اشتقاق سلسلة فوريه حدًا بحد، مما يتطلب قابلية المجموع لـ $n(|a_n| + |b_n|)$.
• مبرهنة بارسيفال (Parseval's Theorem): صياغة الهوية التي تربط معيار $L^2$ لدالة بمعيار $\ell^2$ لمعاملات فوريه الخاصة بها.
• متباينة ويرتينجر (Wirtinger's Inequality): اشتقاق هذه المتباينة (التي تربط معيار $L^2$ لدالة دورية ذات متوسط صفري بمعتقتها) مباشرة من مبرهنة بارسيفال.

المرحلة الثانية: البرهان الهندسي (حجة هيرتز)

قام المؤلفون بنمذجة منحنى بسيط من الفئة $C^1$ في $\mathbb{R}^2$ ونفذوا البرهان في خمس خطوات منطقية:

1. إعادة المعلمة (Reparametrization): تمت إعادة معلمة المنحنى من طول القوس $s \in [0, L]$ إلى معلم زاوي $\theta \in [0, 2\pi]$ لتسهيل تحليل فوريه.
2. صيغة المساحة (Area Formula): تم التعبير عن المساحة المحصورة $A$ باستخدام صيغة الشلال (Shoelace formula) (مبرهنة غرين): $A = \frac{1}{2} \int_0^L (x y' - y x') dt$. وبعد إعادة المعلمة والتكامل بالتجزئة، بسطت الصيغة إلى $A = \int_0^{2\pi} f(\theta)g'(\theta) d\theta$، حيث $f$ و $g$ هما دالتا الإحداثيات.
3. متباينة المتوسط الهندسي والحسابي (AM-GM Inequality): تطبيق المتباينة $2fg' \leq f^2 + (g')^2$ للحد من المساحة: $A \leq \frac{1}{2} \int_0^{2\pi} (f^2 + (g')^2) d\theta$.
4. تطبيق ويرتينجر (Wirtinger's Application): بافتراض أن المركز عند الأصل (متوسط صفري لـ $f$)، تم تطبيق متباينة ويرتينجر ($\int f^2 \leq \int (f')^2$). أدى ذلك إلى رفع الحد: $A \leq \frac{1}{2} \int_0^{2\pi} ((f')^2 + (g')^2) d\theta$.
5. قيد طول القوس (Arc-Length Constraint): باستخدام حقيقة أن المنحنى معلم بطول القوس، أظهر المؤلفون أن $(f')^2 + (g')^2 = (L/2\pi)^2$. وبالتعويض عن هذا الثابت في التكامل، تم الحصول على الحد النهائي: $A \leq \frac{L^2}{4\pi}$.

3. المساهمات الرئيسية

• أول صياغة كاملة لبرهان هيرتز: بينما توجد صياغات جزئية في أنظمة أخرى (Coq, Isabelle)، فإن هذا العمل هو برهان كامل ومتحقق منه آليًا لمنهج هيرتز التحليلي المحدد في Lean 4.
• توسيع Mathlib: وسع المشروع قدرات Mathlib في التحليل الحقيقي الكلاسيكي، وتحديدًا:
  • تنفيذ سلاسل فوريه الكلاسيكية مع متتاليات معاملات صريحة (بدلاً من مجرد نظرية $L^2$ مجردة).
  • صياغة اختبار فاييرشتراس ومبرهنات الاشتقاق حدًا بحد للسلاسل المثلثية.
  • سد الفجوة بين تعريفات الفضاء الإقليدي المجردة (EuclideanSpace) وحساب التفاضل والتكامل الإحداثي.
• التعامل مع التفاصيل التقنية الدقيقة: نجح المؤلفون في تجاوز تحديات الصياغة المعقدة، بما في ذلك:
  • تبادل المجموع والتكامل: استدعاء مبرهنة التقارب المحدود (Dominated Convergence Theorem) صراحةً عبر MeasureTheory.integral_tsum_of_summable_integral_norm.
  • اصطلاحات الفهرسة: حل التناقضات بين فهرسة الأعداد الطبيعية ($\mathbb{N}$) وفهرسة الأعداد الطبيعية الموجبة ($\mathbb{N}^+$) المستخدمة في معاملات فوريه.
  • اشتقاق الإسقاطات: التعامل بشكل صحيح مع تركيب مشتقات فريشيه للإسقاطات مع مشتقة المنحنى للتعامل مع دالات الإحداثيات في $\mathbb{R}^2$.

4. النتائج

تحقق التحقق الرسمي من المبرهنة الرئيسية:
$$\text{لأي منحنى بسيط مغلق من الفئة } C^1, \quad \text{Area}(\gamma) \leq \frac{\text{Length}(\gamma)^2}{4\pi}$$
البرهان متاح في المستودع العام IsoperimetricInequality على GitHub. تم هيكلة الكود المصدري في ملفين رئيسيين:

1. IsoperimenticalInequality.Basic: يحتوي على أسس تحليل فوريه (التعامد، بارسيفال، ويرتينجر).
2. IsoperimenticalInequality.Adolf Hurwitz proof: يحتوي على الاشتقاق الهندسي والمتباينة النهائية.

5. الأهمية

• اليقين في التحليل الكلاسيكي: يوضح هذا العمل أن حتى المبرهنات الكلاسيكية الراسخة تحتوي على تفاصيل تقنية دقيقة (شروط الانتظام، تبريرات التقارب) التي غالبًا ما يتم التغاضي عنها في البراهين المقروءة بشريًا ولكنها ضرورية للتحقق الرسمي.
• معيار لـ Lean 4: يعد هذا المشروع حالة دراسية هامة لنضج Lean 4 في التعامل مع التحليل الحقيقي الكلاسيكي بمستوى الدراسات العليا، بما في ذلك التكامل والاشتقاق والمتسلسلات اللانهائية.
• أساس للأعمال المستقبلية: من خلال صياغة آليات تحليل فوريه، أنشأ المؤلفون مكونات قابلة لإعادة الاستخدام لعمليات صياغة مستقبلية للنظرية الطيفية، وحساب التباين، وغيرها من المتباينات الهندسية.
• تحديد المشكلات المفتوحة: تشير الورقة إلى أنه بينما تم إثبات المتباينة، فإن حالة التساوي (توصيف الدائرة كأقصى قيمة فريدة) و اشتقاق هوية بارسيفال مباشرة من إحداثيات المنحنى (بدلاً من افتراضها كفرضية) تظل تحديات مفتوحة للعمل المستقبلي.

باختصار، تمثل هذه الورقة إعادة بناء صارم ومتحقق منه آليًا لبرهان هندسي كلاسيكي، مما يبرز قوة مساعدات الإثبات الحديثة في التحقق من الأسس المنطقية للتحليل الرياضي.