OAI/Geometry/RCD/Heat/CappedIntegralProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.integrable_min_nonneg line 15
2. theorem OAI.RegularPointCoordinates.integrable_capped_product line 23
3. theorem OAI.RegularPointCoordinates.capped_product_sub_le line 32
4. theorem OAI.RegularPointCoordinates.integral_capped_product_sub_le line 53

   Source documentation

   Capping makes the overlap pairing continuous for the L¹ distance.

   theorem integral_capped_product_sub_le {f g f' g' : X → ℝ}
       (hf : Integrable f μ) (hg : Integrable g μ) (hf' : Integrable f' μ) (hg' : Integrable g' μ)
       (hf0 : ∀ x, 0 ≤ f x) (hg0 : ∀ x, 0 ≤ g x)
       (hf0' : ∀ x, 0 ≤ f' x) (hg0' : ∀ x, 0 ≤ g' x) (C : ℝ≥0) :
       |(∫ x, min (f x) C * min (g x) C ∂μ) -
         (∫ x, min (f' x) C * min (g' x) C ∂μ)| ≤
         C * ((∫ x, |f x - f' x| ∂μ) + ∫ x, |g x - g' x| ∂μ) := by
   …