TorsionMoment.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Moment estimates for the torsion superlevel test

Hölder is applied to a bounded two-level truncation and the indicator of its support. The resulting algebraic estimate is the nonlinear gain needed by the superlevel iteration.

theorem OAI.RegularPointCoordinates.bounded_support_integral_le line 22

Source documentation

Hölder for a bounded nonnegative function supported on a measurable set.

theorem bounded_support_integral_le {X : Type*} [MeasurableSpace X]
    (ν : Measure X) [IsFiniteMeasure ν] {v : X → ℝ} (hv : AEMeasurable v ν)
    {M p q : ℝ} (hpq : p.HolderConjugate q)
    (hb : ∀ᵐ x ∂ν, 0 ≤ v x ∧ v x ≤ M)
    (S : Set X) (hS : MeasurableSet S) (hz : ∀ᵐ x ∂ν, x ∉ S → v x = 0) :
    (∫ x, v x ∂ν) ≤ (∫ x, v x ^ p ∂ν) ^ (1 / p) * (ν.real S) ^ (1 / q) := by
…

theorem OAI.RegularPointCoordinates.moment_le_of_sobolev_holder line 57

Source documentation

The scalar gain after combining Sobolev with the supported Hölder bound.

theorem moment_le_of_sobolev_holder {I C Y p : ℝ}
    (hI : 0 ≤ I) (hC : 0 ≤ C) (hY : 0 ≤ Y) (hp : 1 < p)
    (hbound : I ^ (2 / p) ≤ C * (I ^ (1 / p) * Y ^ ((p - 1) / p))) :
    I ≤ C ^ p * Y ^ (p - 1) := by
…