MassIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.lintegral_weighted_tube_interpolation line 17

Source comment

The exact inverse-Hessian interpolation used in the source cell bound. The two controlling integrals are the cap identity term and the true large principal-minor term; no bound on the weighted integral is presumed.

lemma lintegral_weighted_tube_interpolation {n : ℕ} (hn : 1 ≤ n)
    {B Q t : X → ℝ} (hB : AEMeasurable B μ) (hQ : AEMeasurable Q μ)
    (ht : AEMeasurable t μ) (hBp : ∀ᵐ x ∂μ, 0 < B x)
    (hQp : ∀ᵐ x ∂μ, 0 < Q x) (htp : ∀ᵐ x ∂μ, 0 < t x) :
    (∫⁻ x, ENNReal.ofReal (Real.sqrt (B x*Q x)*t x) ∂μ) ≤
      (∫⁻ x, ENNReal.ofReal (B x ^ (1/((n:ℝ)+2)) * Q x ^ (1-1/((n:ℝ)+2))*t x) ∂μ) ^
        (((n:ℝ)+2)/(2*((n:ℝ)+1))) *
      (∫⁻ x, ENNReal.ofReal (B x*t x) ∂μ) ^ (1-((n:ℝ)+2)/(2*((n:ℝ)+1))) := by
…

lemma OAI.AffineBernstein.lintegral_tube_area_le_mass line 44

Source comment

Controlling the fiber area and the support height converts a positive amount of affine area into a lower bound on the true invariant tube mass.

lemma lintegral_tube_area_le_mass {n : ℕ} (hn : 1 ≤ n)
    {h B Q : X → ℝ} (hh : AEMeasurable h μ) (hB : AEMeasurable B μ)
    (hQ : AEMeasurable Q μ) (hhp : ∀ᵐ x ∂μ, 0 < h x)
    (hBp : ∀ᵐ x ∂μ, 0 < B x) (hQp : ∀ᵐ x ∂μ, 0 < Q x)
    {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ᵐ x ∂μ, h x ≤ M) :
    (∫⁻ x, ENNReal.ofReal (B x ^ (1/((n:ℝ)+2)) * Q x ^ (1-1/((n:ℝ)+2))) ∂μ) ≤
      ENNReal.ofReal (M ^ ((n:ℝ)/((n:ℝ)+2))) *
      (∫⁻ x, ENNReal.ofReal (tubeMeasureCoefficient n (h x) (B x) (Q x)) ∂μ)^(2/((n:ℝ)+2)) *
      (∫⁻ x, ENNReal.ofReal (Q x) ∂μ)^(1-2/((n:ℝ)+2)) := by
…

Mentions: OAI.AffineBernstein.tubeMeasureCoefficient