High-contrast homogenization: Provider.Regularity.CorrectorJointLimit

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

Joint local limits of finite correctors

Componentwise gradient Cauchy convergence for every slope determines one unique family of normalized projective local H¹ carriers. Its scalar-value and Hilbert-vector-gradient projections are linear in the slope.

def HCPolySupport.HighContrast.FiniteAffineCorrectionLocalCauchy {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) : Prop

Componentwise local gradient Cauchy convergence for every boundary slope.

Equations

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

noncomputable def HCPolySupport.HighContrast.NormalizedLocalH1Carrier.addCarrier {d : ℕ} (z w : NormalizedLocalH1Carrier d) : NormalizedLocalH1Carrier d

Addition of normalized local carriers, defined componentwise.

Equations

• z.addCarrier w = { value := z.value + w.value, gradient := z.gradient + w.gradient, graph := ⋯, unitMeanZero := ⋯ }

noncomputable def HCPolySupport.HighContrast.NormalizedLocalH1Carrier.smulCarrier {d : ℕ} (c : ℝ) (z : NormalizedLocalH1Carrier d) : NormalizedLocalH1Carrier d

Scalar multiplication of a normalized local carrier, defined componentwise.

Equations

• HCPolySupport.HighContrast.NormalizedLocalH1Carrier.smulCarrier c z = { value := c • z.value, gradient := c • z.gradient, graph := ⋯, unitMeanZero := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.addCarrier_valueComponent {d : ℕ} (z w : NormalizedLocalH1Carrier d) (n : ℕ) : (z.addCarrier w).valueComponent n = z.valueComponent n + w.valueComponent n

@[simp]

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.addCarrier_gradientComponent {d : ℕ} (z w : NormalizedLocalH1Carrier d) (n : ℕ) : (z.addCarrier w).gradientComponent n = z.gradientComponent n + w.gradientComponent n

@[simp]

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.smulCarrier_valueComponent {d : ℕ} (c : ℝ) (z : NormalizedLocalH1Carrier d) (n : ℕ) : (smulCarrier c z).valueComponent n = c • z.valueComponent n

@[simp]

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.smulCarrier_gradientComponent {d : ℕ} (c : ℝ) (z : NormalizedLocalH1Carrier d) (n : ℕ) : (smulCarrier c z).gradientComponent n = c • z.gradientComponent n

theorem HCPolySupport.HighContrast.IsNormalizedLocalLimit.finiteAffineCorrection_add {d : ℕ} [NeZero d] {a : Book.Ch02.TriadicCoeffFamily d} {e e' : Vec d} {z w : NormalizedLocalH1Carrier d} (hz : IsNormalizedLocalLimit (finiteAffineCorrectionLocalSequence a e) z) (hw : IsNormalizedLocalLimit (finiteAffineCorrectionLocalSequence a e') w) : IsNormalizedLocalLimit (finiteAffineCorrectionLocalSequence a (e + e')) (z.addCarrier w)

Additive normalized local pair limits combine to the normalized local limit of the sum-slope finite correctors.

theorem HCPolySupport.HighContrast.IsNormalizedLocalLimit.finiteAffineCorrection_smul {d : ℕ} [NeZero d] {a : Book.Ch02.TriadicCoeffFamily d} {e : Vec d} {z : NormalizedLocalH1Carrier d} (c : ℝ) (hz : IsNormalizedLocalLimit (finiteAffineCorrectionLocalSequence a e) z) : IsNormalizedLocalLimit (finiteAffineCorrectionLocalSequence a (c • e)) (NormalizedLocalH1Carrier.smulCarrier c z)

Homogeneous normalized local pair limits combine to the normalized local limit of the scaled-slope finite correctors.

def HCPolySupport.HighContrast.IsFiniteAffineCorrectionJointLocalLimit {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) : Prop

A joint normalized local limit is a family satisfying the literal local limit characterization at every slope.

Equations

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

theorem HCPolySupport.HighContrast.existsUnique_finiteAffineCorrectionJointLocalLimit {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) : ∃! Phi : Vec d → NormalizedLocalH1Carrier d, IsFiniteAffineCorrectionJointLocalLimit a Phi

A componentwise Cauchy family has one and only one joint normalized local limit family.

noncomputable def HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalLimit {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) : Vec d → NormalizedLocalH1Carrier d

The joint normalized local corrector family selected from its unique characterization.

Equations

• HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalLimit a hCauchy = Classical.choose ⋯

theorem HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalLimit_isLimit {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) : IsFiniteAffineCorrectionJointLocalLimit a (finiteAffineCorrectionJointLocalLimit a hCauchy)

The selected joint family satisfies the literal local-limit characterization.

theorem HCPolySupport.HighContrast.isFiniteAffineCorrectionJointLocalLimit_iff_eq {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (Phi : Vec d → NormalizedLocalH1Carrier d) : IsFiniteAffineCorrectionJointLocalLimit a Phi ↔ Phi = finiteAffineCorrectionJointLocalLimit a hCauchy

The literal characterization identifies exactly the selected joint family.

theorem HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalLimit_add {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e e' : Vec d) : finiteAffineCorrectionJointLocalLimit a hCauchy (e + e') = (finiteAffineCorrectionJointLocalLimit a hCauchy e).addCarrier (finiteAffineCorrectionJointLocalLimit a hCauchy e')

The selected joint normalized local corrector family is additive in the slope.

theorem HCPolySupport.HighContrast.finiteAffineCorrectionJointLocalLimit_smul {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (c : ℝ) (e : Vec d) : finiteAffineCorrectionJointLocalLimit a hCauchy (c • e) = NormalizedLocalH1Carrier.smulCarrier c (finiteAffineCorrectionJointLocalLimit a hCauchy e)

The selected joint normalized local corrector family is homogeneous in the slope.