Coarse-graining support: Support.CoarseGraining.CoarseBounds.AeBridge

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

A.e.-ellipticity bridge (item C2)

The bridge that lets us replace an almost-everywhere-elliptic coefficient field by an everywhere-elliptic one without changing the coarse block matrix.

• C2(i) — Mu and hence coarseBlockMatrix only see a up to a.e. equality on the (measurable) averaging set.
• C2(ii) — the elliptic locus {x | IsEllipticMatrix 1 Θ (a x)}, intersected with the averaging set, is measurable. The proof avoids the matrix inverse: we replace the fourth ellipticity inequality Θ⁻¹|ξ|² ≤ ξ·A⁻¹ξ by the inverse-free image bound |Aη|² ≤ Θ (η·Aη) (equivalent, given coercivity), which makes the whole ellipticity locus a closed subset of the matrix-entry space — no countable dense reduction is needed.
• C2(iii) — the elliptic truncation ellipticTruncate Θ a, which agrees with a on the a.e.-elliptic set and is everywhere (1, Θ)-elliptic.
• C2(iv) — the consumer-facing packaging.

Vectors are Vec d = Fin d → ℝ; matrices Mat d = Matrix (Fin d) (Fin d) ℝ, which is definitionally the entry space Fin d → Fin d → ℝ. No EuclideanSpace.

C2(i) — Mu / coarseBlockMatrix a.e.-congruence

theorem HCPolySupport.Mu_congr_of_ae_eq {d : ℕ} {a a' : CoeffField d} {U : Set (Vec d)} (hae : a =ᵐ[MeasureTheory.volume.restrict U] a') (P : BlockVec d) : Mu U P a = Mu U P a'

The block energy density only depends on the coefficient field pointwise, so it is insensitive to changing a on a null set.

theorem HCPolySupport.coarseBlockMatrix_congr_of_ae_eq {d : ℕ} {a a' : CoeffField d} {U : Set (Vec d)} (hae : a =ᵐ[MeasureTheory.volume.restrict U] a') : coarseBlockMatrix U a = coarseBlockMatrix U a'

Corollary of C2(i): the coarse block matrix is insensitive to a null-set change of the coefficient field.

C2(ii) — measurability of the elliptic locus

The inverse-free reformulation of the (1, Θ) ellipticity class.

def HCPolySupport.IsEllipticEntry {d : ℕ} (Θ : ℝ) (v : Mat d) : Prop

The two inverse-free ellipticity inequalities, as a predicate on the matrix-entry space Mat d = Fin d → Fin d → ℝ.

Equations

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

theorem HCPolySupport.isEllipticMatrix_one_iff {d : ℕ} {Θ : ℝ} (A : Mat d) : IsEllipticMatrix 1 Θ A ↔ 1 ≤ Θ ∧ IsEllipticEntry Θ A

Inverse-free characterization. For the base constant lam = 1, the A⁻¹ inequality is equivalent to the image bound |Aη|² ≤ Θ (η·Aη).

theorem HCPolySupport.isClosed_isEllipticEntry {d : ℕ} {Θ : ℝ} : IsClosed {v : Fin d → Fin d → ℝ | IsEllipticEntry Θ v}

The inverse-free ellipticity locus is closed in the matrix-entry space Fin d → Fin d → ℝ (definitionally Mat d), which carries the product Borel structure.

theorem HCPolySupport.measurableSet_isEllipticMatrix_inter {d : ℕ} {Θ : ℝ} {a : CoeffField d} {U : Set (Vec d)} (hU : MeasurableSet U) (hmeasA : Measurable fun (x : Vec d) (i j : Fin d) => if x ∈ U then a x i j else 0) : MeasurableSet (U ∩ {x : Vec d | IsEllipticMatrix 1 Θ (a x)})

C2(ii). Given the IsEllipticFieldOn-style entrywise measurability of the U-truncated coefficient field, the elliptic locus intersected with U is measurable.

C2(iii) — the elliptic truncation

noncomputable def HCPolySupport.ellipticTruncate {d : ℕ} (Θ : ℝ) (a : CoeffField d) : CoeffField d

The elliptic truncation: keep a x where it is (1, Θ)-elliptic, otherwise replace it by the identity (which is (1, Θ)-elliptic whenever 1 ≤ Θ).

Equations

• HCPolySupport.ellipticTruncate Θ a x = if HCPolySupport.IsEllipticMatrix 1 Θ (a x) then a x else 1

theorem HCPolySupport.ellipticTruncate_of_elliptic {d : ℕ} {Θ : ℝ} {a : CoeffField d} {x : Vec d} (h : IsEllipticMatrix 1 Θ (a x)) : ellipticTruncate Θ a x = a x

theorem HCPolySupport.ellipticTruncate_of_not_elliptic {d : ℕ} {Θ : ℝ} {a : CoeffField d} {x : Vec d} (h : ¬IsEllipticMatrix 1 Θ (a x)) : ellipticTruncate Θ a x = 1

theorem HCPolySupport.isEllipticMatrix_one_one {d : ℕ} {Θ : ℝ} (hΘ : 1 ≤ Θ) : IsEllipticMatrix 1 Θ 1

The identity matrix is (1, Θ)-elliptic whenever 1 ≤ Θ.

theorem HCPolySupport.isEllipticMatrix_ellipticTruncate {d : ℕ} {Θ : ℝ} {a : CoeffField d} (hΘ : 1 ≤ Θ) (x : Vec d) : IsEllipticMatrix 1 Θ (ellipticTruncate Θ a x)

Every truncated matrix is (1, Θ)-elliptic, given 1 ≤ Θ.

theorem HCPolySupport.isEllipticFieldOn_ellipticTruncate {d : ℕ} {Θ : ℝ} {a : CoeffField d} {U : Set (Vec d)} (hU : MeasurableSet U) (hΘ : 1 ≤ Θ) (hmeasA : Measurable fun (x : Vec d) (i j : Fin d) => if x ∈ U then a x i j else 0) : IsEllipticFieldOn 1 Θ U (ellipticTruncate Θ a)

C2(iii)(a). The elliptic truncation is an everywhere-(1, Θ)-elliptic field on U, given 1 ≤ Θ and the entrywise measurability of the U-truncated coefficient field.

theorem HCPolySupport.ellipticTruncate_ae_eq {d : ℕ} {Θ : ℝ} {a : CoeffField d} {U : Set (Vec d)} (hae : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, IsEllipticMatrix 1 Θ (a x)) : ellipticTruncate Θ a =ᵐ[MeasureTheory.volume.restrict U] a

C2(iii)(b). On the a.e.-elliptic set, the truncation equals a.

C2(iv) — bridge packaging

theorem HCPolySupport.exists_ellipticFieldOn_ae_eq {d : ℕ} {Θ : ℝ} {a : CoeffField d} {U : Set (Vec d)} (hU : MeasurableSet U) (hΘ : 1 ≤ Θ) (hmeasA : Measurable fun (x : Vec d) (i j : Fin d) => if x ∈ U then a x i j else 0) (hae : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, IsEllipticMatrix 1 Θ (a x)) : ∃ (a' : CoeffField d), IsEllipticFieldOn 1 Θ U a' ∧ a' =ᵐ[MeasureTheory.volume.restrict U] a ∧ coarseBlockMatrix U a' = coarseBlockMatrix U a ∧ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, blockCoeffField a' x = blockCoeffField a x

C2(iv). From a.e. ellipticity on the (measurable) averaging set plus the entrywise measurability of the U-truncated field (and 1 ≤ Θ), produce a genuinely (1, Θ)-elliptic field a' that agrees with a a.e. on U, gives the same coarse block matrix, and the same block coefficient field a.e.