Geometry

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Corridor geometry

Formalization of the corridor geometry underlying Lemma 4.2 (l.corridor.geometry) of the high-moment paper (Armstrong–Kuusi–Loher, in preparation).

Fix a mesh size ℓ and a phase σ : Vec d. The corridor set corridorSet ℓ σ is the union over coordinates i of the width-2 slabs around the shifted lattice σ i + ℓ • ℤ. Its complement is the disjoint union of the core boxes coreBox ℓ σ k, k : Fin d → ℤ. This file records:

• corridorSet, coreBox;
• the exhaustion (corridorSet ℓ σ)ᶜ = ⋃ k, coreBox ℓ σ k;
• the sup-metric 2-separation of distinct core boxes, packaged as AreUnitSeparated;
• finiteness of the cores meeting a bounded set;
• the corridor-modified coefficient field corridorField and its algebra;
• the independence bridge to the unit-range dependence machinery.

J1–J2: the corridor set and the core boxes

def HCPolySupport.corridorSet {d : ℕ} (ℓ : ℝ) (σ : Vec d) : Set (Vec d)

The corridor set S_σ of e.corridor.definition: the points that are within (sup-)distance 1 of the shifted lattice σ i + ℓ • ℤ in some coordinate i.

Equations

• HCPolySupport.corridorSet ℓ σ = {x : HCPolySupport.Vec d | ∃ (i : Fin d) (n : ℤ), |x i - σ i - ↑n * ℓ| < 1}

def HCPolySupport.coreBox {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : Set (Vec d)

The core box indexed by k : Fin d → ℤ: the product of the intervals I_{i,k_i} = [σ_i + k_i ℓ + 1, σ_i + (k_i+1) ℓ − 1].

Equations

• HCPolySupport.coreBox ℓ σ k = Set.univ.pi fun (i : Fin d) => Set.Icc (σ i + ↑(k i) * ℓ + 1) (σ i + (↑(k i) + 1) * ℓ - 1)

theorem HCPolySupport.mem_corridorSet {d : ℕ} {ℓ : ℝ} {σ x : Vec d} : x ∈ corridorSet ℓ σ ↔ ∃ (i : Fin d) (n : ℤ), |x i - σ i - ↑n * ℓ| < 1

theorem HCPolySupport.mem_coreBox {d : ℕ} {ℓ : ℝ} {σ x : Vec d} {k : Fin d → ℤ} : x ∈ coreBox ℓ σ k ↔ ∀ (i : Fin d), σ i + ↑(k i) * ℓ + 1 ≤ x i ∧ x i ≤ σ i + (↑(k i) + 1) * ℓ - 1

J3: exhaustion of the complement by core boxes

theorem HCPolySupport.forall_one_le_abs_iff {ℓ : ℝ} (hℓ : 0 < ℓ) (t : ℝ) : (∀ (n : ℤ), 1 ≤ |t - ↑n * ℓ|) ↔ ∃ (m : ℤ), ↑m * ℓ + 1 ≤ t ∧ t ≤ (↑m + 1) * ℓ - 1

One-dimensional heart of the exhaustion: a real number t is at (sup-)distance ≥ 1 from every point of ℓ • ℤ iff it lies in one of the core intervals [m ℓ + 1, (m+1) ℓ − 1]. Needs only 0 < ℓ.

theorem HCPolySupport.compl_corridorSet_eq_iUnion_coreBox {d : ℕ} {ℓ : ℝ} (hℓ : 0 < ℓ) (σ : Vec d) : (corridorSet ℓ σ)ᶜ = ⋃ (k : Fin d → ℤ), coreBox ℓ σ k

Exhaustion (J3): the complement of the corridor set is the union of the core boxes. Needs only 0 < ℓ.

J4: sup-metric separation of distinct core boxes

theorem HCPolySupport.areUnitSeparated_coreBox {d : ℕ} {ℓ : ℝ} (hℓ : 0 ≤ ℓ) (σ : Vec d) {k k' : Fin d → ℤ} (hne : k ≠ k') : AreUnitSeparated (coreBox ℓ σ k) (coreBox ℓ σ k')

Two distinct core boxes are separated by a gap of at least 2 in some coordinate, hence (in the sup metric on Vec d) by AreUnitSeparated. Needs 0 ≤ ℓ.

J5: finiteness of the cores meeting a bounded set

theorem HCPolySupport.finite_coreBox_meets {d : ℕ} {ℓ : ℝ} (hℓ : 0 < ℓ) (σ : Vec d) {U : Set (Vec d)} (hU : Bornology.IsBounded U) : {k : Fin d → ℤ | (coreBox ℓ σ k ∩ U).Nonempty}.Finite

Finiteness (J5): only finitely many core boxes meet a bounded set U. Provided as Set.Finite; consumers can take .toFinset. Needs 0 < ℓ.

J7: the corridor-modified coefficient field

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

The identity matrix is (1, Θ)-elliptic for every Θ ≥ 1.

noncomputable def HCPolySupport.corridorField {d : ℕ} (ℓ : ℝ) (σ : Vec d) (a : CoeffField d) : CoeffField d

The corridor-modified coefficient (e.corridor.coefficient): the identity on the corridor set, and a off it.

Equations

• HCPolySupport.corridorField ℓ σ a x = if x ∈ HCPolySupport.corridorSet ℓ σ then 1 else a x

@[simp]

theorem HCPolySupport.corridorField_apply_of_mem {d : ℕ} {ℓ : ℝ} {σ : Vec d} {a : CoeffField d} {x : Vec d} (hx : x ∈ corridorSet ℓ σ) : corridorField ℓ σ a x = 1

@[simp]

theorem HCPolySupport.corridorField_apply_of_not_mem {d : ℕ} {ℓ : ℝ} {σ : Vec d} {a : CoeffField d} {x : Vec d} (hx : x ∉ corridorSet ℓ σ) : corridorField ℓ σ a x = a x

theorem HCPolySupport.corridorField_eqOn_compl {d : ℕ} (ℓ : ℝ) (σ : Vec d) (a : CoeffField d) : Set.EqOn (corridorField ℓ σ a) a (corridorSet ℓ σ)ᶜ

(J7.iii) Off the corridor set, corridorField ℓ σ a agrees with a.

theorem HCPolySupport.corridorField_isEllipticMatrix {d : ℕ} {Θ ℓ : ℝ} {σ : Vec d} {a : CoeffField d} {x : Vec d} (hΘ : 1 ≤ Θ) (hx : IsEllipticMatrix 1 Θ (a x)) : IsEllipticMatrix 1 Θ (corridorField ℓ σ a x)

(J7.i) Pointwise preservation of the ellipticity class: wherever a x is (1, Θ)-elliptic (and Θ ≥ 1), so is corridorField ℓ σ a x.

theorem HCPolySupport.corridorField_eq_add_indicator {d : ℕ} (ℓ : ℝ) (σ : Vec d) (a : CoeffField d) : corridorField ℓ σ a = fun (x : Vec d) => a x + (corridorSet ℓ σ).indicator (fun (y : Vec d) => 1 - a y) x

(J7.ii) Additive/indicator normal form, convenient for later joint measurability arguments: a_σ = a + 𝟙_{S_σ} · (Id − a).

theorem HCPolySupport.corridorField_congr_of_eqOn_compl {d : ℕ} {ℓ : ℝ} {σ : Vec d} {a a' : CoeffField d} (h : Set.EqOn a a' (corridorSet ℓ σ)ᶜ) : corridorField ℓ σ a = corridorField ℓ σ a'

(J7, restriction compatibility) corridorField ℓ σ a depends on a only through its values off the corridor set.

J8: independence bridge to unit-range dependence

theorem HCPolySupport.pairwise_areUnitSeparated_coreBox {d : ℕ} {ℓ : ℝ} (hℓ : 0 ≤ ℓ) (σ : Vec d) {ι : Type u_1} {k : ι → Fin d → ℤ} (hk : Function.Injective k) : Pairwise fun (i j : ι) => AreUnitSeparated (coreBox ℓ σ (k i)) (coreBox ℓ σ (k j))

(J8, geometric input) The core boxes of an injective family of indices are pairwise AreUnitSeparated. Needs 0 ≤ ℓ.

theorem HCPolySupport.iIndepFun_coreBox_observable {d : ℕ} {ℓ : ℝ} (hℓ : 0 ≤ ℓ) (σ : Vec d) {ι : Type u_1} {γ : ι → Type u_2} [(i : ι) → MeasurableSpace (γ i)] {k : ι → Fin d → ℤ} (hk : Function.Injective k) {P : MeasureTheory.Measure (CoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependent P) (X : (i : ι) → MeasurableRestrictionLocalObservable d (coreBox ℓ σ (k i)) (γ i)) : ProbabilityTheory.iIndepFun (fun (i : ι) => (X i).toFun) P

For an injective family of core indices, any measurable local observables supported on the corresponding cores are jointly independent under a unit-range-dependent (in the restriction sense) probability measure. This is the shape consumed by the Efron–Stein step: combine pairwise_areUnitSeparated_coreBox with the unit-range dependence machinery.