High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.C1ExactGaugeFrameTransport
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Exact gauge-frame transport for the C1 estimate #
The normalized-root frame uses the exact centered coefficient and the canonical joint corrector. An estimate in that frame returns to the physical ellipsoids without introducing a rounded coefficient family.
theorem
HCPolySupport.HighContrast.Root.c1DecayBound_weaken_exponent
(A eta etaFast r R : ℝ)
(hA : 0 ≤ A)
(hr : 0 < r)
(hR : 0 < R)
(hrR : r ≤ R)
(heta : eta ≤ etaFast)
{X Y : ENNReal}
(hbound : X ≤ ENNReal.ofReal (A * (r / R) ^ etaFast) * Y)
:
A decay estimate at a larger exponent implies the same estimate at a smaller exponent on a nested-radius interval.
theorem
HCPolySupport.HighContrast.Root.delayedPhysicalC1_of_exactRootGaugeFrame
{d : ℕ}
[NeZero d]
{abar : Mat d}
(hS : Matrix.PosDef (symmPart abar))
(a : CoeffSpace d)
(gradPhi : Vec d → CoeffSpace d → Vec d → Vec d)
(PhiRef : Vec d → NormalizedLocalH1Carrier d)
(hpullback :
∀ (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)
(L : ℕ)
(eta A x R : ℝ)
(Du : Vec d → Vec d)
:
(have rStart := 3 ^ (Quenched.triadicCeilingIndex x + L);
rStart ≤ R) →
(let q := Selection.normalizedRoot (symmPart abar);
have hq := ⋯;
have bRef := affineCoefficient q hq ↑↑(normalizedCenteredCoeff a abar hS);
have rStart := 3 ^ (Quenched.triadicCeilingIndex x + L);
∃ (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) ^ eta) * 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 (3 ^ (Quenched.triadicCeilingIndex x + L)) R,
(weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar r) fun (y : Vec d) => Du y - (e + gradPhi e a y)) ≤ ENNReal.ofReal (A * (r / R) ^ eta) * weightedGradNorm (fun (y : Vec d) => ↑↑a y) (ellipsoid abar R) Du
A delayed C1 estimate for the exact normalized coefficient and canonical joint corrector transports to the same delayed estimate on physical ellipsoids.