Isoperimetric inequality

Stream: new members

[JH]

Hi all,

As a first project to learn Lean, I have written up a proof of the isoperimetric inequality, Brunn-Minkowski inequality, and Prekopa-Leindler inequality. The code is here: https://github.com/hojonathanho/isoperimetric/ and the theorem statements are:

import Mathlib
open MeasureTheory Pointwise

def PLConditions (n : ℕ) (θ : ℝ) (f g h : (Fin n → ℝ) → ENNReal) : Prop :=
  0 < θ ∧ θ < 1 ∧
  Measurable f ∧ Measurable g ∧ Measurable h ∧
  (∀ x y, (f x) ^ (1 - θ) * (g y) ^ θ ≤ h (x + y))

theorem prekopa_leindler
    {d : ℕ} {θ : ℝ} {f g h : (Fin (d + 1) → ℝ) → ENNReal}
    (hθfgh : PLConditions (d + 1) θ f g h)
    : ENNReal.ofReal ((1 - θ) ^ ((d + 1) * (1 - θ)) * θ ^ ((d + 1) * θ))⁻¹
      * (∫⁻ x, f x) ^ (1 - θ) * (∫⁻ x, g x) ^ θ ≤ ∫⁻ x, h x := sorry

theorem brunn_minkowski
    {d : ℕ} {A B : Set (Fin (d + 1) → ℝ)}
    (hA_nonempty : A.Nonempty) (hA_measurable : MeasurableSet A)
    (hB_nonempty : B.Nonempty) (hB_measurable : MeasurableSet B)
    (hAB_measurable : MeasurableSet (A + B))
    : volume A ^ ((d : ℝ) + 1)⁻¹ + volume B ^ ((d : ℝ) + 1)⁻¹
      ≤ volume (A + B) ^ ((d : ℝ) + 1)⁻¹ := sorry

theorem isoperimetric_inequality
    {d : ℕ} {ε : ℝ} (hε : ε > 0) {A : Set (EuclideanSpace ℝ (Fin (d + 1)))}
    (hA_nonempty : A.Nonempty) (hA_measurable : MeasurableSet A) (hA_finite : volume A ≠ ⊤)
    : (d + 1) * (volume A) ^ (1 - ((d : ℝ) + 1)⁻¹)
      * volume (Metric.ball (0 : EuclideanSpace ℝ (Fin (d + 1))) 1) ^ ((d : ℝ) + 1)⁻¹
      ≤ (volume (A + Metric.ball 0 ε) - volume A) / ENNReal.ofReal ε := sorry

I'd appreciate any comments or suggestions for improvement. The proofs follow this blog post by Terence Tao.
(I only recently became aware of an existing effort in Zulip to formalize these theorems; I apologize and I didn't mean to scoop this effort.)

[Kevin Buzzard]

(can you edit your post, adding imports to make it a #mwe ? It's easier for other people to just click the top right of your code and see/run it live if you do).

[Yongxi Lin (Aaron)]

Are you aware of this project: https://github.com/Brunn-Minkowski-in-Lean/BrunnMinkowski?

[JH]

Sorry, I was not aware of that project since I neglected to search Zulip until too late.

[Yongxi Lin (Aaron)]

There is no need to apologize :joy: , I just think you should try to contact with contributors of the project I mentioned.

[Shreyas Srinivas]

Was there use of AI?

[JH]

I used Claude to learn Lean syntax, learn how to use lake, and suggest how to shorten proofs of theorems I had already proved. Other than that, everything was written and checked manually by me.