High-contrast homogenization: Provider.Response.RowCellPairingProducer #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The annealed cell pairing #
Averaging the per-cell pairing over the law is a Cauchy-Schwarz step in L² of
the law: the energy side collects the annealed cell energy and the load side
collects, by linearity of the block's diagonal entries, the Schur load of the
annealed block itself.
The coefficient is the recentred sample, whose coarse response is the shear congruence of the original one, so the load that appears is the hatted load the response row carries.
Cauchy-Schwarz in L² of a measure #
theorem
HCPolySupport.HighContrast.Response.integral_mul_le_sqrt_mul_sqrt
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f g : α → ℝ}
(hf : MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ)
(hg : MeasureTheory.Integrable (fun (x : α) => g x ^ 2) μ)
(hfg : MeasureTheory.Integrable (fun (x : α) => f x * g x) μ)
:
Cauchy-Schwarz for Bochner integrals at exponent two. Obtained from the
nonnegativity of the quadratic t ↦ ∫ (t f + g)² through its discriminant.