High-contrast homogenization: Provider.Regularity.FiniteAffineVaryingSlopeLimit

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

Varying-slope finite-corrector limits

Finite dimensionality of the slope space upgrades pointwise convergence of the finite corrector operators to convergence along any convergent sequence of slopes. No operator-norm estimate or inverse slope comparison is needed.

theorem HCPolySupport.HighContrast.memVectorL2_const_varyingSlope {d : ℕ} (e : Vec d) (q : ℕ) : MemVectorL2 (openCubeSet (originCube d ↑q)) fun (x : Vec d) => e

noncomputable def HCPolySupport.HighContrast.constantLocalGradientLinearMap (d q : ℕ) : Vec d →ₗ[ℝ] ↥(LocalGradientL2 d q)

The linear map embedding a slope as a constant L² gradient field on the local origin cube at scale q.

Equations

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

noncomputable def HCPolySupport.HighContrast.finiteAffineFullGradientLinearMap {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (q k : ℕ) : Vec d →ₗ[ℝ] ↥(LocalGradientL2 d q)

The linear map assigning a slope its constant gradient plus the normalized finite corrector gradient at scale q + k, on the cube at scale q.

Equations

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

noncomputable def HCPolySupport.HighContrast.jointAffineFullGradientLinearMap {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (q : ℕ) : Vec d →ₗ[ℝ] ↥(LocalGradientL2 d q)

The canonical affine-plus-joint-corrector gradient on a fixed cube as a linear map of the slope.

Equations

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

theorem HCPolySupport.HighContrast.localGradientRestrict_jointAffineFullGradientLinearMap {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) {q r : ℕ} (hqr : q ≤ r) (e : Vec d) : (localGradientRestrict hqr) ((jointAffineFullGradientLinearMap a hCauchy r) e) = (jointAffineFullGradientLinearMap a hCauchy q) e

Canonical full-gradient classes respect restriction between centered cubes.

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

The affine function of slope e plus the normalized finite corrector, realizing the full finite gradient on the local cube at scale q.

Equations

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

theorem HCPolySupport.HighContrast.finiteAffineFullGradientClass_eq_innerH1Gradient {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (q k : ℕ) : (have this := constantGradientOnOriginCube e ↑q; this) + (normalizedLocalPair (finiteAffineCorrectionLocalSequence a e) q k).2 = (finiteAffineSolutionInnerH1 a ↑q ↑(q + k) ⋯ e).gradToHilbertVectorL2

The linear-map presentation of a finite full-gradient class is exactly the gradient class of the finite affine solution restricted to the fixed inner cube.

theorem HCPolySupport.HighContrast.tendsto_linearMap_apply_of_forall_tendsto_of_tendsto {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℕ → Vec d →ₗ[ℝ] E) (L : Vec d →ₗ[ℝ] E) (hT : ∀ (e : Vec d), Filter.Tendsto (fun (k : ℕ) => (T k) e) Filter.atTop (nhds (L e))) (e : ℕ → Vec d) (eLim : Vec d) (he : Filter.Tendsto e Filter.atTop (nhds eLim)) : Filter.Tendsto (fun (k : ℕ) => (T k) (e k)) Filter.atTop (nhds (L eLim))

Pointwise convergence of linear maps out of the finite project-vector space permits simultaneous convergence of the input vectors.

theorem HCPolySupport.HighContrast.finiteAffineFullGradient_varyingSlope_tendsto_jointLocalGradient {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (q : ℕ) (e : ℕ → Vec d) (eLim : Vec d) (he : Filter.Tendsto e Filter.atTop (nhds eLim)) : Filter.Tendsto (fun (k : ℕ) => (have this := constantGradientOnOriginCube (e k) ↑q; this) + (normalizedLocalPair (finiteAffineCorrectionLocalSequence a (e k)) q k).2) Filter.atTop (nhds ((have this := constantGradientOnOriginCube eLim ↑q; this) + (finiteAffineCorrectionJointLocalLimit a hCauchy eLim).gradientComponent q))

On every fixed cube, finite affine full-gradient classes with convergent boundary slopes converge to the canonical affine-plus-corrector class at the limiting slope.

theorem HCPolySupport.HighContrast.finiteAffineSolutionInnerGradient_varyingSlope_tendsto_jointLocalGradient {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (q : ℕ) (e : ℕ → Vec d) (eLim : Vec d) (he : Filter.Tendsto e Filter.atTop (nhds eLim)) : Filter.Tendsto (fun (k : ℕ) => (finiteAffineSolutionInnerH1 a ↑q ↑(q + k) ⋯ (e k)).gradToHilbertVectorL2) Filter.atTop (nhds ((have this := constantGradientOnOriginCube eLim ↑q; this) + (finiteAffineCorrectionJointLocalLimit a hCauchy eLim).gradientComponent q))

Equivalent restricted-solution form of the varying-slope convergence theorem.

theorem HCPolySupport.HighContrast.finiteAffineSolutionInnerGradient_varyingSlope_tendsto_jointLocalGradient_along {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (q : ℕ) (rho : ℕ → ℕ) (hrho : Filter.Tendsto rho Filter.atTop Filter.atTop) (e : ℕ → Vec d) (eLim : Vec d) (he : Filter.Tendsto e Filter.atTop (nhds eLim)) : Filter.Tendsto (fun (k : ℕ) => (finiteAffineSolutionInnerH1 a ↑q ↑(q + rho k) ⋯ (e k)).gradToHilbertVectorL2) Filter.atTop (nhds ((have this := constantGradientOnOriginCube eLim ↑q; this) + (finiteAffineCorrectionJointLocalLimit a hCauchy eLim).gradientComponent q))

Cofinally reindexed form of the varying-slope restricted-solution convergence theorem.

theorem HCPolySupport.HighContrast.finiteAffineResidual_identifies_jointLocalGradient_along {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (q : ℕ) (rho : ℕ → ℕ) (hrho : Filter.Tendsto rho Filter.atTop Filter.atTop) (u : (k : ℕ) → Book.Ch03.CubeSolution (originCube d ↑(q + rho k)) a) (Dv : Vec d → Vec d) (huGrad : ∀ (k : ℕ), (u k).toH1.grad = Dv) (e : ℕ → Vec d) (eLim : Vec d) (he : Filter.Tendsto e Filter.atTop (nhds eLim)) (hresidual : Filter.Tendsto (fun (k : ℕ) => weightedGradNorm (a.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) fun (x : Vec d) => (u k).toH1.grad x - (finiteAffineSolution a (↑(q + rho k)) (e k)).toH1.grad x) Filter.atTop (nhds 0)) : (finiteCubeSolutionRestriction a ⋯ (u 0)).toH1.gradToHilbertVectorL2 = (jointAffineFullGradientLinearMap a hCauchy q) eLim

Cofinal outer-scale version of fixed-cube residual identification.