High-contrast homogenization: Analytic.CenteringInvariance

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

Flux centering, and the classes that must not be vacuous

The flux differences of e.random.dirichlet and e.random.corrector are written for the skew-centered coefficient field. The first section is the reason: a constant antisymmetric matrix added to the coefficient field and to the homogenized matrix leaves the centered flux difference unchanged, while it moves the uncentered difference by that matrix applied to the difference of the two gradients — a quantity no datum of the hypotheses sees.

The remaining sections check that the corrector equation of t.random.homogenization, the growth condition of the Liouville class e.random.liouville.growth and the coefficient-weighted energies of the weighted solution spaces of s.introduction are not satisfied by the failure of an integral: each pairing carries its own absolute convergence, each energy is valued in ℝ≥0∞, and each class is inhabited by the zero field, so none of them is vacuous in either direction. A ball sandwich finally makes its domain nonempty, hence of positive volume, which is what keeps the volume averages and volume-normalized norms from collapsing.

The centering convention makes the flux displays invariant

A constant antisymmetric matrix added to the coefficient field changes neither the solutions nor the coarse-grained blocks, and it moves the homogenized matrix by the same constant. The flux differences of the two estimates are written for the skew-centered field precisely so that they are unmoved by that change; the displays written with the full homogenized matrix are moved by it, and by a quantity no datum of the hypotheses sees.

theorem HCPolySupport.HighContrast.isSkewMat_apply {d : ℕ} {h : Mat d} (hh : IsSkewMat h) (i j : Fin d) : h j i = -h i j

theorem HCPolySupport.HighContrast.symmPart_add_isSkewMat {d : ℕ} {M h : Mat d} (hh : IsSkewMat h) : symmPart (M + h) = symmPart M

theorem HCPolySupport.HighContrast.skewPart_add_isSkewMat {d : ℕ} {M h : Mat d} (hh : IsSkewMat h) : skewPart (M + h) = skewPart M + h

theorem HCPolySupport.HighContrast.centeredFlux_add_isSkewMat {d : ℕ} {A B h : Mat d} (hh : IsSkewMat h) (F G : Vec d) : matVecMul (A + h - skewPart (B + h)) F - matVecMul (symmPart (B + h)) G = matVecMul (A - skewPart B) F - matVecMul (symmPart B) G

The skew-centered flux difference is invariant under adding a constant antisymmetric matrix to the coefficient field and to the homogenized matrix.

theorem HCPolySupport.HighContrast.uncenteredFlux_add_isSkewMat {d : ℕ} (A B h : Mat d) (F G : Vec d) : matVecMul (A + h) F - matVecMul (B + h) G = matVecMul A F - matVecMul B G + matVecMul h (F - G)

The uncentered flux difference is NOT invariant: it moves by the constant antisymmetric matrix applied to the difference of the two gradients. This is the quantity that neither the shape datum nor the reference aspect ratio sees, and it is why the displays are written for the centered field.

The weak equation is fail-closed

theorem HCPolySupport.HighContrast.integral_weakPairing_eq_zero_of_not_integrableOn {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (F : Vec d → Vec d) (φ : Vec d → ℝ) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (F x))) V MeasureTheory.volume) : ∫ (x : Vec d) in V, vecDot (smoothGrad φ x) (matVecMul (b x) (F x)) = 0

The mechanism the weak equation used here closes: with a totalized Bochner pairing, a flux that pairs divergently against a test satisfies the printed identity at that test for no reason at all.

theorem HCPolySupport.HighContrast.integrableOn_of_isWeakSolutionOn {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {F : Vec d → Vec d} (h : IsWeakSolutionOn b V F) {φ : Vec d → ℝ} (hφ : IsLocalTest V φ) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (F x))) V MeasureTheory.volume

IsWeakSolutionOn excludes exactly that: it asserts absolute convergence at every test.

theorem HCPolySupport.HighContrast.isWeakSolutionOn_zero {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) : IsWeakSolutionOn b V fun (x : Vec d) => 0

The zero field solves the equation, so the class is nonempty.

The growth condition of the Liouville class is fail-closed

The Liouville clause is a double inclusion, so its class appears both as a hypothesis and as a conclusion and admits no junk in either direction. Under a totalized real average, a function whose square is not integrable on a ball is assigned normalized L² average 0 there, so the growth condition holds for it by the failure of the average; the class is junk-enlarged and the inclusion that classifies its members is false.

theorem HCPolySupport.HighContrast.sqrt_volumeAverage_sq_eq_zero_of_not_integrableOn {d : ℕ} (V : Set (Vec d)) (v : Vec d → ℝ) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => v x ^ 2) V MeasureTheory.volume) : √(volumeAverage V fun (x : Vec d) => v x ^ 2) = 0

The mechanism, for the growth condition.

theorem HCPolySupport.HighContrast.normalizedL2Norm_zero {d : ℕ} (V : Set (Vec d)) : (normalizedL2Norm V fun (x : Vec d) => 0) = 0

The normalized L² norm of the zero function is zero, so the growth condition is not vacuous in the other direction either.

The energies are fail-closed

theorem HCPolySupport.HighContrast.integral_sEnergy_eq_zero_of_not_integrableOn {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (F : Vec d → Vec d) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (F x) (matVecMul (symmPart (b x)) (F x))) V MeasureTheory.volume) : ∫ (x : Vec d) in V, vecDot (F x) (matVecMul (symmPart (b x)) (F x)) = 0

The mechanism for the weighted energies: under a totalized Bochner integral a divergent Dirichlet energy is valued at 0, making the H¹_s approximation conditions satisfiable by fields of infinite energy.

theorem HCPolySupport.HighContrast.sEnergyOn_eq_top_of_not_integrableOn {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (F : Vec d → Vec d) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => vecDot (F x) (matVecMul (symmPart (b x)) (F x))) (MeasureTheory.volume.restrict V)) (hnonneg : 0 ≤ᵐ[MeasureTheory.volume.restrict V] fun (x : Vec d) => vecDot (F x) (matVecMul (symmPart (b x)) (F x))) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (F x) (matVecMul (symmPart (b x)) (F x))) V MeasureTheory.volume) : sEnergyOn b V F = ⊤

sEnergyOn is the Lebesgue integral of the same nonnegative integrand, so it is infinite exactly where the energy is.

theorem HCPolySupport.HighContrast.sEnergyOn_zero {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) : (sEnergyOn b V fun (x : Vec d) => 0) = 0

The zero field has zero energy.

theorem HCPolySupport.HighContrast.h1sNormSqOn_zero {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) : (h1sNormSqOn b V (fun (x : Vec d) => 0) fun (x : Vec d) => 0) = 0

theorem HCPolySupport.HighContrast.skewFluxPairing_zero {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (φ : Vec d → ℝ) : skewFluxPairing b V (fun (x : Vec d) => 0) φ = 0

theorem HCPolySupport.HighContrast.skewFluxDualNorm_zero {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) : (skewFluxDualNorm b V fun (x : Vec d) => 0) = 0

theorem HCPolySupport.HighContrast.memH1a0_zero {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) : MemH1a0 b V (fun (x : Vec d) => 0) fun (x : Vec d) => 0

The H¹_{a,0} class is nonempty: the zero pair belongs to it. The Dirichlet clause is therefore not vacuous through the failure of its solution hypothesis.

The domain guard

Every volume-normalized quantity above divides by volume V, and on a null V each of them collapses to zero: the estimates would then hold by the collapse of both sides. The clause that carries a domain therefore binds a positive inner radius, and that single binder is what makes the domain nonempty, hence of positive volume.

theorem HCPolySupport.HighContrast.HasBallSandwich.nonempty {d : ℕ} {U : Set (Vec d)} {ρ Rad : ℝ} (h : HasBallSandwich U ρ Rad) : U.Nonempty

A ball sandwich makes the domain nonempty.