Coarse-graining support: Support.Probability.RegCoeffField.Differentiation

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

Ball averages of carrier fields and Lebesgue differentiation

This file is the analytic core of the honest slice-measurability route (Packet P4b of the carrier redesign). For a carrier field a : RegCoeffField d and a measurable set B it introduces the matrix of scalar entry averages

avgMat B a = fun i j => (volume B)⁻¹ • ∫_B a(·)_{ij},

records the entry-test bridge

avgMat B a i j = (volume B)⁻¹ • entryTestR i j (indicator B 1) a

(so that on rational balls B ⊆ U the average is an honest function of the local entry-test generators — used for LocalSigmaR U-measurability in SliceMeasurability.lean), and proves the two-directional characterization of spatial a.e. ellipticity in terms of rational-ball averages:

• forward (Jensen): the average of an a.e.-elliptic field over a ball stays in the closed convex elliptic locus (isEllipticMatrix_avgMat_of_aeRestrict, built on Convex.set_average_mem);
• backward (Lebesgue differentiation): if all rational-ball averages of a inside an open set U are elliptic, then a is a.e.-elliptic on U (aeRestrict_isEllipticMatrix_of_forall_ratBall), built on the centre-free Lebesgue differentiation theorem IsUnifLocDoublingMeasure.ae_tendsto_average (whose Vitali family provides the differentiation basis of closed metric balls on Vec d = Fin d → ℝ, whose Lebesgue volume is a doubling additive Haar measure).

Reference: the paper (Armstrong–Kuusi–Loher, to appear).

The matrix of entry averages

noncomputable def HCPolySupport.avgMat {d : ℕ} (B : Set (Vec d)) (a : RegCoeffField d) : Mat d

The matrix of scalar entry averages of a carrier field over a set B. Its (i, j) entry is the average of a(·)_{ij} over B for the Lebesgue measure.

Equations

• HCPolySupport.avgMat B a i j = (MeasureTheory.volume B).toReal⁻¹ • ∫ (x : HCPolySupport.Vec d) in B, a.toFun x i j

theorem HCPolySupport.avgMat_entry_eq_setAverage {d : ℕ} (B : Set (Vec d)) (a : RegCoeffField d) (i j : Fin d) : avgMat B a i j = ⨍ (x : Vec d) in B, a.toFun x i j

The entry average is the corresponding scalar set-average.

The entry-test bridge

theorem HCPolySupport.isProbeR_indicator {d : ℕ} {B : Set (Vec d)} (hBcpt : IsCompact B) (hBmeas : MeasurableSet B) : IsProbeR (B.indicator fun (x : Vec d) => 1)

The constant-one indicator of a compact measurable set is an enriched probe.

theorem HCPolySupport.support_indicator_one_subset {d : ℕ} (B : Set (Vec d)) : Function.support (B.indicator fun (x : Vec d) => 1) ⊆ B

The support of the constant-one indicator of B is contained in B.

theorem HCPolySupport.entryTestR_indicator_one {d : ℕ} (i j : Fin d) (B : Set (Vec d)) (hBmeas : MeasurableSet B) (a : RegCoeffField d) : entryTestR i j (B.indicator fun (x : Vec d) => 1) a = ∫ (x : Vec d) in B, a.toFun x i j

The entry-test bridge (integral form). The entry test of a carrier field against the constant-one indicator of a measurable set is the set integral of that entry.

theorem HCPolySupport.avgMat_entry_eq_smul_entryTestR {d : ℕ} (i j : Fin d) (B : Set (Vec d)) (hBmeas : MeasurableSet B) (a : RegCoeffField d) : avgMat B a i j = (MeasureTheory.volume B).toReal⁻¹ • entryTestR i j (B.indicator fun (x : Vec d) => 1) a

The entry-test bridge. Each entry of the ball average is a scalar multiple of the localized entry-test generator against the ball indicator.

Integrability and the pi realization

def HCPolySupport.matPi {d : ℕ} (a : RegCoeffField d) (x : Vec d) : Fin d → Fin d → ℝ

The pi realization x ↦ (a(x)_{ij})_{ij} of a carrier field, valued in the genuine finite pi space Fin d → Fin d → ℝ (which — unlike Mat d — carries the NormedSpace/CompleteSpace structure needed by the Bochner–Jensen average).

Equations

• HCPolySupport.matPi a x i j = a.toFun x i j

def HCPolySupport.elliptPi {d : ℕ} (lam Lam : ℝ) : Set (Fin d → Fin d → ℝ)

The elliptic locus, realized natively on the pi space (defeq to the Mat d locus of EllipticSet.lean, but stated so the Bochner average unifies without triggering the blocked Matrix norm instances).

Equations

• HCPolySupport.elliptPi lam Lam = {M : Fin d → Fin d → ℝ | HCPolySupport.IsEllipticMatrix lam Lam M}

theorem HCPolySupport.convex_elliptPi {d : ℕ} (lam Lam : ℝ) : Convex ℝ (elliptPi lam Lam)

theorem HCPolySupport.isClosed_elliptPi {d : ℕ} (lam Lam : ℝ) : IsClosed (elliptPi lam Lam)

def HCPolySupport.entryCLM {d : ℕ} (i j : Fin d) : (Fin d → Fin d → ℝ) →L[ℝ] ℝ

The eval continuous-linear map picking out the (i, j) entry of a pi matrix.

Equations

• HCPolySupport.entryCLM i j = ContinuousLinearMap.proj j ∘SL ContinuousLinearMap.proj i

theorem HCPolySupport.integrableOn_matPi {d : ℕ} (a : RegCoeffField d) {B : Set (Vec d)} (hB : IsCompact B) : MeasureTheory.IntegrableOn (matPi a) B MeasureTheory.volume

The pi realization is integrable on compact sets.

theorem HCPolySupport.avgMat_eq_setAverage {d : ℕ} (a : RegCoeffField d) {B : Set (Vec d)} (hB : IsCompact B) : avgMat B a = ⨍ (x : Vec d) in B, matPi a x

The Mat d entry average agrees with the Bochner set-average of the pi realization.

Forward direction (Jensen)

theorem HCPolySupport.isEllipticMatrix_avgMat_of_aeRestrict {d : ℕ} {U : Set (Vec d)} {lam Lam : ℝ} {a : RegCoeffField d} (hae : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, IsEllipticMatrix lam Lam (a.toFun x)) {B : Set (Vec d)} (hBcpt : IsCompact B) (hBU : B ⊆ U) (hB0 : MeasureTheory.volume B ≠ 0) (hBfin : MeasureTheory.volume B ≠ ⊤) : IsEllipticMatrix lam Lam (avgMat B a)

Forward (Jensen). If a carrier field is a.e.-elliptic on the restricted measure of U, then its average over any compact ball B ⊆ U of positive finite volume is elliptic. Immediate from Convex.set_average_mem on the closed convex elliptic locus.

Rational balls

def HCPolySupport.ratPt {d : ℕ} (q : Fin d → ℚ) : Vec d

The real point with rational coordinates q.

Equations

• HCPolySupport.ratPt q i = ↑(q i)

theorem HCPolySupport.exists_ratBall {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {x : Vec d} (hx : x ∈ U) {ε : ℝ} (hε : 0 < ε) : ∃ (q : Fin d → ℚ) (r : ℚ), 0 < ↑r ∧ ↑r < ε ∧ x ∈ Metric.closedBall (ratPt q) ↑r ∧ Metric.closedBall (ratPt q) ↑r ⊆ U

Rational balls are cofinal in an open set. For a point x of an open set U and any positive tolerance ε, there is a rational-centre rational-radius closed ball of radius below ε that contains x and lies in U.

Backward direction (Lebesgue differentiation)

theorem HCPolySupport.aeRestrict_isEllipticMatrix_of_forall_ratBall {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) {lam Lam : ℝ} {a : RegCoeffField d} (H : ∀ (q : Fin d → ℚ) (r : ℚ), 0 < ↑r → Metric.closedBall (ratPt q) ↑r ⊆ U → IsEllipticMatrix lam Lam (avgMat (Metric.closedBall (ratPt q) ↑r) a)) : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, IsEllipticMatrix lam Lam (a.toFun x)

Backward (Lebesgue differentiation). If every rational ball B ⊆ U (with U open) has elliptic average, then the carrier field is a.e.-elliptic on U. For a.e. x the centre-free Lebesgue differentiation theorem provides a sequence of rational balls containing x and shrinking to it whose averages converge to a x; each average is elliptic and the locus is closed, so a x is elliptic.

The characterization

theorem HCPolySupport.aeRestrict_isEllipticMatrix_iff_forall_ratBall {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (lam Lam : ℝ) (a : RegCoeffField d) : (∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, IsEllipticMatrix lam Lam (a.toFun x)) ↔ ∀ (q : Fin d → ℚ) (r : ℚ), 0 < ↑r → Metric.closedBall (ratPt q) ↑r ⊆ U → IsEllipticMatrix lam Lam (avgMat (Metric.closedBall (ratPt q) ↑r) a)

The rational-ball characterization of spatial a.e. ellipticity. For an open set U, a carrier field is a.e.-elliptic on the restricted measure of U iff all its rational-ball averages inside U are elliptic. This is the exact set equality behind the honest LocalSigmaR U-measurability of the slice event.