High-contrast homogenization: Provider.Regularity.RoundedHarmonicReplacement #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Harmonic replacement for the rounded constant reference #
This module constructs the same-trace constant-coefficient comparison used in the rounded regularity development. The comparison coefficient is the genuinely rounded near-identity matrix, not the scalar identity.
theorem
HCPolySupport.HighContrast.isForcedEquation_zero_of_isWeakSolutionOn
{d : ℕ}
{Q : TriadicCube d}
{a : Book.Ch03.CoeffFamily d}
(u : H1Function (Book.Ch02.cubeDomain Q).carrier)
(hu : IsWeakSolutionOn (a.coeffOn Q).toCoeffField (Book.Ch02.cubeDomain Q).carrier u.grad)
:
Book.Ch03.IsForcedEquation Q a u 0
A smooth-test high-contrast weak solution supplies the Chapter 3 zero-force weak equation on the same cube.
theorem
HCPolySupport.HighContrast.exists_constantCoeffCoarseGrainingComparisonDatum_of_hcWeakSolution
{d : ℕ}
{Q : TriadicCube d}
{a : Book.Ch03.CoeffFamily d}
(a0 : Book.Ch03.ConstantCoeffMatrix d)
(u : H1Function (Book.Ch02.cubeDomain Q).carrier)
(hu : IsWeakSolutionOn (a.coeffOn Q).toCoeffField (Book.Ch02.cubeDomain Q).carrier u.grad)
:
∃ (W : Book.Ch03.CoarseGrainingComparisonDatum Q a a0 0), W.u = u
Any symmetric uniformly elliptic constant matrix admits a same-trace homogeneous comparison for a high-contrast weak solution on an open cube.
noncomputable def
HCPolySupport.HighContrast.roundedHarmonicReplacementDatum
{d : ℕ}
[NeZero d]
(abar : Mat d)
(hS : Matrix.PosDef (symmPart abar))
(a : Book.Ch03.CoeffFamily d)
(m : ℤ)
(u : H1Function (Book.Ch02.cubeDomain (originCube d m)).carrier)
(hu : IsWeakSolutionOn (a.coeffOn (originCube d m)).toCoeffField (Book.Ch02.cubeDomain (originCube d m)).carrier u.grad)
:
Book.Ch03.CoarseGrainingComparisonDatum (originCube d m) a (roundedReferenceConstantCoeffMatrix abar hS) 0
The chosen same-trace replacement for the rounded near-identity comparison matrix.
Equations
- HCPolySupport.HighContrast.roundedHarmonicReplacementDatum abar hS a m u hu = Classical.choose ⋯