OAI/Analysis/AffineBernstein/MassUpper.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.lintegral_tube_mass_le line 17

   Source comment

   The source's unweighted tube mass estimate from support height and the two actual determinant integrals. A positive angular determinant is not needed for this upper estimate: the real square root already discards its negative part.

   lemma lintegral_tube_mass_le {n : ℕ} {h B Q : X → ℝ}
       (hB : AEMeasurable B μ) (hQ : AEMeasurable Q μ)
       (hBp : ∀ᵐ x ∂μ, 0 ≤ B x) {r : ℝ} (hr : 0 < r)
       (hbound : ∀ᵐ x ∂μ, r ≤ h x) :
       (∫⁻ x, ENNReal.ofReal (tubeMeasureCoefficient n (h x) (B x) (Q x)) ∂μ) ≤
         ENNReal.ofReal (r ^ (-(n:ℝ)/2)) *
           (∫⁻ x, ENNReal.ofReal (B x) ∂μ) ^ (1/(2:ℝ)) *
           (∫⁻ x, ENNReal.ofReal (Q x) ∂μ) ^ (1/(2:ℝ)) := by
   …

   Mentions: OAI.AffineBernstein.tubeMeasureCoefficient