High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.C1FiniteCorrectorLimitBridge
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Fixed-cube finite-corrector limit bridge #
This file consumes the joint local-limit field of the available regularity assembly and exposes the exact full-gradient convergence needed by the coefficient-energy telescope.
noncomputable def
HCPolySupport.HighContrast.finiteAffineInnerGradientClass
{d : ℕ}
[NeZero d]
(a : Book.Ch02.TriadicCoeffFamily d)
(e : Vec d)
(q k : ℕ)
:
↥(LocalGradientL2 d q)
The finite affine full-gradient class on the fixed inner cube.
Equations
Instances For
theorem
HCPolySupport.HighContrast.finiteAffineSolutionInnerGradient_tendsto_of_jointLocalEquation
{d : ℕ}
[NeZero d]
(a : Book.Ch02.TriadicCoeffFamily d)
(Phi : Vec d → NormalizedLocalH1Carrier d)
(hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi)
(e : Vec d)
(q : ℕ)
:
Filter.Tendsto (fun (k : ℕ) => finiteAffineInnerGradientClass a e q k) Filter.atTop
(nhds
((have this := constantGradientOnOriginCube e ↑q;
this) + (Phi e).gradientComponent q))
The finite affine full gradients converge on every fixed cube to the full gradient of any joint local-limit family.
theorem
HCPolySupport.HighContrast.sqrt_jointLocalGradient_sub_finiteAffine_le_of_uniform_tail
{d : ℕ}
[NeZero d]
(a : Book.Ch02.TriadicCoeffFamily d)
(Phi : Vec d → NormalizedLocalH1Carrier d)
(hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi)
(e : Vec d)
(q k : ℕ)
(B : ℝ)
(htail :
∀ (m : ℕ),
k ≤ m →
√(normalizedLocalSymmetricEnergy ⋯
(finiteAffineInnerGradientClass a e q m - finiteAffineInnerGradientClass a e q k)) ≤ B)
:
√(normalizedLocalSymmetricEnergy ⋯
((have this := constantGradientOnOriginCube e ↑q;
this) + (Phi e).gradientComponent q - finiteAffineInnerGradientClass a e q k)) ≤ B
A uniform coefficient-energy tail for the finite full gradients passes to the joint local-limit full gradient.