Coarse-graining support: Support.Internal.Ch02.Representatives

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.Internal.Ch02.BookCh02.matVecMul_smul_one {d : ℕ} (c : ℝ) (x : Vec d) : matVecMul (c • 1) x = c • x

theorem HCPolySupport.Internal.Ch02.BookCh02.isEllipticMatrix_smul_one {d : ℕ} {lam Lam : ℝ} (hlam : 0 < lam) (hLe : lam ≤ Lam) : IsEllipticMatrix lam Lam (lam • 1)

theorem HCPolySupport.Internal.Ch02.BookCh02.isSymm_smul_one {d : ℕ} (c : ℝ) : Matrix.IsSymm (c • 1)

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.measurableCoeffField {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : CoeffField d

A measurable representative of the public coefficient field, assembled entrywise from the AEStronglyMeasurable data.

Equations

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

theorem HCPolySupport.Internal.Ch02.BookCh02.measurableCoeffField_measurable {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Measurable fun (x : Vec d) (i j : Fin d) => measurableCoeffField U a x i j

theorem HCPolySupport.Internal.Ch02.BookCh02.measurableCoeffField_entry_ae_eq {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (i j : Fin d) : (fun (x : Vec d) => restrictCoeffField U.carrier a.toCoeffField x i j) =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => measurableCoeffField U a x i j

theorem HCPolySupport.Internal.Ch02.BookCh02.measurableCoeffField_ae_eq {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : measurableCoeffField U a =ᵐ[volumeMeasureOn U.carrier] a.toCoeffField

theorem HCPolySupport.Internal.Ch02.BookCh02.measurableCoeffField_aeElliptic {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U.carrier, IsEllipticMatrix a.lam a.Lam (measurableCoeffField U a x)

theorem HCPolySupport.Internal.Ch02.BookCh02.measurableCoeffField_aeSymmetric {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U.carrier, Matrix.IsSymm (measurableCoeffField U a x)

structure HCPolySupport.Internal.Ch02.BookCh02.GoodSetData {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Type

A measurable set of full measure on U where the measurable coefficient representative is elliptic.

• set : Set (Vec d)

  The chosen full-measure measurable set of pointwise ellipticity.

• ae_mem : self.set ∈ MeasureTheory.ae (volumeMeasureOn U.carrier)
• measurableSet : MeasurableSet self.set
• elliptic (x : Vec d) : x ∈ self.set → IsEllipticMatrix a.lam a.Lam (measurableCoeffField U a x)

theorem HCPolySupport.Internal.Ch02.BookCh02.exists_goodSetData {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Nonempty (GoodSetData U a)

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.goodSetData {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : GoodSetData U a

Choose a measurable full-measure set where the coefficient representative has its ellipticity bounds.

Equations

• HCPolySupport.Internal.Ch02.BookCh02.goodSetData U a = Classical.choice ⋯

structure HCPolySupport.Internal.Ch02.BookCh02.GoodSymmetricSetData {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : Type

A measurable full-measure set where the coefficient representative is both elliptic and symmetric.

• set : Set (Vec d)

  The chosen full-measure measurable set of pointwise ellipticity and symmetry.

• ae_mem : self.set ∈ MeasureTheory.ae (volumeMeasureOn U.carrier)
• measurableSet : MeasurableSet self.set
• elliptic (x : Vec d) : x ∈ self.set → IsEllipticMatrix a.lam a.Lam (measurableCoeffField U a x)
• symmetric (x : Vec d) : x ∈ self.set → Matrix.IsSymm (measurableCoeffField U a x)

theorem HCPolySupport.Internal.Ch02.BookCh02.exists_goodSymmetricSetData {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : Nonempty (GoodSymmetricSetData U a hsym)

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.goodSymmetricSetData {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : GoodSymmetricSetData U a hsym

Choose a measurable full-measure set where the symmetric coefficient representative is elliptic.

Equations

• HCPolySupport.Internal.Ch02.BookCh02.goodSymmetricSetData U a hsym = Classical.choice ⋯

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffField {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : CoeffField d

Internal pointwise-good representative of the public a.e. coefficient field. Outside a measurable full-measure good set we insert the scalar matrix a.lam • I, which is uniformly elliptic with the same constants.

Equations

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

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffField_ae_eq {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : pointwiseCoeffField U a =ᵐ[volumeMeasureOn U.carrier] a.toCoeffField

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffField_measurable {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Measurable fun (x : Vec d) (i j : Fin d) => pointwiseCoeffField U a x i j

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffField_restrict_measurable {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Measurable fun (x : Vec d) (i j : Fin d) => restrictCoeffField U.carrier (pointwiseCoeffField U a) x i j

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffField_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : IsEllipticFieldOn a.lam a.Lam U.carrier (pointwiseCoeffField U a)

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffField_isEllipticFieldOn_cubeSet {d : ℕ} (Q : TriadicCube d) (a : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain Q)) : IsEllipticFieldOn a.lam a.Lam (cubeSet Q) (pointwiseCoeffField (Book.Ch02.cubeDomain Q) a)

The pointwise-good representative attached to the public open-cube coefficient field is pointwise elliptic on the corresponding closed cube.

The public CoeffOn data are a.e.-elliptic on the open cube. The representative fills the exceptional set by a.lam • I, so the same pointwise ellipticity extends across the half-open/closed cube realization used by the deterministic proof engines.

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : Book.Ch02.CoeffOn U

The coefficient representative using the measurable field on its good set and a.lam • 1 elsewhere.

Equations

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

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffOn_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : IsEllipticFieldOn (pointwiseCoeffOn U a).lam (pointwiseCoeffOn U a).Lam U.carrier (pointwiseCoeffOn U a).toCoeffField

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffOn_ae_eq {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : (pointwiseCoeffOn U a).AEEq a

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffField {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : CoeffField d

Pointwise elliptic and pointwise symmetric representative used to consume old symmetric proof engines while preserving the public a.e. symmetry surface.

Equations

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

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffField_ae_eq {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : pointwiseSymmetricCoeffField U a hsym =ᵐ[volumeMeasureOn U.carrier] a.toCoeffField

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffField_measurable {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : Measurable fun (x : Vec d) (i j : Fin d) => pointwiseSymmetricCoeffField U a hsym x i j

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffField_restrict_measurable {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : Measurable fun (x : Vec d) (i j : Fin d) => restrictCoeffField U.carrier (pointwiseSymmetricCoeffField U a hsym) x i j

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffField_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : IsEllipticFieldOn a.lam a.Lam U.carrier (pointwiseSymmetricCoeffField U a hsym)

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffField_isSymmetricCoeffField {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : IsSymmetricCoeffField (pointwiseSymmetricCoeffField U a hsym)

noncomputable def HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : Book.Ch02.CoeffOn U

The symmetric coefficient representative using its measurable field on the good set and a.lam • 1 elsewhere.

Equations

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

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffOn_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : IsEllipticFieldOn (pointwiseSymmetricCoeffOn U a hsym).lam (pointwiseSymmetricCoeffOn U a hsym).Lam U.carrier (pointwiseSymmetricCoeffOn U a hsym).toCoeffField

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffOn_isSymmetricCoeffField {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : IsSymmetricCoeffField (pointwiseSymmetricCoeffOn U a hsym).toCoeffField

theorem HCPolySupport.Internal.Ch02.BookCh02.pointwiseSymmetricCoeffOn_ae_eq {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : (pointwiseSymmetricCoeffOn U a hsym).AEEq a