Cell discretization for the primitive-pairing estimate

This file contains the geometric and measure-theoretic interface used in paper §5.1, equations (5.1)--(5.5). It deliberately separates three facts:

• the coordinatewise floor map and its half-open cells;
• the compact-support consequence of a nonzero covariance factor;
• a finite measurable-cell lemma which turns a nonnegative integral into a lattice sum, with all measurability and integrability assumptions visible.

The last lemma is an exact decomposition/majorization statement, rather than an assumption carrying the desired lattice estimate. The analytic estimate inside one product cell (paper (5.3)) is supplied separately by Continuum/SingularChain.lean.

The ε-grid on ℝ⁴ and the torus

noncomputable def Anderson4D.floorCell (ε : ℝ) (x : R4) : Z4

Coordinatewise integer part of ε⁻¹x, paper §5.1.

Equations

• Anderson4D.floorCell ε x i = ⌊ε⁻¹ * x i⌋

def Anderson4D.cellRepresentative (ε : ℝ) (y : Z4) : R4

The lower-left representative εy of the cell indexed by y.

Equations

• Anderson4D.cellRepresentative ε y i = ε * ↑(y i)

def Anderson4D.euclideanCell (ε : ℝ) (y : Z4) : Set R4

The half-open Euclidean cell εy ≤ x < ε(y+1), coordinatewise.

Equations

• Anderson4D.euclideanCell ε y = Set.univ.pi fun (i : Fin Anderson4D.dim) => Set.Ico (ε * ↑(y i)) (ε * (↑(y i) + 1))

theorem Anderson4D.measurableSet_euclideanCell (ε : ℝ) (y : Z4) : MeasurableSet (euclideanCell ε y)

theorem Anderson4D.mem_euclideanCell_iff_floorCell {ε : ℝ} (hε : 0 < ε) (x : R4) (y : Z4) : x ∈ euclideanCell ε y ↔ floorCell ε x = y

On a positive grid, membership in the half-open cell is exactly the coordinatewise floor equation.

theorem Anderson4D.norm_sub_cellRepresentative_lt {ε : ℝ} (hε : 0 < ε) (x : R4) : ‖x - cellRepresentative ε (floorCell ε x)‖ < ε

A point is within one mesh size (in the fixed sup norm) of its cell representative.

theorem Anderson4D.norm_sub_lt_two_mul_of_floorCell_eq {ε : ℝ} (hε : 0 < ε) {x x' : R4} (hcell : floorCell ε x = floorCell ε x') : ‖x - x'‖ < 2 * ε

Two points in the same floor cell are at sup-distance < 2ε. The harmless factor two is retained to make the triangle argument robust.

theorem Anderson4D.norm_cellRepresentative_sub (ε : ℝ) (y y' : Z4) : ‖cellRepresentative ε y - cellRepresentative ε y'‖ = |ε| * znorm (y - y')

The distance between cell representatives is exactly the mesh size times the fixed lattice sup norm.

theorem Anderson4D.norm_sub_le_cell_lattice {ε : ℝ} (hε : 0 < ε) {x x' : R4} {y y' : Z4} (hxcell : floorCell ε x = y) (hx'cell : floorCell ε x' = y') : ‖x - x'‖ < ε * znorm (y - y') + 2 * ε

Cell/lattice distance comparison, upper direction.

theorem Anderson4D.cell_lattice_le_norm_sub {ε : ℝ} (hε : 0 < ε) {x x' : R4} {y y' : Z4} (hxcell : floorCell ε x = y) (hx'cell : floorCell ε x' = y') : ε * znorm (y - y') < ‖x - x'‖ + 2 * ε

Cell/lattice distance comparison, lower direction.

noncomputable def Anderson4D.torusFloorCell (ε : ℝ) (z : T4) : Z4

The torus cell index uses the canonical lift in [-π,π)⁴.

Equations

• Anderson4D.torusFloorCell ε z = Anderson4D.floorCell ε (Anderson4D.torusLift z)

def Anderson4D.torusCell (ε : ℝ) (y : Z4) : Set T4

The measurable torus cell carrying a fixed floor index.

Equations

• Anderson4D.torusCell ε y = Anderson4D.torusFloorCell ε ⁻¹' {y}

theorem Anderson4D.measurable_torusFloorCell (ε : ℝ) : Measurable (torusFloorCell ε)

theorem Anderson4D.measurableSet_torusCell (ε : ℝ) (y : Z4) : MeasurableSet (torusCell ε y)

@[simp]

theorem Anderson4D.mem_torusCell (ε : ℝ) (z : T4) (y : Z4) : z ∈ torusCell ε y ↔ torusFloorCell ε z = y

theorem Anderson4D.torusCell_pairwiseDisjoint (ε : ℝ) : Set.univ.Pairwise fun (y y' : Z4) => Disjoint (torusCell ε y) (torusCell ε y')

noncomputable def Anderson4D.torusGridRadius (ε : ℝ) : ℤ

Integer half-width of the finite grid met by the canonical fundamental cube. It is comparable to ε⁻¹; dyadic enlargement to the paper's M is a later harmless monotonicity step.

Equations

• Anderson4D.torusGridRadius ε = ⌈Real.pi / ε⌉

noncomputable def Anderson4D.torusGrid (ε : ℝ) : Finset Z4

The finite box ℤ⁴ ∩ [-⌈π/ε⌉,⌈π/ε⌉]⁴.

Equations

• Anderson4D.torusGrid ε = Fintype.piFinset fun (x : Fin Anderson4D.dim) => Finset.Icc (-Anderson4D.torusGridRadius ε) (Anderson4D.torusGridRadius ε)

theorem Anderson4D.torusFloorCell_mem_torusGrid {ε : ℝ} (hε : 0 < ε) (z : T4) : torusFloorCell ε z ∈ torusGrid ε

Every canonical torus floor index lies in the finite grid box.

Compact support of η and the periodized covariance

theorem Anderson4D.SmoothCutoff.norm_lt_two_radius_of_eta_ne_zero (ρ : SmoothCutoff) {x : R4} (hx : ρ.eta x ≠ 0) : ‖x‖ < 2 * ρ.radius

A nonzero convolution value lies in the radius-2R support of η = ρ * ρ. This uses the cutoff support itself, not an abstract support hypothesis on η.

noncomputable def Anderson4D.periodicDisplacement (z : T4) (k : Z4) : R4

A lifted displacement, translated by a period vector.

Equations

• Anderson4D.periodicDisplacement z k i = Anderson4D.torusLift z i + 2 * Real.pi * ↑(k i)

noncomputable def Anderson4D.periodizeR4 (x : R4) : T4

Coordinatewise quotient map ℝ⁴ → 𝕋⁴.

Equations

• Anderson4D.periodizeR4 x i = ↑(x i)

theorem Anderson4D.periodizeR4_periodicDisplacement (z : T4) (k : Z4) : periodizeR4 (periodicDisplacement z k) = z

Adding an integer period does not change the represented torus displacement.

theorem Anderson4D.SmoothCutoff.exists_periodicDisplacement_of_etaEpsT4_ne_zero (ρ : SmoothCutoff) {ε : ℝ} {z : T4} (hε : ε ≠ 0) (hz : ρ.etaEpsT4 ε z ≠ 0) : ∃ (k : Z4), ‖periodicDisplacement z k‖ < 2 * ρ.radius * |ε|

Nonvanishing of the periodized covariance produces an actual period translate on which the Euclidean covariance is supported. No summability assumption is hidden here: if every summand vanished, the tsum would be the tsum of the zero family.

structure Anderson4D.PairedCellConstraint (ρ : SmoothCutoff) (ε : ℝ) (z w : T4) (y : Z4) : Prop

The exact paired-cell constraint extracted from the support of one η_ε factor. It records the cell chosen at the first endpoint and the small periodic displacement of the paired endpoint; no assertion is made that the canonical floor indices of both endpoints coincide (which is false near cell and torus boundaries).

• first_cell : torusFloorCell ε z = y
• periodic_support : ∃ (k : Z4), ‖periodicDisplacement (z - w) k‖ < 2 * ρ.radius * |ε|

noncomputable def Anderson4D.pairedEuclideanRepresentative (z w : T4) (k : Z4) : R4

A Euclidean representative of the paired endpoint obtained by subtracting the supported displacement from the canonical representative of the first endpoint.

Equations

• Anderson4D.pairedEuclideanRepresentative z w k = Anderson4D.torusLift z - Anderson4D.periodicDisplacement (z - w) k

theorem Anderson4D.periodizeR4_pairedEuclideanRepresentative (z w : T4) (k : Z4) : periodizeR4 (pairedEuclideanRepresentative z w k) = w

theorem Anderson4D.PairedCellConstraint.exists_representative_near_cell {ρ : SmoothCutoff} {ε : ℝ} (hε : 0 < ε) {z w : T4} {y : Z4} (h : PairedCellConstraint ρ ε z w y) : ∃ (wrep : R4), periodizeR4 wrep = w ∧ ‖wrep - cellRepresentative ε y‖ < (1 + 2 * ρ.radius) * ε

Paper §5.1's concrete paired-cell conclusion: if z lies in cell y and the covariance support relates z to w, then w has a Euclidean representative within (1+2R)ε of the same point εy.

theorem Anderson4D.SmoothCutoff.pairedCellConstraint_of_etaEpsT4_ne_zero (ρ : SmoothCutoff) {ε : ℝ} (hε : ε ≠ 0) (z w : T4) (hη : ρ.etaEpsT4 ε (z - w) ≠ 0) : PairedCellConstraint ρ ε z w (torusFloorCell ε z)

Pairing-compatible assignments

def Anderson4D.pairingAnchor {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin m) : Fin m

The endpoint chosen to index a pair: the smaller of i and κ i. Singles are fixed.

Equations

• Anderson4D.pairingAnchor κ i = if i ≤ κ i then i else κ i

theorem Anderson4D.pairingAnchor_apply {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin m) : pairingAnchor κ (κ i) = pairingAnchor κ i

noncomputable def Anderson4D.pairedCellAssignment {m : ℕ} (κ : PartialPairing (Fin m)) (ε : ℝ) (x : Fin m → T4) : Fin m → Z4

The lattice label used in (5.2): choose a floor cell only at the smaller endpoint of every pair and copy that label to its mate.

Equations

• Anderson4D.pairedCellAssignment κ ε x i = Anderson4D.torusFloorCell ε (x (Anderson4D.pairingAnchor κ i))

theorem Anderson4D.pairedCellAssignment_apply {m : ℕ} (κ : PartialPairing (Fin m)) (ε : ℝ) (x : Fin m → T4) (i : Fin m) : pairedCellAssignment κ ε x (κ i) = pairedCellAssignment κ ε x i

The copied labels obey yᵢ = y_{κ(i)} exactly.

def Anderson4D.RespectsPairing {m : ℕ} (κ : PartialPairing (Fin m)) (y : Fin m → Z4) : Prop

Predicate cutting out precisely the copied-label constraint in the quantification following paper (5.5).

Equations

• Anderson4D.RespectsPairing κ y = ∀ (i : Fin m), y (κ i) = y i

@[implicit_reducible]

instance Anderson4D.instDecidableRespectsPairing {m : ℕ} (κ : PartialPairing (Fin m)) (y : Fin m → Z4) : Decidable (RespectsPairing κ y)

Equations

• Anderson4D.instDecidableRespectsPairing κ y = Anderson4D.instDecidableRespectsPairing._aux_1 κ y

theorem Anderson4D.pairedCellAssignment_respectsPairing {m : ℕ} (κ : PartialPairing (Fin m)) (ε : ℝ) (x : Fin m → T4) : RespectsPairing κ (pairedCellAssignment κ ε x)

theorem Anderson4D.measurable_pairedCellAssignment {m : ℕ} (κ : PartialPairing (Fin m)) (ε : ℝ) : Measurable (pairedCellAssignment κ ε)

theorem Anderson4D.pairedCellAssignment_mem_piFinset {m : ℕ} (κ : PartialPairing (Fin m)) {ε : ℝ} (hε : 0 < ε) (x : Fin m → T4) : pairedCellAssignment κ ε x ∈ Fintype.piFinset fun (x : Fin m) => torusGrid ε

Every copied assignment lies in the finite product box.

theorem Anderson4D.pairedCellConstraints_of_covariance_ne_zero {m : ℕ} (ρ : SmoothCutoff) (κ : PartialPairing (Fin m)) {ε : ℝ} (hε : ε ≠ 0) (x : Fin m → T4) (hη : ∀ i < κ i, ρ.etaEpsT4 ε (x i - x (κ i)) ≠ 0) (i : Fin m) : i < κ i → PairedCellConstraint ρ ε (x i) (x (κ i)) (pairedCellAssignment κ ε x i)

Nonvanishing covariance at every (smaller) paired endpoint gives the paper's support constraint at every selected cell. The conclusion keeps the actual torus variables and periodic translate explicit.

A finite measurable-cell compression lemma

structure Anderson4D.FiniteMeasurableCells (X : Type u_1) (ι : Type u_2) [MeasurableSpace X] [DecidableEq ι] : Type (max u_1 u_2)

A finite measurable partition encoded by an index map. indices contains the range of index; the fibers are measurable. The formulation avoids quotienting by null sets and is convenient for product cells.

• indices : Finset ι
• index : X → ι
• range_subset (x : X) : self.index x ∈ self.indices
• measurable_fiber (i : ι) : MeasurableSet (self.index ⁻¹' {i})

theorem Anderson4D.FiniteMeasurableCells.pairwiseDisjoint {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] [DecidableEq ι] (P : FiniteMeasurableCells X ι) : (↑P.indices).Pairwise fun (i j : ι) => Disjoint (P.index ⁻¹' {i}) (P.index ⁻¹' {j})

Fibers belonging to different indices are disjoint.

theorem Anderson4D.FiniteMeasurableCells.iUnion_fibers {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] [DecidableEq ι] (P : FiniteMeasurableCells X ι) : ⋃ i ∈ P.indices, P.index ⁻¹' {i} = Set.univ

The selected fibers cover the whole space.

theorem Anderson4D.FiniteMeasurableCells.integral_le_measure_mul_sum {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] [DecidableEq ι] (P : FiniteMeasurableCells X ι) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (f : X → ℝ) (B : ι → ℝ) (R : ι → Prop) [DecidablePred R] (V : ℝ) (hf : MeasureTheory.Integrable f μ) (hf_nonneg : ∀ᵐ (x : X) ∂μ, 0 ≤ f x) (hB_nonneg : ∀ i ∈ P.indices, 0 ≤ B i) (hmajor : ∀ i ∈ P.indices, ∀ (x : X), P.index x = i → f x ≤ B i) (hsupport : ∀ i ∈ P.indices, ¬R i → ∀ᵐ (x : X) ∂μ.restrict (P.index ⁻¹' {i}), f x = 0) (hvol : ∀ i ∈ P.indices, (μ (P.index ⁻¹' {i})).toReal ≤ V) : ∫ (x : X), f x ∂μ ≤ V * ∑ i ∈ P.indices with R i, B i

Finite-cell integral compression.

Let f ≥ 0 be integrable. On the fiber indexed by i, suppose f ≤ B i; suppose also that this fiber has real measure at most V. Then the integral is bounded by V times the finite lattice sum of B. An optional predicate R restricts the sum: f must vanish on fibers outside R. These are precisely the explicit analytic, support, and measurability obligations needed when applying the lemma to (5.2).

theorem Anderson4D.FiniteMeasurableCells.integral_le_activeMeasure_mul_sum {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] [DecidableEq ι] (P : FiniteMeasurableCells X ι) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (f : X → ℝ) (B : ι → ℝ) (R : ι → Prop) [DecidablePred R] (active : ι → Set X) (V : ℝ) (hf : MeasureTheory.Integrable f μ) (hB_nonneg : ∀ i ∈ P.indices, 0 ≤ B i) (hactive : ∀ i ∈ P.indices, MeasurableSet (active i)) (hmajor : ∀ i ∈ P.indices, ∀ (x : X), P.index x = i → x ∈ active i → f x ≤ B i) (hvanish : ∀ i ∈ P.indices, ∀ᵐ (x : X) ∂μ, x ∈ P.index ⁻¹' {i} \ (P.index ⁻¹' {i} ∩ active i) → f x = 0) (hsupport : ∀ i ∈ P.indices, ¬R i → ∀ᵐ (x : X) ∂μ.restrict (P.index ⁻¹' {i}), f x = 0) (hvol : ∀ i ∈ P.indices, (μ (P.index ⁻¹' {i} ∩ active i)).toReal ≤ V) : ∫ (x : X), f x ∂μ ≤ V * ∑ i ∈ P.indices with R i, B i

Variant of integral_le_measure_mul_sum with an effective support inside every cell. This is the form used in (5.2): the floor cell controls the chosen endpoint, while compact support of η_ε cuts the paired endpoint down to another O(ε) neighbourhood. Consequently hvol measures the intersection with active i, not the whole (too large) floor fiber.

theorem Anderson4D.FiniteMeasurableCells.integral_le_sum_of_cellIntegrals {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] [DecidableEq ι] (P : FiniteMeasurableCells X ι) (μ : MeasureTheory.Measure X) (f : X → ℝ) (B : ι → ℝ) (R : ι → Prop) [DecidablePred R] (hf : MeasureTheory.Integrable f μ) (hsupport : ∀ i ∈ P.indices, ¬R i → ∀ᵐ (x : X) ∂μ.restrict (P.index ⁻¹' {i}), f x = 0) (hcell : ∀ i ∈ P.indices, R i → ∫ (x : X) in P.index ⁻¹' {i}, f x ∂μ ≤ B i) : ∫ (x : X), f x ∂μ ≤ ∑ i ∈ P.indices with R i, B i

Cell-integral form of the compression lemma. This is the most direct consumer of paper (5.3): once the integral over each cell is bounded, the finite disjoint decomposition simply sums those bounds.

The concrete finite cell family used by the pairing reduction.

noncomputable def Anderson4D.pairedTorusGridCells {m : ℕ} (κ : PartialPairing (Fin m)) (ε : ℝ) (hε : 0 < ε) : FiniteMeasurableCells (Fin m → T4) (Fin m → Z4)

Finite measurable cells indexed by copied pair labels.

Equations

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

The (5.5) lattice summand

def Anderson4D.latticeBracketSq (x y : Z4) : ℝ

Japanese bracket squared in the project's fixed lattice norm: ⟨x-y⟩² = 1 + |x-y|².

Equations

• Anderson4D.latticeBracketSq x y = 1 + Anderson4D.znorm (x - y) ^ 2

noncomputable def Anderson4D.reductionWeight (m : ℕ) (y : Fin (m + 1) → Z4) : ℝ

The exact nonnegative lattice weight displayed in (5.5): max_{i,j} ⟨yᵢ-yⱼ⟩² · ∏ⱼ ⟨yⱼ-yⱼ₊₁⟩⁻². The input is indexed by Fin (m+1), so the maximum is nonempty. In the paper one applies this with m+1 = 2n ≥ 4.

Equations

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

theorem Anderson4D.latticeBracketSq_nonneg (x y : Z4) : 0 ≤ latticeBracketSq x y

theorem Anderson4D.reductionWeight_nonneg (m : ℕ) (y : Fin (m + 1) → Z4) : 0 ≤ reductionWeight m y

theorem Anderson4D.integral_le_reductionWeight_sum_of_cellIntegrals (m : ℕ) (κ : PartialPairing (Fin (m + 1))) {ε : ℝ} (hε : 0 < ε) (μ : MeasureTheory.Measure (Fin (m + 1) → T4)) (f : (Fin (m + 1) → T4) → ℝ) (C : ℝ) (hf : MeasureTheory.Integrable f μ) (hcell : ∀ y ∈ Fintype.piFinset fun (x : Fin (m + 1)) => torusGrid ε, RespectsPairing κ y → ∫ (x : Fin (m + 1) → T4) in pairedCellAssignment κ ε ⁻¹' {y}, f x ∂μ ≤ C * reductionWeight m y) : ∫ (x : Fin (m + 1) → T4), f x ∂μ ≤ C * ∑ y ∈ Fintype.piFinset fun (x : Fin (m + 1)) => torusGrid ε with (RespectsPairing κ) y, reductionWeight m y

Direct cell-integral form of (5.2) → (5.5).

This is the paper-faithful consumer of (5.3). The hypothesis hcell is exactly the estimate after integrating all variables over one copied-pair cell; summing the disjoint floor cells produces the finite (5.5) sum. The constraint y_{κ(i)} = y_i is not assumed for actual cells: it is proved by pairedCellAssignment_respectsPairing, so all other summands have empty fibers and disappear.

theorem Anderson4D.integral_le_reductionWeight_latticeSum (m : ℕ) (κ : PartialPairing (Fin (m + 1))) {ε : ℝ} (hε : 0 < ε) (μ : MeasureTheory.Measure (Fin (m + 1) → T4)) [MeasureTheory.IsFiniteMeasure μ] (f : (Fin (m + 1) → T4) → ℝ) (active : (Fin (m + 1) → Z4) → Set (Fin (m + 1) → T4)) (C V : ℝ) (hf : MeasureTheory.Integrable f μ) (hC : 0 ≤ C) (hactive : ∀ y ∈ Fintype.piFinset fun (x : Fin (m + 1)) => torusGrid ε, MeasurableSet (active y)) (hmajor : ∀ y ∈ Fintype.piFinset fun (x : Fin (m + 1)) => torusGrid ε, ∀ (x : Fin (m + 1) → T4), pairedCellAssignment κ ε x = y → x ∈ active y → f x ≤ C * reductionWeight m y) (hvanish : ∀ y ∈ Fintype.piFinset fun (x : Fin (m + 1)) => torusGrid ε, ∀ᵐ (x : Fin (m + 1) → T4) ∂μ, x ∈ pairedCellAssignment κ ε ⁻¹' {y} \ (pairedCellAssignment κ ε ⁻¹' {y} ∩ active y) → f x = 0) (hvol : ∀ y ∈ Fintype.piFinset fun (x : Fin (m + 1)) => torusGrid ε, (μ (pairedCellAssignment κ ε ⁻¹' {y} ∩ active y)).toReal ≤ V) : ∫ (x : Fin (m + 1) → T4), f x ∂μ ≤ V * C * ∑ y ∈ Fintype.piFinset fun (x : Fin (m + 1)) => torusGrid ε with (RespectsPairing κ) y, reductionWeight m y

Reusable (5.2) → (5.5) compression.

For 2n = m+1 variables, assume the analytic work has provided:

• an effective support active y inside each copied-pair cell;
• a uniform active-cell measure bound V;
• the pointwise cell bound f ≤ C · reductionWeight.

Then the continuous integral is bounded by the exact finite lattice sum from (5.5), restricted by y_{κ(i)} = y_i. Measurability, integrability, support-vanishing, and cell-volume hypotheses are all explicit. In the paper, compact support of η_ε supplies active (see pairedCellConstraints_of_covariance_ne_zero) and (5.3)--(5.4) supply the pointwise/volume ledger.