High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.ExactRootPullback

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

The exact-root affine pullback

The terminal cube solution exists only for the base-rounded family: its coefficient-corrector-family premise does not accept the exact-root aRef. The obstruction is not analytic: the chain

isWeakSolutionOn_add_constSkew_iff → isWeakSolutionOn_smul_coefficient_iff
                                  → isWeakSolutionOn_affinePullback_iff

is entirely generic in the pullback matrix, and the rounded modules merely instantiate it at baseRoundedGrid (symmPart abar). This module instantiates the same chain at Selection.normalizedRoot (symmPart abar) — the exact root — and identifies the resulting coefficient with the large-scale C¹ slope approximation terminal's bRef.

Two facts make the exact-root instance no harder than the rounded one:

• the exact root is symmetric, because it is a positive scalar multiple of matSqrt, so the transpose in the general affine chain rule disappears exactly as it does for the rounded grid;
• the scalar normalizer specBound ((symmPart abar)⁻¹) is the same one normalizedCenteredCoeff applies, so the pulled-back coefficient is almost everywhere affineCoefficient (Selection.normalizedRoot (symmPart abar)) _ ⇑(normalizedCenteredCoeff a abar hS).1, which is literally the terminal's bRef.

Nothing here is an estimate.

The exact root as a pullback matrix

theorem HCPolySupport.HighContrast.CorrectorComposition.isUnit_det_exactRoot {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) : IsUnit (Matrix.det (Selection.normalizedRoot (symmPart abar)))

The exact normalized root is invertible on a positive-definite symmetric part.

theorem HCPolySupport.HighContrast.CorrectorComposition.matTranspose_exactRoot {d : ℕ} (m : Mat d) : matTranspose (Selection.normalizedRoot m) = Selection.normalizedRoot m

The exact normalized root is symmetric: it is a positive scalar multiple of the symmetric square root.

The H¹ pullback

noncomputable def HCPolySupport.HighContrast.CorrectorComposition.exactRootH1Pullback {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} (hU : MeasurableSet U) (u : H1Function U) : H1Function (matImage (Selection.normalizedRoot (symmPart abar))⁻¹ U)

Pull back an H¹ representative by the exact normalized root.

Equations

• HCPolySupport.HighContrast.CorrectorComposition.exactRootH1Pullback abar hS hU u = Classical.choose ⋯

theorem HCPolySupport.HighContrast.CorrectorComposition.exactRootH1Pullback_grad {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} (hU : MeasurableSet U) (u : H1Function U) : (exactRootH1Pullback abar hS hU u).grad = fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (u.grad (matVecMul (Selection.normalizedRoot (symmPart abar)) y))

Symmetry of the exact root turns the general transpose chain rule into the exact-root gradient action.

The exact-root centered coefficient

noncomputable def HCPolySupport.HighContrast.CorrectorComposition.exactRootCenteredCoefficient {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffField d) : CoeffField d

The exact-root analogue of roundedCenteredCoefficient: skew recentering, scalar normalization, exact-root pullback.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.CorrectorComposition.exactRootCenteredCoefficient_ae {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) : exactRootCenteredCoefficient abar hS ↑↑a =ᵐ[MeasureTheory.volume] affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)

The exact-root centered coefficient is the large-scale C¹ slope approximation terminal's bRef, almost everywhere. The scalar normalizer is exactly the one normalizedCenteredCoeff applies, so no factor survives.

The weak-solution transfer

theorem HCPolySupport.HighContrast.CorrectorComposition.isWeakSolutionOn_exactRootCenteredPullback_iff {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} (hU : IsOpen U) (a : CoeffField d) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemScalarL2 U u) (hDu : ∀ (i : Fin d), MemScalarL2 U fun (x : Vec d) => Du x i) (hweak : HasWeakGradientOn U u Du) : IsWeakSolutionOn a U Du ↔ IsWeakSolutionOn (exactRootCenteredCoefficient abar hS a) (matImage (Selection.normalizedRoot (symmPart abar))⁻¹ U) fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (Du (matVecMul (Selection.normalizedRoot (symmPart abar)) y))

A physical weak solution is equivalent to its exact-root, skew-centered, scalar-normalized affine pullback. This is the rounded centered-pullback equivalence with baseRoundedGrid replaced by the exact root; every step of the proof is generic in the matrix.