Formalization of the isoperimetric inequality

This repository contains Lean 4 proofs of the isoperimetric inequality, Brunn-Minkowski inequality, and Prékopa-Leindler inequality, following this blog post by Terence Tao.

The results proved are:

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 := ...

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)⁻¹ := ...

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 ε := ...