High-contrast homogenization: Setup.CoefficientSpace

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

The high-contrast coefficient space

This file fixes the coefficient class of s.introduction: measurable coefficient fields modulo equality almost everywhere that are uniformly elliptic almost everywhere on every bounded set, together with the integer translation action on them.

Scope of the coefficient class. The coefficient space used here is the set of measurable fields that are locally uniformly elliptic: on every bounded subset of ℝ^d one pair of ellipticity constants serves almost every value of the field there, the pair being attached to the field and to the set rather than fixed in advance. No constant appearing in any statement below depends on such a pair, and no bound of the development is uniform over the coefficient space. The class contains the fields uniformly elliptic almost everywhere on all of ℝ^d. The paper's condition e.qualitative.ellipticity states local essential bounds on s, s⁻¹ and kᵗ s⁻¹ k, expressing local uniform ellipticity in matrix terms. The coefficient class here also satisfies the weaker local integrability conditions used by the analytic library. All quantitative content — the reference aspect ratio Π, the concentration gauge and its growth witness, the annealed contrast Θ_m, and every dimensional constant — is unchanged.

The canonical measurable structure on Mat d. Several modules of the reference library introduce a measurable structure on Mat d, all of them the entrywise product structure transported from Fin d → Fin d → ℝ; one of them, HCPolySupport.Book.Ch04.SourceObservable, declares its copy private, which hides the name but still registers the instance globally. Whichever copy instance resolution happens to select, BorelSpace (Mat d) is then searched for that copy, and the two Borel instances of the reference library are stated for two of the others, so a goal BorelSpace (Mat d) becomes unsolvable in any public import closure where the private copy wins. The pair HCPolySupport.instMeasurableSpaceMat and HCPolySupport.instBorelSpaceMat is the canonical path, and it is raised here to a priority no other copy reaches, so that every module of this library — both the polynomial-entry route and the proofs of the other three theorems — resolves MeasurableSpace (Mat d) and BorelSpace (Mat d) along one and the same path. All the copies are the same structure up to unfolding, so nothing stated for another of them stops applying.

The coefficient space Ω

def HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic {d : ℕ} (b : CoeffField d) : Prop

Qualitative local uniform ellipticity of a coefficient field: on every ball around the origin there is a pair of ellipticity constants for which almost every value of the field on that ball is uniformly elliptic in the sense of IsEllipticMatrix, that is, coercive with a bounded inverse.

The constants are quantified inside the predicate: they belong to the field and to the ball, and never enter an estimate. Since every bounded set lies in a ball, the same statement holds with an arbitrary bounded set in place of the ball.

Equations

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

def HCPolySupport.HighContrast.AEUniformlyEllipticField {d : ℕ} (a : Source.AKL.Field d) : Prop

Qualitative local uniform ellipticity of a point of the a.e.-quotient carrier Source.AKL.Field: local uniform ellipticity of any of its representatives.

The paper's local essential boundedness of s, s⁻¹ and kᵗ s⁻¹ k at e.qualitative.ellipticity, and the almost everywhere positive definiteness of the symmetric part, both follow.

Equations

• HCPolySupport.HighContrast.AEUniformlyEllipticField a = HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic ↑a

def HCPolySupport.HighContrast.CoeffSpace (d : ℕ) : Type

The coefficient space Ω: measurable coefficient fields modulo equality almost everywhere, locally uniformly elliptic in the qualitative sense.

Equations

• HCPolySupport.HighContrast.CoeffSpace d = { a : HCPolySupport.Source.AKL.Field d // HCPolySupport.HighContrast.AEUniformlyEllipticField a }

Bounded sets

theorem HCPolySupport.HighContrast.exists_ball_of_isBounded {d : ℕ} {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (R : ℝ), 0 < R ∧ S ⊆ Metric.ball 0 R

Every bounded subset of ℝ^d lies in a ball of positive radius around the origin.

theorem HCPolySupport.HighContrast.ae_restrict_mem_of_subset {d : ℕ} {S T : Set (Vec d)} (hST : S ⊆ T) (hT : MeasurableSet T) : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict S, x ∈ T

The restricted Lebesgue measure of a subset is carried by any measurable set containing it.

theorem HCPolySupport.HighContrast.isEllipticMatrix_one_le {d : ℕ} {Theta : ℝ} (hTheta : 1 ≤ Theta) : IsEllipticMatrix 1 Theta 1

The identity matrix is uniformly elliptic with lower constant 1 and any upper constant at least 1.

Local uniform ellipticity of a coefficient field

theorem HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic.exists_ae_isEllipticMatrix_of_isBounded {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ᵐ (x : Vec d), x ∈ S → IsEllipticMatrix lam Lam (b x)

Local uniform ellipticity on bounded sets. A locally uniformly elliptic field has a pair of ellipticity constants for almost every value on any bounded set, not only on a ball.

theorem HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic.congr {d : ℕ} {b b' : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) (h : b =ᵐ[MeasureTheory.volume] b') : IsAELocallyUniformlyElliptic b'

Local uniform ellipticity depends only on the almost everywhere class of the field.

theorem HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic.comp_add_right {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) (z : Vec d) : IsAELocallyUniformlyElliptic fun (x : Vec d) => b (x + z)

Local uniform ellipticity is preserved by translating the argument: the ball of radius R is served by the constants of the ball of radius R + ‖z‖.

theorem HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic.ae_exists_isEllipticMatrix {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) : ∀ᵐ (x : Vec d), ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ IsEllipticMatrix lam Lam (b x)

Almost every value of a locally uniformly elliptic field is uniformly elliptic for some pair of constants: the balls of integer radius exhaust ℝ^d, so the countably many null sets of the local statements unite into one.

theorem HCPolySupport.HighContrast.norm_matVecMul_le {d : ℕ} (L : Mat d) (x : Vec d) : ‖matVecMul L x‖ ≤ (∑ i : Fin d, ∑ j : Fin d, |L i j|) * ‖x‖

Every coordinate of L x is bounded by the sum of the absolute entries of L times the sup norm of x.

theorem HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic.comp_matVecMul {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) (L : Mat d) (hL : MeasureTheory.QuasiMeasurePreserving (matVecMul L) MeasureTheory.volume MeasureTheory.volume) : IsAELocallyUniformlyElliptic fun (y : Vec d) => b (matVecMul L y)

Local uniform ellipticity is preserved by composing the argument with a matrix that transports the Lebesgue null sets: a ball is carried into a ball of proportional radius.

theorem HCPolySupport.HighContrast.IsAELocallyUniformlyElliptic.exists_ae_isEllipticMatrix_ae_eq_restrict {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (lam : ℝ) (Lam : ℝ) (c : CoeffField d), 0 < lam ∧ lam ≤ Lam ∧ (∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (c x)) ∧ b =ᵐ[MeasureTheory.volume.restrict S] c

The globally elliptic companion on a bounded set. A locally uniformly elliptic field agrees, almost everywhere on a bounded set, with a field that is uniformly elliptic almost everywhere on all of ℝ^d: keep the field on a ball containing the set and put the identity matrix outside.

theorem HCPolySupport.HighContrast.isAELocallyUniformlyElliptic_of_ae_isEllipticMatrix {d : ℕ} {b : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) : IsAELocallyUniformlyElliptic b

A field uniformly elliptic almost everywhere on all of ℝ^d is locally uniformly elliptic, with the same pair of constants on every ball.

Local uniform ellipticity on the a.e.-quotient carrier

theorem HCPolySupport.HighContrast.AEUniformlyEllipticField.exists_ae_isEllipticMatrix_of_isBounded {d : ℕ} {a : Source.AKL.Field d} (ha : AEUniformlyEllipticField a) {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ᵐ (x : Vec d), x ∈ S → IsEllipticMatrix lam Lam (↑a x)

Local uniform ellipticity on bounded sets, on the a.e.-quotient carrier.

theorem HCPolySupport.HighContrast.aeUniformlyEllipticField_of_ae_eq {d : ℕ} {a : Source.AKL.Field d} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) (hab : ↑a =ᵐ[MeasureTheory.volume] b) : AEUniformlyEllipticField a

A point of the a.e.-quotient carrier whose representatives are locally uniformly elliptic lies in the coefficient class.

theorem HCPolySupport.HighContrast.aeUniformlyEllipticField_iff_isBounded {d : ℕ} {a : Source.AKL.Field d} : AEUniformlyEllipticField a ↔ ∀ (S : Set (Vec d)), Bornology.IsBounded S → ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ᵐ (x : Vec d), x ∈ S → IsEllipticMatrix lam Lam (↑a x)

The ball form and the bounded-set form of the coefficient class agree.

theorem HCPolySupport.HighContrast.aeUniformlyEllipticField_of_ae_isEllipticMatrix {d : ℕ} {a : Source.AKL.Field d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (↑a x)) : AEUniformlyEllipticField a

A point of the a.e.-quotient carrier uniformly elliptic almost everywhere on all of ℝ^d lies in the coefficient class, with the same pair of constants on every ball.

Integer translations

theorem HCPolySupport.HighContrast.aeUniformlyEllipticField_translateField {d : ℕ} (z : Fin d → ℤ) {a : Source.AKL.Field d} (ha : AEUniformlyEllipticField a) : AEUniformlyEllipticField (Source.AKL.translateField z a)

Qualitative local uniform ellipticity is preserved by integer translation of the field: the ball of radius R for the translated field is served by the constants of the ball of radius R + ‖z‖ for the field.

noncomputable def HCPolySupport.HighContrast.translateCoeff {d : ℕ} (z : Fin d → ℤ) (a : CoeffSpace d) : CoeffSpace d

The integer translation action T_z on the coefficient space.

Equations

• HCPolySupport.HighContrast.translateCoeff z a = ⟨HCPolySupport.Source.AKL.translateField z ↑a, ⋯⟩

Essential boundedness and pointwise representatives

theorem HCPolySupport.HighContrast.ae_abs_entry_le_of_aeUniformlyEllipticField {d : ℕ} {a : Source.AKL.Field d} (ha : AEUniformlyEllipticField a) {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d), x ∈ S → ∀ (i j : Fin d), |↑a x i j| ≤ M

Every entry of a locally uniformly elliptic field is essentially bounded on every bounded set, by the upper ellipticity constant of the field there.

theorem HCPolySupport.HighContrast.not_aeUniformlyEllipticField_of_not_ae_bounded {d : ℕ} {a : Source.AKL.Field d} {S : Set (Vec d)} (hS : Bornology.IsBounded S) (hub : ∀ (M : ℝ), ¬∀ᵐ (x : Vec d), x ∈ S → ∀ (i j : Fin d), |↑a x i j| ≤ M) : ¬AEUniformlyEllipticField a

A field with an entry essentially unbounded on a bounded set is not in the coefficient space.

theorem HCPolySupport.HighContrast.integrableOn_sq_entry_of_aeUniformlyEllipticField {d : ℕ} {a : Source.AKL.Field d} (ha : AEUniformlyEllipticField a) {U : Set (Vec d)} (hU : Bornology.IsBounded U) (i j : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => ↑a x i j ^ 2) U MeasureTheory.volume

Every entry of a field of the coefficient space is square integrable on every bounded set.

theorem HCPolySupport.HighContrast.not_aeUniformlyEllipticField_of_not_integrableOn_sq {d : ℕ} {a : Source.AKL.Field d} {U : Set (Vec d)} (hU : Bornology.IsBounded U) (i j : Fin d) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => ↑a x i j ^ 2) U MeasureTheory.volume) : ¬AEUniformlyEllipticField a

A field with an entry that fails to be square integrable on a bounded set is not in the coefficient space.

theorem HCPolySupport.HighContrast.ne_of_not_integrableOn_sq {d : ℕ} {a : Source.AKL.Field d} {U : Set (Vec d)} (hU : Bornology.IsBounded U) (i j : Fin d) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => ↑a x i j ^ 2) U MeasureTheory.volume) (b : CoeffSpace d) : ↑b ≠ a

No point of the coefficient space carries such a field, so no law on the coefficient space is supported on one.

theorem HCPolySupport.HighContrast.isEllipticMatrix_inv_smul {d : ℕ} {lam Lam : ℝ} (hlam : 0 < lam) {A : Mat d} (hA : IsEllipticMatrix lam Lam A) : IsEllipticMatrix 1 (Lam / lam) (lam⁻¹ • A)

Normalizing the lower ellipticity constant to 1.

theorem HCPolySupport.HighContrast.isEllipticMatrix_smul {d : ℕ} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) {B : Mat d} (hB : IsEllipticMatrix 1 (Lam / lam) B) : IsEllipticMatrix lam Lam (lam • B)

Undoing the normalization.

theorem HCPolySupport.HighContrast.exists_pointwise_elliptic_representative {d : ℕ} {a : Source.AKL.Field d} (ha : AEUniformlyEllipticField a) {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (lam : ℝ) (Lam : ℝ) (f : CoeffField d), 0 < lam ∧ lam ≤ Lam ∧ Measurable f ∧ (∀ x ∈ S, IsEllipticMatrix lam Lam (f x)) ∧ ↑a =ᵐ[MeasureTheory.volume] f

The pointwise representative on a bounded set. Every field of the coefficient space has a measurable representative, equal to it almost everywhere, that is uniformly elliptic at every point of a prescribed bounded set.

theorem HCPolySupport.HighContrast.exists_locally_pointwise_elliptic_representative {d : ℕ} {a : Source.AKL.Field d} (ha : AEUniformlyEllipticField a) : ∃ (f : CoeffField d), Measurable f ∧ ↑a =ᵐ[MeasureTheory.volume] f ∧ ∀ (R : ℝ), 0 < R → ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ ∀ x ∈ Metric.ball 0 R, IsEllipticMatrix lam Lam (f x)

The locally elliptic representative. Every field of the coefficient space has one measurable representative, equal to it almost everywhere, that is uniformly elliptic at every point of every ball, with the constants of that ball: the representatives of the balls of integer radius are glued along the shells they exhaust ℝ^d by.

theorem HCPolySupport.HighContrast.exists_globally_elliptic_representative_ae_eq_on {d : ℕ} {a : Source.AKL.Field d} (ha : AEUniformlyEllipticField a) {S : Set (Vec d)} (hS : Bornology.IsBounded S) : ∃ (lam : ℝ) (Lam : ℝ) (f : CoeffField d), 0 < lam ∧ lam ≤ Lam ∧ Measurable f ∧ (∀ (x : Vec d), IsEllipticMatrix lam Lam (f x)) ∧ ↑a =ᵐ[MeasureTheory.volume.restrict S] f

The everywhere elliptic representative of a bounded set. Every field of the coefficient space agrees, almost everywhere on a prescribed bounded set, with a measurable field that is uniformly elliptic at every point of ℝ^d.