Control

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Deterministic local control for the lower shell tail

This file contains only the deterministic, countable good-event layer for the lower shell tail. It does not define an infinite cutoff or assert that the good event has full probability.

noncomputable def Algsuperdiff.Section3.Cutoff.localCubeControl {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) : ℝ

A nonnegative control of a shell on the origin-centered cube at scale ell. It is the exact unit-cube value norm after the corresponding spatial rescaling; the source C² shell carrier makes this finite and Borel measurable.

Equations

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

theorem Algsuperdiff.Section3.Cutoff.localCubeControl_nonneg {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) : 0 ≤ localCubeControl ell j

theorem Algsuperdiff.Section3.Cutoff.measurable_localCubeControl {d : ℕ} (ell : ℤ) : Measurable (localCubeControl ell)

theorem Algsuperdiff.Section3.Cutoff.matrixOperatorNorm_le_localCubeControl {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) : HCPolySupport.Book.Ch02.matrixOperatorNorm ((↑j).1 x) ≤ localCubeControl ell j

The local control bounds the operator norm at every point of its open cube.

theorem Algsuperdiff.Section3.Cutoff.localCubeControl_le_of_pointwise {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) (C : ℝ) (hC : ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell), HCPolySupport.Book.Ch02.matrixOperatorNorm ((↑j).1 x) ≤ C) (hC_nonneg : 0 ≤ C) : localCubeControl ell j ≤ C

A nonnegative pointwise bound controls the exact local supremum.

theorem Algsuperdiff.Section3.Cutoff.abs_entry_le_localCubeControl {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) (i k : Fin d) : |(↑j).1 x i k| ≤ localCubeControl ell j

The local control bounds every matrix entry on its corresponding open origin cube.

noncomputable def Algsuperdiff.Section3.Cutoff.lowerTailPartialSum {d : ℕ} (ell m : ℤ) (q : ℕ) (omega : ShellSeq d) : ℝ

The finite partial sum of descending-shell local controls.

Equations

• Algsuperdiff.Section3.Cutoff.lowerTailPartialSum ell m q omega = ∑ r ∈ Finset.range q, Algsuperdiff.Section3.Cutoff.localCubeControl ell (omega (m - ↑r))

theorem Algsuperdiff.Section3.Cutoff.measurable_lowerTailPartialSum {d : ℕ} (ell m : ℤ) (q : ℕ) : Measurable (lowerTailPartialSum ell m q)

def Algsuperdiff.Section3.Cutoff.LowerTailBounded {d : ℕ} (ell m : ℤ) (omega : ShellSeq d) : Prop

Bounded nonnegative partial sums, the countable formulation of descending shell summability used in the lower-tail good event.

Equations

• Algsuperdiff.Section3.Cutoff.LowerTailBounded ell m omega = ∃ (C : ℕ), ∀ (q : ℕ), Algsuperdiff.Section3.Cutoff.lowerTailPartialSum ell m q omega ≤ ↑C

theorem Algsuperdiff.Section3.Cutoff.lowerTailBounded_summable {d : ℕ} {ell m : ℤ} {omega : ShellSeq d} (h : LowerTailBounded ell m omega) : Summable fun (r : ℕ) => localCubeControl ell (omega (m - ↑r))

def Algsuperdiff.Section3.Cutoff.LowerTailGood {d : ℕ} (omega : ShellSeq d) : Prop

The deterministic lower-tail good condition: for every pair of integer scales, its nonnegative descending-shell control series has bounded partial sums.

Equations

• Algsuperdiff.Section3.Cutoff.LowerTailGood omega = ∀ (ell m : ℤ), Algsuperdiff.Section3.Cutoff.LowerTailBounded ell m omega

def Algsuperdiff.Section3.Cutoff.lowerTailGoodSet (d : ℕ) : Set (ShellSeq d)

The measurable event on which all descending local-control tails are summable.

Equations

• Algsuperdiff.Section3.Cutoff.lowerTailGoodSet d = {omega : Algsuperdiff.Section3.Cutoff.ShellSeq d | Algsuperdiff.Section3.Cutoff.LowerTailGood omega}

theorem Algsuperdiff.Section3.Cutoff.lowerTailGood_summable {d : ℕ} {omega : ShellSeq d} (h : LowerTailGood omega) (ell m : ℤ) : Summable fun (r : ℕ) => localCubeControl ell (omega (m - ↑r))

theorem Algsuperdiff.Section3.Cutoff.measurableSet_lowerTailBounded {d : ℕ} (ell m : ℤ) : MeasurableSet {omega : ShellSeq d | LowerTailBounded ell m omega}

theorem Algsuperdiff.Section3.Cutoff.measurableSet_lowerTailGoodSet (d : ℕ) : MeasurableSet (lowerTailGoodSet d)

theorem Algsuperdiff.Section3.Cutoff.lowerTailGood_tendstoUniformlyOn_finiteLowerCutoff_entry {d : ℕ} {omega : ShellSeq d} (hgood : LowerTailGood omega) (ell m : ℤ) (i k : Fin d) : TendstoUniformlyOn (fun (q : ℕ) (x : HCPolySupport.Vec d) => (finiteLowerCutoff m q omega).toFun x i k) (fun (x : HCPolySupport.Vec d) => ∑' (r : ℕ), (↑(omega (m - ↑r))).1 x i k) Filter.atTop (HCPolySupport.openCubeSet (HCPolySupport.originCube d ell))

On the good event, every matrix entry of the finite lower cutoffs converges uniformly on each open origin cube. The limit is only displayed as an internal series here; no infinite cutoff is defined in this file.