SourceCrudeMassBudget.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The polynomial total-mass factor requires one extra unit of logarithmic slack beyond the manuscript's log N ≤ 2L. This leaves the same Gaussian large-imaginary argument, with exp(6√L) in its crude bound.

theorem OAI.LipschitzHilbert.eventually_source_crude_mass_budget line 17

Source documentation

For p=√L the root mass contributes only exp(6√L), uniformly in the imaginary phase. This is the crude estimate in §11.

theorem eventually_source_crude_mass_budget (q b : ℝ) (_hb : 0 ≤ b) :
    ∀ᶠ L : ℝ in atTop, ∀ (μ : Measure X)
      (n : X → ℝ) (A : X → EuclideanSpace ℂ κ) (U S alpha r : ℝ),
      (∀ x, 0 < n x) → (∀ᵐ x ∂μ, n x ≤ U) → Measurable n → Integrable n μ →
      Measurable A → 0 < U → 0 ≤ S → 1 ≤ alpha → alpha ≤ 3 → 0 ≤ r →
      Real.log U ≤ 3*L → (∫ x, n x ∂μ) ≤ L^b*S →
      (∀ᵐ x ∂μ, ‖A x‖ ≤ L^q*(1+r)*n x) →
      Integrable (fun x => ‖(n x^(alpha/Real.sqrt L-1)) • A x‖^(Real.sqrt L)) μ ∧
      (∫ x, ‖(n x^(alpha/Real.sqrt L-1)) • A x‖^(Real.sqrt L) ∂μ)^(1/Real.sqrt L) ≤
        (L^(q+1)*S^(1/Real.sqrt L))*(1+r)*Real.exp (6*Real.sqrt L) := by
…