High-contrast homogenization: Provider.Regularity.CorrectorLocalEquation

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

Local equations for the joint corrector limit

On each fixed centered cube, the finite affine solutions form a sequence in the closed Hilbert space of coefficient-harmonic gradients. The normalized local limit therefore has a coefficient-harmonic affine-plus-corrector representative on that cube. The Cauchy premise remains explicit here.

noncomputable def HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalH1 {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (n : ℕ) : H1Function (localGradientCube d n)

The local affine-plus-corrector H¹ representative selected by the joint projective limit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalH1_gradToHilbertVectorL2 {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (n : ℕ) : (finiteAffineCorrectionJointLocalH1 a hCauchy e n).gradToHilbertVectorL2 = (have this := id (finiteAffineBoundaryH1 (↑n) e).gradToHilbertVectorL2; this) + (finiteAffineCorrectionJointLocalLimit a hCauchy e).gradientComponent n

The gradient class of the local full solution is the constant affine gradient plus the stored corrector-gradient component.

noncomputable def HCPolySupport.HighContrast.finiteAffineNormalizedLocalFullH1 {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (n k : ℕ) : H1Function (localGradientCube d n)

Add the affine boundary datum to the normalized local correction on localGradientCube d n.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.finiteAffineNormalizedLocalFullH1_grad_eq {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (n k : ℕ) : (finiteAffineNormalizedLocalFullH1 a e n k).grad = (finiteCubeSolutionRestriction a ⋯ (finiteAffineCubeSolution a (↑(n + k)) e)).toH1.grad

noncomputable def HCPolySupport.HighContrast.finiteAffineNormalizedLocalCubeSolution {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (n k : ℕ) : Book.Ch03.CubeSolution (originCube d ↑n) a

The normalized finite affine field packaged as an a-harmonic solution on originCube d n.

Equations

• HCPolySupport.HighContrast.finiteAffineNormalizedLocalCubeSolution a e n k = { toH1 := HCPolySupport.HighContrast.finiteAffineNormalizedLocalFullH1 a e n k, isHarmonic := ⋯ }

theorem HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalH1_isHarmonic {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (n : ℕ) : IsAHarmonicGradient (a.coeffOn (originCube d ↑n)).toCoeffField (localGradientCube d n) (finiteAffineCorrectionJointLocalH1 a hCauchy e n).grad

On every fixed cube, the local affine-plus-corrector representative has the public compatible coefficient as its harmonic coefficient.

noncomputable def HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalCubeSolution {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (n : ℕ) : Book.Ch03.CubeSolution (originCube d ↑n) a

The fixed-cube affine-plus-corrector limit as the homogeneous cube solution carrier.

Equations

• HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalCubeSolution a hCauchy e n = { toH1 := HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalH1 a hCauchy e n, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalCubeSolution_toH1 {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (n : ℕ) : (finiteAffineCorrectionJointLocalCubeSolution a hCauchy e n).toH1 = finiteAffineCorrectionJointLocalH1 a hCauchy e n

The local cube-solution wrapper retains the selected H¹ representative definitionally.