High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.C1ExactGaugeFrameConditional
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Conditional exact-frame C1 composition #
This module isolates the terminal estimate that remains subject to the gauge frame decision. Once that estimate is supplied for the exact normalized coefficient and canonical joint corrector, affine transport and finite-prefix absorption give the full physical-radius conclusion.
theorem
HCPolySupport.HighContrast.Root.exists_rangeCompletePhysicalC1_of_exactRootGaugeTerminal
{d : ℕ}
[NeZero d]
(L : ℕ)
(eta A : ℝ)
(heta : 0 ≤ eta)
(hA : 0 < A)
:
∃ (K : ℝ),
0 < K ∧ ∀ (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffSpace d) (x : ℝ),
1 ≤ x →
∀ (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d),
(∀ (c : ℝ) (e e' : Vec d),
gradPhi (c • e + e') a =ᵐ[MeasureTheory.volume] fun (y : Vec d) => c • gradPhi e a y + gradPhi e' a y) →
∀ (PhiRef : Vec d → NormalizedLocalH1Carrier d),
(∀ (e : Vec d),
(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 + (PhiRef (matVecMul (Selection.normalizedRoot (symmPart abar)) e)).globalGradientRepresentative
y) →
∀ (R : ℝ),
x ≤ R →
∀ (u : Vec d → ℝ) (Du : Vec d → Vec d),
MemH1a (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) u Du →
IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du →
(let q := Selection.normalizedRoot (symmPart abar);
have hq := ⋯;
have bRef := affineCoefficient q hq ↑↑(normalizedCenteredCoeff a abar hS);
have rStart := 3 ^ (Quenched.triadicCeilingIndex x + L);
rStart ≤ R →
∃ (eRef : Vec d),
∀ r ∈ Set.Icc rStart R,
(weightedGradNorm bRef {y : Vec d | vecNormSq y ≤ r ^ 2} fun (y : Vec d) =>
matVecMul q (Du (matVecMul q y)) - (eRef + (PhiRef eRef).globalGradientRepresentative y)) ≤ ENNReal.ofReal (A * (r / R) ^ max eta (1 / 2)) * weightedGradNorm bRef {y : Vec d | vecNormSq y ≤ R ^ 2} fun (y : Vec d) =>
matVecMul q (Du (matVecMul q y))) →
∃ (e : Vec d),
∀ r ∈ Set.Icc x R,
(weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) fun (y : Vec d) =>
Du y - (e + gradPhi e a y)) ≤ ENNReal.ofReal (K * (r / R) ^ eta) * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du
The exact gauge-frame terminal, affine return, and deterministic prefix compose to the physical C1 estimate on every radius above the root scale.