High-contrast homogenization: Provider.Response.AnnealedCutoffEnergy

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The annealed cutoff-energy estimate

The samplewise cutoff-energy estimate keeps the cutoff-weighted child responses inside the absolute value, because for a single coefficient sample they do not vanish. Averaging over a translation invariant law removes them, and what is left is an estimate for the expectation of the cutoff-weighted energy defect alone.

This module performs that average. The expectation of the correction is zero by the annealed vanishing; the remaining composition is a mean-zero correction combinator, so the only additional inputs are integrability hypotheses and one equality saying that the reference coefficient family represents the sample. The right-hand side is then reduced to expectations of the response, the partition defect, and the difference energy by an integral form of the Cauchy-Schwarz inequality.

Cauchy-Schwarz for the roots of two nonnegative observables

theorem HCPolySupport.HighContrast.Response.integral_sqrt_mul_sqrt_le_sqrt_mul_sqrt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfnn : 0 ≤ᵐ[μ] f) (hgnn : 0 ≤ᵐ[μ] g) : ∫ (x : α), √(f x) * √(g x) ∂μ ≤ √(∫ (x : α), f x ∂μ) * √(∫ (x : α), g x ∂μ)

Cauchy-Schwarz for square roots. The expectation of a product of square roots of nonnegative integrable observables is at most the product of the roots of their expectations.

The annealed cutoff-energy estimate