High-contrast homogenization: Provider.Quenched.AlignedSubdivisionQuadraticGap

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

Quadratic gap over an aligned subdivision

The response on a parent adapted cell is below the arithmetic mean of the responses on its aligned children. The sharp involution turns the harmonic gap of those children into a quadratic fluctuation. This module combines the two facts while retaining the pathwise, matrix-valued form of the estimate.

noncomputable def HCPolySupport.HighContrast.Quenched.fullBlockSharpFluctuation {d : ℕ} (A G : FullBlockMat d) : FullBlockMat d

The fluctuation expression obtained after combining the sharp quadratic gap with the primal-minus-sharp remainder.

Equations

• HCPolySupport.HighContrast.Quenched.fullBlockSharpFluctuation A G = A - G + G * ((HCPolySupport.HighContrast.fullBlockSharp A)⁻¹ - G⁻¹) * G

theorem HCPolySupport.HighContrast.Quenched.fullBlockSharp_quadratic_add_primal_sub_eq_fluctuation {d : ℕ} {A G : FullBlockMat d} (hA : Matrix.PosDef A) (hG : Matrix.PosDef G) : (fullBlockSharp A - G) * (fullBlockSharp A)⁻¹ * (fullBlockSharp A - G) + (A - fullBlockSharp A) = fullBlockSharpFluctuation A G

The sharp quadratic term and the primal-minus-sharp remainder combine into the fluctuation expression used by the variance estimate.