High-contrast homogenization: Provider.Regularity.CorrectorLocalSequenceAlgebra

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

Local class algebra for finite correctors

Restriction and fixed-unit normalization act linearly on scalar and Hilbert-vector L² classes. Consequently the normalized local pairs of the finite zero-trace correctors are linear in the boundary slope. No equality of raw H1Function representatives is asserted.

theorem HCPolySupport.HighContrast.localValueRestrict_toScalarL2_restrictLocalH1 {d m n : ℕ} (hmn : m ≤ n) (u : H1Function (localGradientCube d n)) : (localValueRestrict hmn) u.toScalarL2 = (restrictLocalH1 hmn u).toScalarL2

Restricting an H¹ function and restricting its scalar L² class give the same local class.

theorem HCPolySupport.HighContrast.localGradientRestrict_gradToHilbertVectorL2_restrictLocalH1 {d m n : ℕ} (hmn : m ≤ n) (u : H1Function (localGradientCube d n)) : (localGradientRestrict hmn) u.gradToHilbertVectorL2 = (restrictLocalH1 hmn u).gradToHilbertVectorL2

Restricting an H¹ function and restricting its Hilbert-vector gradient class give the same local class.

theorem HCPolySupport.HighContrast.localValueRestrict_oneScalarL2_eq {d m n : ℕ} (hmn : m ≤ n) : (localValueRestrict hmn) oneScalarL2 = oneScalarL2

Scalar restriction preserves the constant-one class.

theorem HCPolySupport.HighContrast.normalizeOnUnitCube_toScalarL2_eq {d n : ℕ} (u : H1Function (localGradientCube d n)) : (normalizeOnUnitCube u).toScalarL2 = u.toScalarL2 - integralAverageCLM ((localValueRestrict ⋯) u.toScalarL2) • oneScalarL2

Fixed-unit normalization is a linear formula on scalar local classes.

theorem HCPolySupport.HighContrast.normalizeOnUnitCube_gradToHilbertVectorL2_eq {d n : ℕ} (u : H1Function (localGradientCube d n)) : (normalizeOnUnitCube u).gradToHilbertVectorL2 = u.gradToHilbertVectorL2

Fixed-unit normalization leaves the Hilbert-vector gradient class unchanged.

theorem HCPolySupport.HighContrast.normalizedLocalPair_value_eq {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (n k : ℕ) : (normalizedLocalPair u n k).1 = (localValueRestrict ⋯) (u (n + k)).toScalarL2 - integralAverageCLM ((localValueRestrict ⋯) (u (n + k)).toScalarL2) • oneScalarL2

The value component of a normalized local pair is the corresponding restricted class with its fixed-unit average removed.

theorem HCPolySupport.HighContrast.normalizedLocalPair_gradient_eq {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (n k : ℕ) : (normalizedLocalPair u n k).2 = (localGradientRestrict ⋯) (u (n + k)).gradToHilbertVectorL2

The gradient component of a normalized local pair is the restricted Hilbert-vector gradient class.

theorem HCPolySupport.HighContrast.finiteAffineCorrectionLocalSequence_toScalarL2_add {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e e' : Vec d) (q : ℕ) : (finiteAffineCorrectionLocalSequence a (e + e') q).toScalarL2 = (finiteAffineCorrectionLocalSequence a e q).toScalarL2 + (finiteAffineCorrectionLocalSequence a e' q).toScalarL2

Scalar local classes of finite correctors are additive in the slope.

theorem HCPolySupport.HighContrast.finiteAffineCorrectionLocalSequence_toScalarL2_smul {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (c : ℝ) (e : Vec d) (q : ℕ) : (finiteAffineCorrectionLocalSequence a (c • e) q).toScalarL2 = c • (finiteAffineCorrectionLocalSequence a e q).toScalarL2

Scalar local classes of finite correctors are homogeneous in the slope.

theorem HCPolySupport.HighContrast.finiteAffineCorrectionLocalSequence_gradient_add {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e e' : Vec d) (q : ℕ) : (finiteAffineCorrectionLocalSequence a (e + e') q).gradToHilbertVectorL2 = (finiteAffineCorrectionLocalSequence a e q).gradToHilbertVectorL2 + (finiteAffineCorrectionLocalSequence a e' q).gradToHilbertVectorL2

Hilbert-vector gradient classes of finite correctors are additive in the slope.

theorem HCPolySupport.HighContrast.finiteAffineCorrectionLocalSequence_gradient_smul {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (c : ℝ) (e : Vec d) (q : ℕ) : (finiteAffineCorrectionLocalSequence a (c • e) q).gradToHilbertVectorL2 = c • (finiteAffineCorrectionLocalSequence a e q).gradToHilbertVectorL2

Hilbert-vector gradient classes of finite correctors are homogeneous in the slope.

theorem HCPolySupport.HighContrast.normalizedLocalPair_finiteAffineCorrection_add {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e e' : Vec d) (n k : ℕ) : normalizedLocalPair (finiteAffineCorrectionLocalSequence a (e + e')) n k = normalizedLocalPair (finiteAffineCorrectionLocalSequence a e) n k + normalizedLocalPair (finiteAffineCorrectionLocalSequence a e') n k

Normalized local value-gradient pairs of finite correctors are additive in the slope.

theorem HCPolySupport.HighContrast.normalizedLocalPair_finiteAffineCorrection_smul {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (c : ℝ) (e : Vec d) (n k : ℕ) : normalizedLocalPair (finiteAffineCorrectionLocalSequence a (c • e)) n k = c • normalizedLocalPair (finiteAffineCorrectionLocalSequence a e) n k

Normalized local value-gradient pairs of finite correctors are homogeneous in the slope.