High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.GaugeRepresentativeJoin

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

theorem HCPolySupport.HighContrast.rawIdentityFamily_aeeq {d : ℕ} [NeZero d] {a : CoeffSpace d} {abar : Mat d} (geom : RoundedGenerationAnalyticGeometry d) (hS : Matrix.PosDef (symmPart abar)) (aRaw : Book.Ch03.CoeffFamily d) (hRaw : ∀ (Q : TriadicCube d), (aRaw.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d) (hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS))) : Book.Ch02.TriadicCoeffFamily.AEEq aRaw aIdentity

The raw exact-root family retained by the canonical physical corrector and the sanitized identity-gauge response family are a.e. the same family.

theorem HCPolySupport.HighContrast.rawIdentityCoeff_ae_global {d : ℕ} [NeZero d] {a : CoeffSpace d} {abar : Mat d} (geom : RoundedGenerationAnalyticGeometry d) (hS : Matrix.PosDef (symmPart abar)) (aRaw : Book.Ch03.CoeffFamily d) (hRaw : ∀ (Q : TriadicCube d), (aRaw.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d) (hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS))) (Q : TriadicCube d) : (aRaw.coeffOn Q).toCoeffField =ᵐ[MeasureTheory.volume] (aIdentity.coeffOn Q).toCoeffField

On a fixed cube, the preceding two coefficient representatives agree globally, not merely after restriction to the cube. This stronger form is what composes with the global affine pullback identities.

theorem HCPolySupport.HighContrast.physicalPair_le_identityGaugePair {d : ℕ} [NeZero d] {a : CoeffSpace d} {abar : Mat d} (geom : RoundedGenerationAnalyticGeometry d) (hS : Matrix.PosDef (symmPart abar)) (aRaw : Book.Ch03.CoeffFamily d) (hRaw : ∀ (Q : TriadicCube d), (aRaw.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) (hCauchy : FiniteAffineCorrectionLocalCauchy aRaw) (hRawJoint : IsFiniteAffineCorrectionJointLocalEquation aRaw (finiteAffineCorrectionJointLocalLimit aRaw hCauchy)) (hI : Matrix.PosDef (symmPart 1)) (aIdentity : Book.Ch03.CoeffFamily d) (hIdentity : ∀ (Q : TriadicCube d), (aIdentity.coeffOn Q).toCoeffField = ↑↑(geom.centeredCoeffSpace 1 hI (exactGaugeCoeffSpace a abar hS))) (PhiIdentity : Vec d → NormalizedLocalH1Carrier d) (hIdentityJoint : IsFiniteAffineCorrectionJointLocalEquation aIdentity PhiIdentity) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d) (e : Vec d) (hpullback : (fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (e + gradPhi e a (matVecMul (Selection.normalizedRoot (symmPart abar)) y))) =ᵐ[MeasureTheory.volume] fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) e + (finiteAffineCorrectionJointLocalLimit aRaw hCauchy (matVecMul (Selection.normalizedRoot (symmPart abar)) e)).globalGradientRepresentative y) {r : ℝ} (hr : 0 < r) (m : ℤ) (hm : m = outerTriadicGeneration (4 * r) ⋯) : ((ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) fun (x : Vec d) => matVecMul (matSqrt (symmPart abar)) (gradPhi e a x)) + ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) fun (x : Vec d) => matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (↑↑a x - skewPart abar) (e + gradPhi e a x) - matVecMul (symmPart abar) e)) ≤ ENNReal.ofReal (√(h1AffineFactor (Selection.normalizedRoot (symmPart abar))) * closedBallScaledNegOneConstant d) * (triadicScaledNegOneNorm m (correctorGradientOnOriginCube PhiIdentity (matVecMul (matSqrt (symmPart abar)) e) m) + triadicScaledNegOneNorm m (scalarIdentityCorrectorFluxDefectOnOriginCube aIdentity PhiIdentity (matVecMul (matSqrt (symmPart abar)) e) m))

Exact gauge transport, plus a.e.-invariance of the finite-corrector limit, feeds the physical inverse-radius pair into the identity-gauge quotient pair. No equality of bundled coefficient-family records is assumed.