Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.FiniteCorrectorLocalSequence

High-contrast homogenization: Provider.Regularity.FiniteCorrectorLocalSequence #

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

Finite-corrector local sequences #

The zero-trace parts of the selected affine Dirichlet solutions form an unshifted sequence on the centered cube exhaustion. This module records the almost-everywhere linearity needed to pass that sequence to local limits.

source
theorem HCPolySupport.HighContrast.finiteAffineCorrection_toFun_add_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e e' : Vec d) :
(finiteAffineCorrection a m (e + e')).toFun =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] fun (x : Vec d) => (finiteAffineCorrection a m e).toFun x + (finiteAffineCorrection a m e').toFun x

The finite zero-trace correction is additive in its slope almost everywhere.

source
theorem HCPolySupport.HighContrast.finiteAffineCorrection_toFun_smul_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (c : ℝ) (e : Vec d) :
(finiteAffineCorrection a m (c • e)).toFun =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] fun (x : Vec d) => c * (finiteAffineCorrection a m e).toFun x

The finite zero-trace correction is homogeneous in its slope almost everywhere.

source
theorem HCPolySupport.HighContrast.finiteAffineCorrection_grad_add_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (e e' : Vec d) :
(finiteAffineCorrection a m (e + e')).grad =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] fun (x : Vec d) => (finiteAffineCorrection a m e).grad x + (finiteAffineCorrection a m e').grad x

The weak gradient of the finite zero-trace correction is additive in its slope almost everywhere.

source
theorem HCPolySupport.HighContrast.finiteAffineCorrection_grad_smul_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (c : ℝ) (e : Vec d) :
(finiteAffineCorrection a m (c • e)).grad =ᵐ[volumeMeasureOn (Book.Ch02.cubeDomain (originCube d m)).carrier] fun (x : Vec d) => c • (finiteAffineCorrection a m e).grad x

The weak gradient of the finite zero-trace correction is homogeneous in its slope almost everywhere.

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

The unshifted finite zero-trace corrections on the centered cube exhaustion.

Equations
Instances For