Euclidean isoperimetry, sharp inequalities, and rigidity

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremTauCeti.hasPrekopaLeindler_volume#

The Prékopa–Leindler inequality on a finite-dimensional real inner product space, such as EuclideanSpace ℝ (Fin n): its volume has the Prékopa–Leindler property at every weight 0 ≤ θ ≤ 1.

TauCeti.hasPrekopaLeindler_volume.{u_1} (E : Type u_1) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {θ : ℝ}
  (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : MeasureTheory.volume.HasPrekopaLeindler θ

Lean

Formalized in Tau Ceti as TauCeti.hasPrekopaLeindler_volume.

Sources

• Tau Ceti documentation: TauCeti.hasPrekopaLeindler_volume
• Source of TauCeti.hasPrekopaLeindler_volume in TauCeti/MeasureTheory/Integral/PrekopaLeindler.lean
• Tau Ceti roadmap status: Euclidean isoperimetry, sharp inequalities, and rigidity

LeanTauCeti.hasPrekopaLeindler_volume

Uses 1 · Used by 6

Proof usesPrékopa–Leindler inequality for the minimum on ℝ

Used byBall rigidity from the sharp first variation of parallel volume · Brunn–Minkowski for a shell · Brunn–Minkowski inequality · Brunn's concavity principle · Equality cases of multiplicative Brunn–Minkowski for convex bodies · Vaaler's cube-slicing theorem

TheoremBrunn–Minkowski inequality#

Brunn–Minkowski inequality for nonempty Lebesgue-measurable sets in a positive-dimensional real inner product space. The sum has its outer volume and need not be measurable or have finite volume.

TauCeti.volume_rpow_add_volume_rpow_le.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {A B : Set E}
  (hn : Module.finrank ℝ E ≠ 0) (hAn : A.Nonempty)
  (hA : MeasureTheory.NullMeasurableSet A MeasureTheory.volume) (hBn : B.Nonempty)
  (hB : MeasureTheory.NullMeasurableSet B MeasureTheory.volume) :
  MeasureTheory.volume A ^ (↑(Module.finrank ℝ E))⁻¹ +
      MeasureTheory.volume B ^ (↑(Module.finrank ℝ E))⁻¹ ≤
    MeasureTheory.volume (A + B) ^ (↑(Module.finrank ℝ E))⁻¹

Lean

Formalized in Tau Ceti as TauCeti.volume_rpow_add_volume_rpow_le.

Sources

• Tau Ceti documentation: TauCeti.volume_rpow_add_volume_rpow_le
• Source of TauCeti.volume_rpow_add_volume_rpow_le in TauCeti/MeasureTheory/Measure/Lebesgue/BrunnMinkowski/Basic.lean
• Tau Ceti roadmap status: Euclidean isoperimetry, sharp inequalities, and rigidity

LeanTauCeti.volume_rpow_add_volume_rpow_le

Uses 1 · Used by 1

Proof usesTauCeti.hasPrekopaLeindler_volume

Used byThe density theorem for rectifiable sets

TheoremEquality cases of multiplicative Brunn–Minkowski for convex bodies#

Let K and L be compact convex sets of positive volume and 0 < θ < 1. Then volume ((1 - θ) • K + θ • L) = volume K ^ (1 - θ) * volume L ^ θ exactly when L is a translate of K.

Convex.volume_smul_add_smul_eq_iff.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {K L : Set E}
  (hK : Convex ℝ K) (hKc : IsCompact K) (hK0 : MeasureTheory.volume K ≠ 0) (hL : Convex ℝ L)
  (hLc : IsCompact L) (hL0 : MeasureTheory.volume L ≠ 0) {θ : ℝ} (hθ₀ : 0 < θ) (hθ₁ : θ < 1) :
  MeasureTheory.volume ((1 - θ) • K + θ • L) =
      MeasureTheory.volume K ^ (1 - θ) * MeasureTheory.volume L ^ θ ↔
    ∃ v, L = v +ᵥ K

Lean

Formalized in Tau Ceti as Convex.volume_smul_add_smul_eq_iff.

Sources

• Tau Ceti documentation: Convex.volume_smul_add_smul_eq_iff
• Source of Convex.volume_smul_add_smul_eq_iff in TauCeti/MeasureTheory/Measure/Lebesgue/BrunnMinkowski/Homothety.lean
• Tau Ceti roadmap status: Euclidean isoperimetry, sharp inequalities, and rigidity

LeanConvex.volume_smul_add_smul_eq_iff

Uses 2

Proof usesBrunn's concavity principle · TauCeti.hasPrekopaLeindler_volume

TheoremEquality in the area–energy inequality#

For an absolutely continuous closed plane curve with square-integrable derivative, (b - a) ∫ₐᵇ ‖γ'‖² = 4π |signedArea γ a b| exactly when γ is constant or traverses a circle once at constant angular speed, in either orientation.

TauCeti.mul_integral_norm_sq_eq_four_pi_mul_abs_signedArea_iff {a b : ℝ} {γ γ' : ℝ → ℂ}
  (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b)
  (hγ' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt γ (γ' t) t) (hγab : γ a = γ b)
  (hL2 : MeasureTheory.MemLp γ' 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) :
  (b - a) * ∫ (t : ℝ) in a..b, ‖γ' t‖ ^ 2 = 4 * Real.pi * |TauCeti.signedArea γ a b| ↔
    ∃ c w,
      (∀ t ∈ Set.Icc a b, γ t = c + w * Complex.exp (2 * ↑Real.pi * Complex.I * ↑t / (↑b - ↑a))) ∨
        ∀ t ∈ Set.Icc a b, γ t = c + w * Complex.exp (-(2 * ↑Real.pi * Complex.I * ↑t / (↑b - ↑a)))

Lean

Formalized in Tau Ceti as TauCeti.mul_integral_norm_sq_eq_four_pi_mul_abs_signedArea_iff.

Sources

• Tau Ceti documentation: TauCeti.mul_integral_norm_sq_eq_four_pi_mul_abs_signedArea_iff
• Source of TauCeti.mul_integral_norm_sq_eq_four_pi_mul_abs_signedArea_iff in TauCeti/Analysis/Fourier/AreaEnergy.lean
• Tau Ceti roadmap status: Euclidean isoperimetry, sharp inequalities, and rigidity

LeanTauCeti.mul_integral_norm_sq_eq_four_pi_mul_abs_signedArea_iff

Uses 1

Proof usesParseval's energy identity

TheoremBall rigidity from the sharp first variation of parallel volume#

A convex body K of positive volume has parallel-volume root t ↦ volume (K + t • closedBall 0 1) ^ (1 / n) with right derivative volume (closedBall 0 1) ^ (1 / n) at zero exactly when K is a closed ball of positive radius.

ConvexBody.hasDerivWithinAt_volume_real_add_smul_closedBall_rpow_iff_exists_eq_closedBall.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (K : ConvexBody E) (hn : Module.finrank ℝ E ≠ 0)
  (hK : MeasureTheory.volume ↑K ≠ 0) :
  HasDerivWithinAt
      (fun t =>
        MeasureTheory.volume.real (↑K + t • Metric.closedBall 0 1) ^ (↑(Module.finrank ℝ E))⁻¹)
      (MeasureTheory.volume.real (Metric.closedBall 0 1) ^ (↑(Module.finrank ℝ E))⁻¹) (Set.Ioi 0)
      0 ↔
    ∃ c r, 0 < r ∧ ↑K = Metric.closedBall c r

Lean

Formalized in Tau Ceti as ConvexBody.hasDerivWithinAt_volume_real_add_smul_closedBall_rpow_iff_exists_eq_closedBall.

Sources

• Tau Ceti documentation: ConvexBody.hasDerivWithinAt_volume_real_add_smul_closedBall_rpow_iff_exists_eq_closedBall
• Source of ConvexBody.hasDerivWithinAt_volume_real_add_smul_closedBall_rpow_iff_exists_eq_closedBall in TauCeti/MeasureTheory/Measure/Lebesgue/BrunnMinkowski/Parallel.lean
• Tau Ceti roadmap status: Euclidean isoperimetry, sharp inequalities, and rigidity

LeanConvexBody.hasDerivWithinAt_volume_real_add_smul_closedBall_rpow_iff_exists_eq_closedBall

Uses 2

Proof usesBrunn's concavity principle · TauCeti.hasPrekopaLeindler_volume

DefinitionTauCeti.steinerSymmetrization#

Steiner symmetrization along the unit direction e, centered on its orthogonal hyperplane. The section of length ℓ is the open centered interval of radius ℓ / 2; this includes empty intervals for ℓ = 0 and the whole line for ℓ = ∞.

TauCeti.steinerSymmetrization.{u_1} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (e : E) (he : ‖e‖ = 1) (s : Set E) : Set E

Lean

Formalized in Tau Ceti as TauCeti.steinerSymmetrization.

Sources

• Tau Ceti documentation: TauCeti.steinerSymmetrization
• Source of TauCeti.steinerSymmetrization in TauCeti/MeasureTheory/Measure/Lebesgue/Steiner/Basic.lean
• Tau Ceti roadmap status: Euclidean isoperimetry, sharp inequalities, and rigidity

LeanTauCeti.steinerSymmetrization

DefinitionTauCeti.schwarzRearrangement#

The Schwarz rearrangement of f : E → ℝ≥0∞ with respect to μ: the radially nonincreasing function whose superlevel set {t < f*} is {x | μ (ball 0 ‖x‖) < μ {t < f}}. For an additive Haar measure on a nontrivial finite-dimensional real normed space, this is the centered open ball of the same measure when μ {t < f} is finite, and the whole space when it is infinite.

TauCeti.schwarzRearrangement.{u_1} {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E]
  (μ : MeasureTheory.Measure E) (f : E → ENNReal) (x : E) : ENNReal

Lean

Formalized in Tau Ceti as TauCeti.schwarzRearrangement.

Sources

• Tau Ceti documentation: TauCeti.schwarzRearrangement
• Source of TauCeti.schwarzRearrangement in TauCeti/MeasureTheory/Function/SchwarzRearrangement.lean
• Tau Ceti roadmap status: Euclidean isoperimetry, sharp inequalities, and rigidity

LeanTauCeti.schwarzRearrangement

Used by 1

Used byHardy--Littlewood rearrangement inequality

TheoremDe la Vallée Poussin's lemma#

Every integrable function f remains integrable after composing its norm with some convex, monotone function Φ with Φ 0 = 0 that grows superlinearly, Φ t / t → ∞.

MeasureTheory.Integrable.exists_convexOn_superlinear_integrable.{u_1, u_2} {α : Type u_1}
  {F : Type u_2} [MeasurableSpace α] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α}
  {f : α → F} (hf : MeasureTheory.Integrable f μ) :
  ∃ Φ,
    Φ 0 = 0 ∧
      Monotone Φ ∧
        ConvexOn ℝ Set.univ Φ ∧
          Filter.Tendsto (fun t => Φ t / t) Filter.atTop Filter.atTop ∧
            MeasureTheory.Integrable (fun a => Φ ‖f a‖) μ

Lean

Formalized in Tau Ceti as MeasureTheory.Integrable.exists_convexOn_superlinear_integrable.

Sources

• Tau Ceti documentation: MeasureTheory.Integrable.exists_convexOn_superlinear_integrable
• Source of MeasureTheory.Integrable.exists_convexOn_superlinear_integrable in TauCeti/MeasureTheory/Function/DeLaValleePoussin.lean
• Tau Ceti roadmap status: Euclidean isoperimetry, sharp inequalities, and rigidity

LeanMeasureTheory.Integrable.exists_convexOn_superlinear_integrable

TheoremThe isoperimetric inequality on the line#

A null-measurable set of positive finite measure in ℝ has perimeter at least two.

TauCeti.Real.two_le_perimeter {s : Set ℝ}
  (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (h0 : MeasureTheory.volume s ≠ 0)
  (hfin : MeasureTheory.volume s ≠ ⊤) : 2 ≤ TauCeti.perimeter MeasureTheory.volume ⊤ s

Lean

Formalized in Tau Ceti as TauCeti.Real.two_le_perimeter.

Sources

• Tau Ceti documentation: TauCeti.Real.two_le_perimeter
• Source of TauCeti.Real.two_le_perimeter in TauCeti/Analysis/BoundedVariation/Real.lean
• Tau Ceti roadmap status: Euclidean isoperimetry, sharp inequalities, and rigidity

LeanTauCeti.Real.two_le_perimeter

Uses 3

Statement usesTauCeti.perimeter

Proof usesLebesgue's differentiation theorem · TauCeti.totalVariationOn

TheoremBrunn's concavity principle#

if every fiber of a convex set has finite volume, the dimension root of the fiber volume is concave on the projection of the set.

Convex.concaveOn_volume_real_preimage_prodMk_rpow.{u_1, u_2} {P : Type u_1} {F : Type u_2}
  [AddCommGroup P] [_root_.Module ℝ P] [NormedAddCommGroup F] [InnerProductSpace ℝ F]
  [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {s : Set (P × F)} (hs : Convex ℝ s)
  (hfin : ∀ (p : P), MeasureTheory.volume (Prod.mk p ⁻¹' s) ≠ ⊤) :
  ConcaveOn ℝ (Prod.fst '' s) fun p =>
    MeasureTheory.volume.real (Prod.mk p ⁻¹' s) ^ (↑(Module.finrank ℝ F))⁻¹

Lean

Formalized in Tau Ceti as Convex.concaveOn_volume_real_preimage_prodMk_rpow.

Other forms

Brunn's concavity principle for hyperplane sections. Formalized in Tau Ceti as Convex.concaveOn_volume_real_hyperplaneSection_rpow.

Convex.concaveOn_volume_real_hyperplaneSection_rpow.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E}
  (hs : Convex ℝ s) {e : E} (he : ‖e‖ = 1)
  (hfin : ∀ (t : ℝ), MeasureTheory.volume {y | ↑y + t • e ∈ s} ≠ ⊤) :
  ConcaveOn ℝ ((fun x => inner ℝ e x) '' s) fun t =>
    MeasureTheory.volume.real {y | ↑y + t • e ∈ s} ^ (↑(Module.finrank ℝ E - 1))⁻¹

Brunn's concavity principle for hyperplane sections, extended form. Formalized in Tau Ceti as Convex.mul_volume_hyperplaneSection_rpow_add_mul_volume_hyperplaneSection_rpow_le.

Convex.mul_volume_hyperplaneSection_rpow_add_mul_volume_hyperplaneSection_rpow_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : Convex ℝ s) {e : E} (he : ‖e‖ = 1) {t u : ℝ}
  (ht : t ∈ (fun x => inner ℝ e x) '' s) (hu : u ∈ (fun x => inner ℝ e x) '' s) {a b : ℝ}
  (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
  ENNReal.ofReal a * MeasureTheory.volume {y | ↑y + t • e ∈ s} ^ (↑(Module.finrank ℝ E - 1))⁻¹ +
      ENNReal.ofReal b * MeasureTheory.volume {y | ↑y + u • e ∈ s} ^ (↑(Module.finrank ℝ E - 1))⁻¹ ≤
    MeasureTheory.volume {y | ↑y + (a * t + b * u) • e ∈ s} ^ (↑(Module.finrank ℝ E - 1))⁻¹

Brunn's concavity principle, extended form. Formalized in Tau Ceti as Convex.mul_volume_preimage_prodMk_rpow_add_mul_volume_preimage_prodMk_rpow_le.

Convex.mul_volume_preimage_prodMk_rpow_add_mul_volume_preimage_prodMk_rpow_le.{u_1, u_2}
  {P : Type u_1} {F : Type u_2} [AddCommGroup P] [_root_.Module ℝ P] [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F]
  {s : Set (P × F)} (hs : Convex ℝ s) {p q : P} (hp : (Prod.mk p ⁻¹' s).Nonempty)
  (hq : (Prod.mk q ⁻¹' s).Nonempty) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
  ENNReal.ofReal a * MeasureTheory.volume (Prod.mk p ⁻¹' s) ^ (↑(Module.finrank ℝ F))⁻¹ +
      ENNReal.ofReal b * MeasureTheory.volume (Prod.mk q ⁻¹' s) ^ (↑(Module.finrank ℝ F))⁻¹ ≤
    MeasureTheory.volume (Prod.mk (a • p + b • q) ⁻¹' s) ^ (↑(Module.finrank ℝ F))⁻¹

Sources

• Tau Ceti documentation: Convex.concaveOn_volume_real_preimage_prodMk_rpow
• Source of Convex.concaveOn_volume_real_preimage_prodMk_rpow in TauCeti/MeasureTheory/Measure/Lebesgue/BrunnMinkowski/Section.lean

LeanConvex.concaveOn_volume_real_preimage_prodMk_rpow · Convex.concaveOn_volume_real_hyperplaneSection_rpow · Convex.mul_volume_hyperplaneSection_rpow_add_mul_volume_hyperplaneSection_rpow_le · Convex.mul_volume_preimage_prodMk_rpow_add_mul_volume_preimage_prodMk_rpow_le

Uses 1 · Used by 2

Proof usesTauCeti.hasPrekopaLeindler_volume

Used byBall rigidity from the sharp first variation of parallel volume · Equality cases of multiplicative Brunn–Minkowski for convex bodies

TheoremBrunn's principle, in log-concave form#

For a measurable convex set s ⊆ E × F and a measure ν with the Prékopa–Leindler property at every weight, the measure of the slices, x ↦ ν (Prod.mk x ⁻¹' s), is log-concave.

Convex.logConcave_measure_preimage_prodMk.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [MeasurableSpace E] [AddCommMonoid E] [_root_.Module ℝ E] [MeasurableSpace F] [AddCommMonoid F]
  [_root_.Module ℝ F] {ν : MeasureTheory.Measure F}
  (hν : ∀ ⦃θ : ℝ⦄, 0 ≤ θ → θ ≤ 1 → ν.HasPrekopaLeindler θ) {s : Set (E × F)} (hs : MeasurableSet s)
  (hsc : Convex ℝ s) : TauCeti.LogConcave fun x => ν (Prod.mk x ⁻¹' s)

Lean

Formalized in Tau Ceti as Convex.logConcave_measure_preimage_prodMk.

Sources

• Tau Ceti documentation: Convex.logConcave_measure_preimage_prodMk
• Source of Convex.logConcave_measure_preimage_prodMk in TauCeti/MeasureTheory/Integral/PrekopaLeindler.lean

LeanConvex.logConcave_measure_preimage_prodMk

Used by 1

Used byVaaler's cube-slicing theorem

TheoremBrunn–Minkowski for a shell#

If the r-neighbourhood G + ball 0 r of a nonempty null-measurable set G lies in a set F of finite volume, then in dimension n ≥ 1 volume F - volume G ≥ n (volume G ^ (1 / n)) ^ (n - 1) r ω_n ^ (1 / n).

TauCeti.finrank_mul_rpow_pow_mul_le_volume_real_sub.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (hn : Module.finrank ℝ E ≠ 0) {G F : Set E}
  (hG : MeasureTheory.NullMeasurableSet G MeasureTheory.volume) (hG0 : G.Nonempty)
  (hF : MeasureTheory.volume F ≠ ⊤) {r : ℝ} (hr : 0 < r) (hsub : G + Metric.ball 0 r ⊆ F) :
  ↑(Module.finrank ℝ E) *
        (MeasureTheory.volume.real G ^ (↑(Module.finrank ℝ E))⁻¹) ^ (Module.finrank ℝ E - 1) *
      (r * MeasureTheory.volume.real (Metric.ball 0 1) ^ (↑(Module.finrank ℝ E))⁻¹) ≤
    MeasureTheory.volume.real F - MeasureTheory.volume.real G

Lean

Formalized in Tau Ceti as TauCeti.finrank_mul_rpow_pow_mul_le_volume_real_sub.

Sources

• Tau Ceti documentation: TauCeti.finrank_mul_rpow_pow_mul_le_volume_real_sub
• Source of TauCeti.finrank_mul_rpow_pow_mul_le_volume_real_sub in TauCeti/MeasureTheory/Measure/Lebesgue/BrunnMinkowski/Basic.lean

LeanTauCeti.finrank_mul_rpow_pow_mul_le_volume_real_sub

Uses 1 · Used by 1

Proof usesTauCeti.hasPrekopaLeindler_volume

Used byThe sharp BV Sobolev bound

TheoremDe la Vallée Poussin's criterion#

A family of a.e. strongly measurable functions with ∫ Φ(‖f i‖) ≤ C < ∞ for a superlinear Φ is uniformly integrable.

TauCeti.unifIntegrable_of_lintegral_ofReal_le.{u_1, u_2, u_3} {α : Type u_1} {F : Type u_2}
  {ι : Type u_3} [MeasurableSpace α] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α}
  {Φ : ℝ → ℝ} (hΦ : Filter.Tendsto (fun t => Φ t / t) Filter.atTop Filter.atTop) {f : ι → α → F}
  (hfm : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) {C : ENNReal} (hC : C ≠ ⊤)
  (hf : ∀ (i : ι), ∫⁻ (a : α), ENNReal.ofReal (Φ ‖f i a‖) ∂μ ≤ C) :
  MeasureTheory.UnifIntegrable f 1 μ

Lean

Formalized in Tau Ceti as TauCeti.unifIntegrable_of_lintegral_ofReal_le.

Other forms

De la Vallée Poussin's criterion, quantitative form. Formalized in Tau Ceti as TauCeti.exists_setLIntegral_enorm_le_mul_add.

TauCeti.exists_setLIntegral_enorm_le_mul_add.{u_1, u_2, u_3} {α : Type u_1} {F : Type u_2}
  {ι : Type u_3} [MeasurableSpace α] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α}
  {Φ : ℝ → ℝ} (hΦ : Filter.Tendsto (fun t => Φ t / t) Filter.atTop Filter.atTop) {f : ι → α → F}
  {C : ENNReal} (hC : C ≠ ⊤) (hf : ∀ (i : ι), ∫⁻ (a : α), ENNReal.ofReal (Φ ‖f i a‖) ∂μ ≤ C)
  {ε : ENNReal} (hε : ε ≠ 0) :
  ∃ T, ∀ (i : ι) (s : Set α), ∫⁻ (a : α) in s, ‖f i a‖ₑ ∂μ ≤ ↑T * μ s + ε

Sources

• Tau Ceti documentation: TauCeti.unifIntegrable_of_lintegral_ofReal_le
• Source of TauCeti.unifIntegrable_of_lintegral_ofReal_le in TauCeti/MeasureTheory/Function/DeLaValleePoussin.lean

LeanTauCeti.unifIntegrable_of_lintegral_ofReal_le · TauCeti.exists_setLIntegral_enorm_le_mul_add

Used by 1

Used byThe elementary renewal theorem

TheoremHardy--Littlewood rearrangement inequality#

For two nonnegative a.e.-measurable functions on a finite-dimensional real normed space, Schwarz rearrangement can only increase the integral of their product. The statement includes infinite integrals and dimension zero.

TauCeti.lintegral_mul_le_lintegral_schwarzRearrangement_mul.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f g : E → ENNReal}
  (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
  ∫⁻ (x : E), f x * g x ∂μ ≤
    ∫⁻ (x : E), TauCeti.schwarzRearrangement μ f x * TauCeti.schwarzRearrangement μ g x ∂μ

Lean

Formalized in Tau Ceti as TauCeti.lintegral_mul_le_lintegral_schwarzRearrangement_mul.

Sources

• Tau Ceti documentation: TauCeti.lintegral_mul_le_lintegral_schwarzRearrangement_mul
• Source of TauCeti.lintegral_mul_le_lintegral_schwarzRearrangement_mul in TauCeti/MeasureTheory/Function/SchwarzRearrangement.lean

LeanTauCeti.lintegral_mul_le_lintegral_schwarzRearrangement_mul

Uses 1

Statement usesTauCeti.schwarzRearrangement

TheoremPrékopa–Leindler inequality for the minimum on ℝ#

If f and g have the same supremum and h (c * x + d * y) dominates min (f x) (g y) for all x and y, then c ∫ f + d ∫ g ≤ ∫ h. The coefficients may vanish, and the common supremum and the integrals may be infinite.

TauCeti.Real.mul_lintegral_add_mul_lintegral_le {f g h : ℝ → ENNReal}
  (hf : AEMeasurable f MeasureTheory.volume) (hg : AEMeasurable g MeasureTheory.volume)
  (hh : AEMeasurable h MeasureTheory.volume) (hfg : ⨆ x, f x = ⨆ y, g y) {c d : ℝ} (hc : 0 ≤ c)
  (hd : 0 ≤ d) (hmin : ∀ (x y : ℝ), min (f x) (g y) ≤ h (c * x + d * y)) :
  (ENNReal.ofReal c * ∫⁻ (x : ℝ), f x) + ENNReal.ofReal d * ∫⁻ (y : ℝ), g y ≤ ∫⁻ (z : ℝ), h z

Lean

Formalized in Tau Ceti as TauCeti.Real.mul_lintegral_add_mul_lintegral_le.

Sources

• Tau Ceti documentation: TauCeti.Real.mul_lintegral_add_mul_lintegral_le
• Source of TauCeti.Real.mul_lintegral_add_mul_lintegral_le in TauCeti/MeasureTheory/Integral/PrekopaLeindler.lean

LeanTauCeti.Real.mul_lintegral_add_mul_lintegral_le

Used by 1

Used byTauCeti.hasPrekopaLeindler_volume

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.