OAI/Geometry/RCD/Metric/IntegralSquareProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integral Cauchy--Schwarz from a pointwise product bound

  1. theorem OAI.RegularPointCoordinates.quadratic_nonneg_of_square_bound line 12
  2. theorem OAI.RegularPointCoordinates.integral_sq_le_of_sq_le_product line 27

    Source documentation

    No square integrability of H is required: the pointwise product bound and integrability of the three entries suffice.

    theorem integral_sq_le_of_sq_le_product {X : Type*} [MeasurableSpace X]
    (μ : Measure X) {F G H : X → ℝ} (hF : Integrable F μ) (hG : Integrable G μ)
    (hH : Integrable H μ) (hF0 : ∀ᵐ x ∂μ, 0≤F x) (hG0 : ∀ᵐ x ∂μ, 0≤G x)
    (hbound : ∀ᵐ x ∂μ, (H x)^2≤F x*G x) :
    (∫ x, H x ∂μ)^2≤(∫ x, F x ∂μ)*(∫ x, G x ∂μ) := by
…