ShiftedRadonBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating shifted density bounds without discarding singular mass

theorem OAI.RegularPointCoordinates.memLp_two_of_sq_le_shifted_radon line 17

Source documentation

A density bound with a constant shift is integrated against the full positive measure. Its singular part is retained in the upper bound.

theorem memLp_two_of_sq_le_shifted_radon (σ : Measure X) [IsFiniteMeasure σ]
    {S : Set X} [IsFiniteMeasure (μ.restrict S)] {f : X → ℝ}
    (hf : AEStronglyMeasurable f (μ.restrict S))
    (c B : ℝ) (hB : 0≤B)
    (hbound : ∀ᵐ x ∂μ.restrict S, (f x)^2≤B*((σ.rnDeriv μ x).toReal-c)) :
    MemLp f 2 (μ.restrict S) ∧
      (∫ x in S, (f x)^2 ∂μ)≤B*(σ.real S-c*μ.real S) := by
…

theorem OAI.RegularPointCoordinates.memLp_two_of_shifted_radon_product line 43

Source documentation

The mixed estimate permits separate caps on both gradient lengths.

theorem memLp_two_of_shifted_radon_product (σ : Measure X) [IsFiniteMeasure σ]
    {S : Set X} [IsFiniteMeasure (μ.restrict S)] {f g h : X → ℝ}
    (hf : AEStronglyMeasurable f (μ.restrict S)) (c C D : ℝ)
    (hC : 0≤C) (hD : 0≤D)
    (hden : ∀ᵐ x ∂μ.restrict S, c≤(σ.rnDeriv μ x).toReal)
    (hg : ∀ᵐ x ∂μ.restrict S, 0≤g x ∧ g x≤C)
    (hh : ∀ᵐ x ∂μ.restrict S, 0≤h x ∧ h x≤D)
    (hbound : ∀ᵐ x ∂μ.restrict S,
      (f x)^2≤((σ.rnDeriv μ x).toReal-c)*g x*h x) :
    MemLp f 2 (μ.restrict S) ∧
      (∫ x in S, (f x)^2 ∂μ)≤(C*D)*(σ.real S-c*μ.real S) := by
…

theorem OAI.RegularPointCoordinates.measure_lower_of_radon_lower line 65

Source documentation

A local lower bound for the absolutely continuous density bounds the full positive mass on every measurable subset, for either sign of c.

theorem measure_lower_of_radon_lower (σ : Measure X) [IsFiniteMeasure σ]
    {Ω : Set X} [IsFiniteMeasure (μ.restrict Ω)]
    (c : ℝ) (hc : ∀ᵐ x ∂μ.restrict Ω, c≤(σ.rnDeriv μ x).toReal)
    (s : Set X) (hs : MeasurableSet s) :
    c*(μ.restrict Ω).real s≤σ.real s := by
…

theorem OAI.RegularPointCoordinates.shiftedBochnerLowerBound_of_density line 92

Source documentation

The local density consequence of the finite-dimensional inequality constructs positivity of the full shifted measure.

theorem shiftedBochnerLowerBound_of_density (M : PositiveBilinearMeasure X E)
    {Ω : Set X} [IsFiniteMeasure (μ.restrict Ω)]
    (ell : E →ₗ[ℝ] ℝ) (n : ℝ)
    (hd : ∀ v b, ∀ᵐ x ∂μ.restrict Ω,
      2*b*ell v-n*b^2≤((M.measure v).rnDeriv μ x).toReal) :
    ShiftedBochnerLowerBound M (μ.restrict Ω) ell n := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.ShiftedBochnerLowerBound