Nonnegative integral Gram kernels

Extended Cauchy–Schwarz, including zero and infinite diagonal integrals.

The energy of an integral Gram kernel is itself an integral Gram pairing of potentials.

theorem LiebThirring.lintegral_mul_sq_le {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) {f g : Ω → ENNReal} (hf : Measurable f) (hg : Measurable g) : (∫⁻ (z : Ω), f z * g z ∂ν) ^ 2 ≤ (∫⁻ (z : Ω), f z ^ 2 ∂ν) * ∫⁻ (z : Ω), g z ^ 2 ∂ν

Extended Cauchy–Schwarz, including zero and infinite diagonal integrals.

theorem LiebThirring.lintegral_gram_pairing {X : Type u_1} {Ω : Type u_2} [MeasurableSpace X] [MeasurableSpace Ω] (α β : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Ω) [MeasureTheory.SFinite α] [MeasureTheory.SFinite β] [MeasureTheory.SFinite ν] (f : X → Ω → ENNReal) (hf : Measurable (Function.uncurry f)) : ∫⁻ (x : X), ∫⁻ (y : X), ∫⁻ (z : Ω), f x z * f y z ∂ν ∂β ∂α = ∫⁻ (z : Ω), (∫⁻ (x : X), f x z ∂α) * ∫⁻ (y : X), f y z ∂β ∂ν

The energy of an integral Gram kernel is itself an integral Gram pairing of potentials.