OAI/Geometry/RCD/Harmonic/CappedPairingL2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

L² control from pairings with capped nonnegative functions

  1. theorem OAI.RegularPointCoordinates.integral_sq_le_of_capped_pairing line 16

    Source documentation

    Testing only the capped function itself suffices for the L² conclusion.

    theorem integral_sq_le_of_capped_pairing {f : X → ℝ}
    (hf : Measurable f) (hi : Integrable f μ) (hfn : ∀ x, 0 ≤ f x)
    {A : ℝ} (hA : 0 ≤ A)
    (hpair : ∀ C : ℝ≥0, (∫ x, f x * min (f x) C ∂μ) ≤
      A * Real.sqrt (∫ x, (min (f x) C)^2 ∂μ)) :
    Integrable (fun x => (f x)^2) μ ∧ (∫ x, (f x)^2 ∂μ) ≤ A^2 := by
…