SourceCrudeMomentAE.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere node and mass bounds suffice for normalized moments. This lets the spatial measure be restricted to the common good set, without adding bounds at points excluded by the construction.

theorem OAI.LipschitzHilbert.source_node_normalized_moment_ae line 15

theorem OAI.LipschitzHilbert.eventually_source_crude_normalized_moment_ae line 50

Source documentation

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

theorem eventually_source_crude_normalized_moment_ae (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 ≤ 2*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 (4*Real.sqrt L) := by
…