High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessCubeSolutionData

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

the analytic inputs, parts (b) and (d): the observation family and the cube solution listed as

"absent" both the coefficient identification ∀ y, aHat (y + c) = (aFam.coeffOn (originCube d j)).toCoeffField y and the exhibition of the gauge solution as a DirichletForcedCubeSolution on the origin cube. Both are closed here.

• (d), the coefficient family. exists_affineCoeffFamily (HCPoly.Provider.PolynomialHomogenization.AffineCoeffFamily) produces a Chapter 3 family whose representative is, on every cube and literally, a prescribed affine pullback. Applied not to fun w ↦ scaledCoeff ε a w - skewPart abar (as the skew-centered scaled affine family does) but to its translate by the gauge centre fun w ↦ scaledCoeff ε a (w + z) - skewPart abar, it gives a family for which the required identification is a pointwise equality, discharged by the single gauge identity matVecMul S (y + S⁻¹ z) = matVecMul S y + z. The a.e. identification that the module consumes as hObsEps falls out of the same pointwise equality, so one family serves both binders — which is exactly what that module needs, since hb and hObs there speak about the same aFam.

• (b), the cube solution. IsWeakSolutionOn.untranslate (HCPoly.Provider.Regularity.ObservationCoefficientTransport) moves the gauge weak solution (row 4′, module that module) from matImage S⁻¹ U = translateSet c (openCubeSet Q) onto the cube; the pointwise hb rewrites its coefficient into (aFam.coeffOn Q).toCoeffField; the upstream private isForcedEquation_zero_of_isWeakSolutionOn' is re-proved in-module; and E15's witnessDirichletForcedCubeSolution packages the result. The construction keeps v.toH1 = uObs and dirichletBoundaryGradientField v = gObs.grad definitionally, so the hu premise and hF are identities read backwards.

  The one remaining hypothesis is the zero-trace datum hzero; it is a binder here, and it is the last of the analytic inputs.

The gauge cancellation

theorem HCPolySupport.HighContrast.RowSupply.matVecMul_matVecMul_nonsing_inv {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) (w : Vec d) : matVecMul L (matVecMul L⁻¹ w) = w

An invertible gauge composed with its inverse is the identity on vectors.

(d) The translated observation family

theorem HCPolySupport.HighContrast.RowSupply.exists_translatedSkewCenteredScaledAffineCoeffFamily {d : ℕ} {epsilon : ℝ} (hepsilon : 0 < epsilon) (a : CoeffSpace d) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (z : Vec d) : ∃ (aFam : Book.Ch03.CoeffFamily d), ∀ (Q : TriadicCube d), (aFam.coeffOn Q).toCoeffField = affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (w : Vec d) => scaledCoeff epsilon a (w + z) - skewPart abar

The skew-centred rescaled coefficient, translated by the gauge centre, is a Chapter 3 coefficient family with its displayed representative on every cube.

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessCoeffFamilyAtCube {d : ℕ} {epsilon : ℝ} (hepsilon : 0 < epsilon) (a : CoeffSpace d) {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (z : Vec d) (j : ℤ) : ∃ (aFam : Book.Ch03.CoeffFamily d), (∀ (y : Vec d), affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (w : Vec d) => scaledCoeff epsilon a w - skewPart abar) (y + matVecMul (matSqrt (symmPart abar))⁻¹ z) = (aFam.coeffOn (originCube d j)).toCoeffField y) ∧ (aFam.coeffOn (originCube d j)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (originCube d j))] fun (y : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (w : Vec d) => scaledCoeff epsilon a w - skewPart abar) (y + matVecMul (matSqrt (symmPart abar))⁻¹ z)

the analytic inputs (d), closed. One Chapter 3 family serves both of coefficient binders at the frozen witness: the pointwise hb and the a.e. observation identification hObs, at scaledCoeff ε a.

(b) The forced equation and the cube solution

theorem HCPolySupport.HighContrast.RowSupply.isForcedEquation_zero_of_isWeakSolutionOn {d : ℕ} {Q : TriadicCube d} {aFam : Book.Ch03.CoeffFamily d} (u : H1Function (Book.Ch02.cubeDomain Q).carrier) (hu : IsWeakSolutionOn (aFam.coeffOn Q).toCoeffField (Book.Ch02.cubeDomain Q).carrier u.grad) : Book.Ch03.IsForcedEquation Q aFam u 0

The upstream private conversion of a cube weak solution into a forced equation, re-proved in-module so it can be used at the frozen witness.

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessDirichletCubeSolution {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (y : Vec d) => z + matVecMul (matSqrt (symmPart abar)) y) '' openCubeSet (originCube d j)) {aHat : CoeffField d} {aFam : Book.Ch03.CoeffFamily d} (hb : ∀ (y : Vec d), aHat (y + matVecMul (matSqrt (symmPart abar))⁻¹ z) = (aFam.coeffOn (originCube d j)).toCoeffField y) (F : Vec d → Vec d) (hWeak : IsWeakSolutionOn aHat (matImage (matSqrt (symmPart abar))⁻¹ U) F) (uObs gObs : H1Function (openCubeSet (originCube d j))) (huObs : ∀ (y : Vec d), uObs.grad y = F (y + matVecMul (matSqrt (symmPart abar))⁻¹ z)) (hzero : ∃ (w : H10Function (openCubeSet (originCube d j))), w.toFun =ᵐ[volumeMeasureOn (openCubeSet (originCube d j))] fun (x : Vec d) => uObs.toFun x - gObs.toFun x) : ∃ (v : Book.Ch03.DirichletForcedCubeSolution (originCube d j) aFam 0), v.toH1 = uObs ∧ Book.Ch03.dirichletBoundaryGradientField v = gObs.grad

the analytic inputs (b), closed modulo the zero-trace datum. The gauge solution of the frozen witness is a Dirichlet forced cube solution on the origin cube of the witness generation, with the prescribed boundary datum.