High-contrast homogenization: Provider.Response.AnnealedCutoffEnergyComponent

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

The cutoff-energy component of the pre-Young estimate

The annealed cutoff-energy estimate bounds an expectation by the expectation of a sum of a multiple of the response and a product of two square roots. The compact assembly consumes instead three extended-nonnegative terms built from the roots of the response defect and of the terminal response.

This module performs that reduction. The product of roots is integrated by Cauchy-Schwarz, so the two remaining expectations are the terminal response and the partition defect; the resulting real inequality is then transferred to the extended nonnegative reals, where the two roots reappear as the two factors of each quadratic term.

Square integrability of a root

theorem HCPolySupport.HighContrast.Response.memLp_two_sqrt_of_integrable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) (hfnn : 0 ≤ᵐ[μ] f) : MeasureTheory.MemLp (fun (x : α) => √(f x)) 2 μ

The square root of a nonnegative integrable observable is square integrable.

theorem HCPolySupport.HighContrast.Response.integrable_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) : MeasureTheory.Integrable (fun (x : α) => √(f x) * √(g x)) μ

The product of the roots of two nonnegative integrable observables is integrable.

The annealed right-hand side

theorem HCPolySupport.HighContrast.Response.integral_cutoffEnergyBound_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {J D T : α → ℝ} {Ccut expo EJ tau : ℝ} (hJnn : 0 ≤ᵐ[μ] J) (hTnn : 0 ≤ᵐ[μ] T) (hDT : D =ᵐ[μ] T) (hJ : MeasureTheory.Integrable J μ) (hT : MeasureTheory.Integrable T μ) (hbound : MeasureTheory.Integrable (fun (a : α) => Ccut * expo * J a + √(D a) * √(4 * J a + 2 * T a)) μ) (hEJ : ∫ (a : α), J a ∂μ = EJ) (htau : ∫ (a : α), T a ∂μ = tau) : ∫ (a : α), Ccut * expo * J a + √(D a) * √(4 * J a + 2 * T a) ∂μ ≤ 2 * tau + 4 * (√tau * √EJ) + Ccut * expo * EJ

The expectation of the samplewise cutoff-energy bound. The product of the two roots is integrated by Cauchy-Schwarz, leaving only the expectations of the response and of the partition defect.

The extended nonnegative component

theorem HCPolySupport.HighContrast.Response.ofReal_abs_le_cutoffEnergyComponent {x Ccut expo EJ tau : ℝ} (hCcut : 0 ≤ Ccut) (hexpo : 0 ≤ expo) (hEJ : 0 ≤ EJ) (htau : 0 ≤ tau) (hx : |x| ≤ 2 * tau + 4 * (√tau * √EJ) + Ccut * expo * EJ) : ENNReal.ofReal |x| ≤ ENNReal.ofReal 2 * ENNReal.ofReal √tau * ENNReal.ofReal √tau + ENNReal.ofReal 4 * ENNReal.ofReal √tau * ENNReal.ofReal √EJ + ENNReal.ofReal Ccut * ENNReal.ofReal expo * ENNReal.ofReal √EJ * ENNReal.ofReal √EJ

The cutoff-energy component. A real bound by the response defect, the mixed root product, and the scaled response becomes the exact three-term extended-nonnegative expression consumed by the compact assembly, in which each quadratic term is written as a product of two roots.

The annealed cutoff-energy component