OAI/Geometry/RCD/Metric/RadonDensityL2Bound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.memLp_two_of_sq_le_radon line 17

   Source documentation

   A bound by the absolutely continuous density gives an L² estimate by full positive mass. Singular mass is retained in the upper bound.

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

2. theorem OAI.RegularPointCoordinates.memLp_two_of_radon_direction line 39

   Source documentation

   A bounded direction turns the pointwise quadratic estimate into a full-mass bound with the square of its energy bound.

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