High-contrast homogenization: Consistency.WitnessField

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

The constant identity coefficient field as a point of CoeffSpace

This module checks the definition CoeffSpace of the coefficient space of s.introduction at its reference point constIdentity, through the field identityField and the translation translateCoeff that the point must respect.

Were the check to fail, the coefficient space would lose its exhibited point: the class CoeffSpace d would be empty, the Dirac witness law of HCPoly.Annealed.Witness could not be formed, and the hypothesis set of t.polynomial.entry — a probability law that is stationary, of unit range and coarsely elliptic — would be left without a model and its conclusion vacuous. A failure of translateCoeff_constIdentity would put the witness law outside the translation-invariant class s.introduction prints, and a failure of coeFn_identityField would make the field, as an a.e. class, something other than the identity matrix.

This module is a consistency check of that definition and is not a result of the paper.

The reference point of the coefficient space of s.introduction: the field whose value is the identity matrix almost everywhere. It is uniformly elliptic with both ellipticity constants equal to one, and it is fixed by every integer translation of the coefficient space.

noncomputable def HCPolySupport.HighContrast.identityField (d : ℕ) : Source.AKL.Field d

The constant identity coefficient field, as a point of the a.e.-quotient carrier of coefficient fields.

Equations

• HCPolySupport.HighContrast.identityField d = MeasureTheory.AEEqFun.const (HCPolySupport.Vec d) 1

theorem HCPolySupport.HighContrast.coeFn_identityField {d : ℕ} : ↑(identityField d) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => 1

theorem HCPolySupport.HighContrast.matVecMul_identity {d : ℕ} (x : Vec d) : matVecMul 1 x = x

The identity matrix acts as the identity on vectors.

theorem HCPolySupport.HighContrast.isEllipticMatrix_identity {d : ℕ} : IsEllipticMatrix 1 1 1

The identity matrix is uniformly elliptic with both constants equal to one.

theorem HCPolySupport.HighContrast.aeUniformlyEllipticField_identityField {d : ℕ} : AEUniformlyEllipticField (identityField d)

noncomputable def HCPolySupport.HighContrast.constIdentity (d : ℕ) : CoeffSpace d

The constant identity field as a point of the coefficient space.

Equations

• HCPolySupport.HighContrast.constIdentity d = ⟨HCPolySupport.HighContrast.identityField d, ⋯⟩

theorem HCPolySupport.HighContrast.coeFn_constIdentity {d : ℕ} : ↑↑(constIdentity d) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => 1

theorem HCPolySupport.HighContrast.translateField_identityField {d : ℕ} (z : Fin d → ℤ) : Source.AKL.translateField z (identityField d) = identityField d

The constant identity field is fixed by every integer translation.

theorem HCPolySupport.HighContrast.translateCoeff_constIdentity {d : ℕ} (z : Fin d → ℤ) : translateCoeff z (constIdentity d) = constIdentity d