High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessPhysicalRealization

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

The composed row u/huGrad/haff/huPhys

This is the row whose producer, exists_h1Function_memAffineH10_of_memH1a0, needs an AEUniformlyEllipticField witness for scaledCoeff ε a that "exists only as a private helper from the modules named above and must be re-proved".

It is re-proved here, from two public lemmas of HCPoly.Analytic.ScaledCoeff — aestronglyMeasurable_scaledCoeff and isAELocallyUniformlyElliptic_scaledCoeff — so the row composes with no new mathematics, exactly as predicted.

The physical domain's convexity, which that module does not state, is recovered from the gauge domain's: Uphys = matImage (matSqrt (symmPart abar)) Uhat and isOpenBoundedConvexDomain_matImage.

theorem HCPolySupport.HighContrast.RowSupply.exists_scaledCoeff_sourceField {d : ℕ} {ε : ℝ} (hε : 0 < ε) (a : CoeffSpace d) : ∃ (aε : Source.AKL.Field d), AEUniformlyEllipticField aε ∧ ↑aε =ᵐ[MeasureTheory.volume] scaledCoeff ε a

The scaled representative defines a source field with the same local ellipticity data.

theorem HCPolySupport.HighContrast.RowSupply.frozenWitness_physicalDomain_isOpenBoundedConvexDomain {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) : IsOpenBoundedConvexDomain U

The physical frozen witness domain is a bounded open convex domain.

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessPhysicalRealization {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {epsilon : ℝ} {a : CoeffSpace d} (hepsilon : 0 < epsilon) (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (g₀ h : H1Function U) (hgh : MemAffineH10 U g₀ h) (uFun : Vec d → ℝ) (uGrad : Vec d → Vec d) (hu0 : MemH1a0 (scaledCoeff epsilon a) U (fun (x : Vec d) => uFun x - g₀.toFun x) fun (x : Vec d) => uGrad x - g₀.grad x) (hweak : IsWeakSolutionOn (scaledCoeff epsilon a) U uGrad) : ∃ (u : H1Function U), u.toFun = uFun ∧ u.grad = uGrad ∧ MemAffineH10 U h u ∧ IsWeakSolutionOn (scaledCoeff epsilon a) U u.grad

Row u/huGrad/haff/huPhys. The frozen clause's MemH1a0 datum is realized as an H1Function on the physical witness domain, with the frozen affine boundary relation and the frozen weak-solution property transported to it.