SourceCrudeMoment.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The linear node envelope gives the crude normalized moment on the whole phase tube. Only the first power of the mass is integrated; its remaining small power is controlled by the root mass bound.

theorem OAI.LipschitzHilbert.source_node_normalized_energy_le line 16
theorem OAI.LipschitzHilbert.source_node_normalized_moment line 44

theorem OAI.LipschitzHilbert.eventually_source_crude_normalized_moment line 78

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 (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
…