PositiveSourceMoment.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The moment estimate used for positive Poisson sources

A weak power-tail bound of exponent d gives every smaller positive moment. In the Poisson argument the tail follows by testing with a truncation and applying the Dirichlet Sobolev inequality. The constants below do not depend on an upper bound for the solution.

theorem OAI.RegularPointCoordinates.lintegral_small_rpow line 22
theorem OAI.RegularPointCoordinates.lintegral_large_rpow line 36

theorem OAI.RegularPointCoordinates.moment_lintegral_le_of_power_tail line 53

Source documentation

A tail bound at levels at least one gives an explicit smaller-moment bound; low levels cost only the total measure.

theorem moment_lintegral_le_of_power_tail {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ] {H : X → ℝ}
    (hH : AEMeasurable H μ) (hH0 : 0 ≤ᵐ[μ] H)
    {q d C : ℝ} (hq : 0 < q) (hqd : q < d) (hC : 0 ≤ C)
    (htail : ∀ t : ℝ, 1 ≤ t → μ {x | t ≤ H x} ≤ ENNReal.ofReal (C * t ^ (-d))) :
    (∫⁻ x, ENNReal.ofReal (H x ^ q) ∂μ) ≤
      ENNReal.ofReal q *
        (μ univ * ENNReal.ofReal q⁻¹ + ENNReal.ofReal C * ENNReal.ofReal (d - q)⁻¹) := by
…

theorem OAI.RegularPointCoordinates.integrable_rpow_of_power_tail line 93

Source documentation

The tail estimate also supplies genuine integrability of the moment.

theorem integrable_rpow_of_power_tail {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ] {H : X → ℝ}
    (hH : AEMeasurable H μ) (hH0 : 0 ≤ᵐ[μ] H)
    {q d C : ℝ} (hq : 0 < q) (hqd : q < d) (hC : 0 ≤ C)
    (htail : ∀ t : ℝ, 1 ≤ t → μ {x | t ≤ H x} ≤ ENNReal.ofReal (C * t ^ (-d))) :
    Integrable (fun x => H x ^ q) μ := by
…

theorem OAI.RegularPointCoordinates.integral_rpow_le_of_power_tail line 110

Source documentation

A real-valued form of the moment bound for subsequent energy estimates.

theorem integral_rpow_le_of_power_tail {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ] {H : X → ℝ}
    (hH : AEMeasurable H μ) (hH0 : 0 ≤ᵐ[μ] H)
    {q d C : ℝ} (hq : 0 < q) (hqd : q < d) (hC : 0 ≤ C)
    (htail : ∀ t : ℝ, 1 ≤ t → μ {x | t ≤ H x} ≤ ENNReal.ofReal (C * t ^ (-d))) :
    (∫ x, H x ^ q ∂μ) ≤ q * (μ.real univ * q⁻¹ + C * (d - q)⁻¹) := by
…