High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Duality.GaugeWitnessPremiseTransport

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

Transporting the two PDE premises to the gauge image

The Seam-2 consumer states the duality clause at the gauge image, but the two PDE hypotheses of the printed lemma — u − v ∈ H₀^{1−s}(U) and ∇·(a∇u − a₁∇v) = 0 — are supplied one level up, at the physical domain (ScheduledLocalizationRowSupply). This file carries both across the gauge.

• the zero-trace potential half moves covariantly, by the H¹₀ affine pullback;
• the solenoidal half moves through the affine transport of the weak equation, after the constant skew part of the comparison matrix is annihilated: the gauge image of that skew part is again a constant skew matrix, and a constant skew matrix applied to a weak gradient is solenoidal.

Matrix preliminaries

theorem HCPolySupport.HighContrast.RowSupply.matTranspose_matSqrt {d : ℕ} {A : Mat d} (hA : Matrix.PosDef A) : matTranspose (matSqrt A) = matSqrt A

The matrix square root of a positive definite matrix is symmetric.

theorem HCPolySupport.HighContrast.RowSupply.matTranspose_inv_of_symm {d : ℕ} {L : Mat d} (hLsymm : matTranspose L = L) : matTranspose L⁻¹ = L⁻¹

The inverse of a symmetric invertible matrix is symmetric.

theorem HCPolySupport.HighContrast.RowSupply.isSkewMat_conj {d : ℕ} {M K : Mat d} (hMsymm : matTranspose M = M) (hK : IsSkewMat K) : IsSkewMat (M * K * M)

A symmetric conjugation of a skew matrix is skew.

theorem HCPolySupport.HighContrast.RowSupply.symmPart_add_skewPart' {d : ℕ} (A : Mat d) : A = symmPart A + skewPart A

The matrix decomposition into symmetric and skew parts.

theorem HCPolySupport.HighContrast.RowSupply.gaugeConj_symmPart_eq_one {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : (matSqrt (symmPart abar))⁻¹ * symmPart abar * matTranspose (matSqrt (symmPart abar))⁻¹ = 1

The gauge conjugation normalizes the symmetric part to the identity.

theorem HCPolySupport.HighContrast.RowSupply.affineCoefficient_sub {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) (a b : CoeffField d) (y : Vec d) : affineCoefficient L hL (fun (x : Vec d) => a x - b x) y = affineCoefficient L hL a y - affineCoefficient L hL b y

The affine coefficient transform is additive on differences.

Solenoidal algebra

theorem HCPolySupport.HighContrast.RowSupply.isSolenoidalOn_sub {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hfL2 : MemVectorL2 U f) (hgL2 : MemVectorL2 U g) (hf : IsSolenoidalOn U f) (hg : IsSolenoidalOn U g) : IsSolenoidalOn U fun (x : Vec d) => f x - g x

Solenoidal fields are closed under differences.

theorem HCPolySupport.HighContrast.RowSupply.isSolenoidalOn_of_isWeakSolutionOn {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (b : CoeffField d) {F : Vec d → Vec d} (hbF : MemVectorL2 U fun (x : Vec d) => matVecMul (b x) (F x)) (hweak : IsWeakSolutionOn b U F) : IsSolenoidalOn U fun (x : Vec d) => matVecMul (b x) (F x)

A compact-test weak equation upgrades to solenoidality of its flux once the flux is square integrable.

The two transports

theorem HCPolySupport.HighContrast.RowSupply.isPotentialZeroTraceOn_gaugeGradSub {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (hLsymm : matTranspose L = L) {U : Set (Vec d)} (hU : MeasurableSet U) (u h : H1Function U) (haff : MemAffineH10 U h u) (uHat hHat : H1Function (matImage L⁻¹ U)) (huHat : uHat.grad = fun (y : Vec d) => matVecMul L (u.grad (matVecMul L y))) (hhHat : hHat.grad = fun (y : Vec d) => matVecMul L (h.grad (matVecMul L y))) : IsPotentialZeroTraceOn (matImage L⁻¹ U) fun (y : Vec d) => uHat.grad y - hHat.grad y

The zero-trace potential premise, transported to the gauge image. The printed hypothesis u − v ∈ H₀^{1−s}(U) is supplied at the physical domain; its gauge image is the zero-trace potential the duality reduction consumes.

theorem HCPolySupport.HighContrast.RowSupply.isSolenoidalOn_gaugeFluxDefect {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} (hU : MeasurableSet U) (hVopen : IsOpen (matImage (matSqrt (symmPart abar))⁻¹ U)) (aPhysical : CoeffField d) (u h : H1Function U) (huPhys : IsWeakSolutionOn aPhysical U u.grad) (hhPhys : IsWeakSolutionOn (fun (x : Vec d) => abar) U h.grad) (uHat hHat : H1Function (matImage (matSqrt (symmPart abar))⁻¹ U)) (huHat : uHat.grad = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (u.grad (matVecMul (matSqrt (symmPart abar)) y))) (hhHat : hHat.grad = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (h.grad (matVecMul (matSqrt (symmPart abar)) y))) {aHat : CoeffField d} (haHat : aHat = affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (x : Vec d) => aPhysical x - skewPart abar) (hFdefect : MemVectorL2 (matImage (matSqrt (symmPart abar))⁻¹ U) fun (y : Vec d) => matVecMul (aHat y - 1) (uHat.grad y)) : IsSolenoidalOn (matImage (matSqrt (symmPart abar))⁻¹ U) fun (y : Vec d) => matVecMul (aHat y) (uHat.grad y) - hHat.grad y

The solenoidal premise, transported to the gauge image. The printed hypothesis ∇·(a∇u − a₁∇v) = 0 is supplied at the physical domain as two weak equations; after the constant skew part is annihilated, its gauge image is the solenoidality the duality reduction consumes.