WeightedMassUpper.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.lintegral_weighted_tube_mass_le line 16

Source comment

The determinant interpolation controls the genuine tube mass with inverse trace weight after using only the normalized positive support-height bound.

lemma lintegral_weighted_tube_mass_le {n : ℕ} (hn : 1 ≤ n)
    {h 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)
    {r : ℝ} (hr : 0 < r) (hbound : ∀ᵐ x ∂μ, r ≤ h x) :
    (∫⁻ x, ENNReal.ofReal (tubeMeasureCoefficient n (h x) (B x) (Q x)*t x) ∂μ) ≤
      ENNReal.ofReal (r^(-(n:ℝ)/2)) *
      (∫⁻ 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
…

Mentions: OAI.AffineBernstein.tubeMeasureCoefficient

lemma OAI.AffineBernstein.lintegral_sigma_mass_le line 48

Source comment

Full sigma mass estimate. The inputs are the source determinant, fiber area, cap inverse-energy, and principal-minor integrals, not an assumed sigma bound. This is manuscript bounds.tex322–351 before geometric normalization.

lemma lintegral_sigma_mass_le {n : ℕ} (hn : 1 ≤ n)
    {h B Q t W : X → ℝ} (hh : AEMeasurable h μ)
    (hB : AEMeasurable B μ) (hQ : AEMeasurable Q μ) (ht : AEMeasurable t μ)
    (hBp : ∀ᵐ x ∂μ, 0 < B x) (hQp : ∀ᵐ x ∂μ, 0 < Q x)
    (htp : ∀ᵐ x ∂μ, 0 < t x)
    {r K : ℝ} (hr : 0 < r) (hK : 0 ≤ K)
    (hbound : ∀ᵐ x ∂μ, r ≤ h x) (hW : ∀ᵐ x ∂μ, W x ≤ 1+K*t x) :
    (∫⁻ x, ENNReal.ofReal (tubeMeasureCoefficient n (h x) (B x) (Q x)*W x) ∂μ) ≤
      ENNReal.ofReal (r^(-(n:ℝ)/2)) *
        (∫⁻ x, ENNReal.ofReal (B x) ∂μ)^(1/(2:ℝ)) *
        (∫⁻ x, ENNReal.ofReal (Q x) ∂μ)^(1/(2:ℝ)) +
      ENNReal.ofReal K * (ENNReal.ofReal (r^(-(n:ℝ)/2)) *
…

Mentions: OAI.AffineBernstein.tubeMeasureCoefficient