RepresentativeTransfer

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

The representative/literal transfer of the clause-(i) display

ABK26, Section 4.1. ClauseOne proves the four-term estimate pointwise in omega, at a fixed cutoff level L, for the literal carriers Support.fluxCorrectedError and real-valued right-hand families. The Section 4.1 display is stated almost surely, at the representative observables, over the supremum in L, in [0, infinity]. This module performs that transfer.

Three separate moves are involved and each is isolated below.

1. Literal to representative (indicator_observableSqSup_le). The proved Support.ae_forall_fluxCorrectedError_eq_representative gives a single probability-one event on which the literal error and its measurable representative agree simultaneously for every L >= m (the index set is countable). On that event the [0,infinity]-valued supremum fluxCorrectedErrorObservableSqSup is bounded by any uniform-in-L bound for the literal, and the indicator of the good event only lowers it.
2. Real to [0,infinity] (ofReal_tsum_le, ofReal_annDouble_le_ennDouble). This is what lets the display be stated without convergence side conditions.
3. The lattice maxima (hE2dom, hG1bdom slots). The real right-hand families of ClauseOne are upper bounds for the per-cube atoms; the display carries the honest [0,infinity]-valued suprema over the lattice index sets.

Part A -- the transport helpers

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_tsum_le {iota : Type u_1} {f : iota → ℝ} (hf : ∀ (i : iota), 0 ≤ f i) : ENNReal.ofReal (∑' (i : iota), f i) ≤ ∑' (i : iota), ENNReal.ofReal (f i)

ofReal under-approximates an infinite sum of nonnegative reals, with no summability hypothesis: a non-summable real sum is 0 by convention.

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_ite_zero (P : Prop) [Decidable P] (a : ℝ) : ENNReal.ofReal (if P then a else 0) = if P then ENNReal.ofReal a else 0

ofReal commutes with a guarded value.

theorem Algsuperdiff.Section4.Provider.Annular.ennreal_tsum_guard (b : ℤ) (g : ℤ → ENNReal) : ∑' (j : { j : ℤ // j ≤ b }), g ↑j = ∑' (j : ℤ), if j ≤ b then g j else 0

The [0,infinity]-valued sum over {j : j <= b} as a guarded sum over Z.

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_annDouble_le_ennDouble {m : ℤ} {h : ℤ → ℤ → ℝ} {H : ℤ → ℤ → ENNReal} (hh0 : ∀ (j n : ℤ), 0 ≤ h j n) (hdom : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → ENNReal.ofReal (h j n) ≤ H j n) : ENNReal.ofReal (annDouble m h) ≤ ∑' (j : { j : ℤ // j ≤ m }) (n : { n : ℤ // n ≤ ↑j - 1 }), H ↑j ↑n

The annular double sum, transported to [0,infinity]. A nonnegative real annular double sum is dominated by the corresponding iterated [0,infinity]-valued sum over the two subtypes, given a termwise domination on the annular region. No summability enters.

Part B -- the four right-hand terms at the representative observables

noncomputable def Algsuperdiff.Section4.Provider.Annular.clauseOneTermOne {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The first right-hand term of clause (i): the annular double sum of the [0,infinity]-valued lattice maxima of the squared (2,2) error atoms.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Annular.clauseOneTermThree {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The squared shell-gradient sum forming the third term of the annular bound.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Annular.clauseOneTermFour {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) : ENNReal

The fourth right-hand term of clause (i): the W^{2,infinity} block sum.

Equations

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

Part C -- the two provable dominations

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_annDouble_le_clauseOneTermOne {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) {E2 : ℤ → ℤ → ℝ} (hE0 : ∀ (j n : ℤ), 0 ≤ E2 j n) (hE2dom : ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → ENNReal.ofReal (E2 j n) ≤ ⨆ (v : ↑(Support.latticeAnnulusSet d n j (j - 1))), ENNReal.ofReal (Support.annularErrorObservable M n s (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n ↑v) omega) ^ 2)) : ENNReal.ofReal (annDouble m fun (j n : ℤ) => 3 ^ (-(↑s * ↑(m - n))) * E2 j n) ≤ clauseOneTermOne M m s omega

The first term, from the atom-level slot. The real annular double sum of ClauseOne is dominated by clauseOneTermOne as soon as each real atom family value is dominated by the [0,infinity]-valued lattice supremum -- the only genuinely missing direction, since a real supremum over a lattice index set has no proved existence lemma.

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_gradTailSq_le_clauseOneTermThree {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ENNReal.ofReal (gradTailSq M m omega) ≤ clauseOneTermThree M m omega

The third term, unconditionally. ClauseOne's gradTailSq is the square of a real l^1 tail; clauseOneTermThree is the square of the same tail formed in [0,infinity], and ofReal under-approximates it with no summability hypothesis.

Part D -- the literal-to-representative transfer of the left-hand side

theorem Algsuperdiff.Section4.Provider.Annular.indicator_observableSqSup_le {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) {Event : Set (Section3.Cutoff.CutoffSample d)} {omega : Section3.Cutoff.CutoffSample d} {B : ENNReal} (hall : ∀ (L : { L : ℤ // m ≤ L }), Support.fluxCorrectedError M (↑L) m (↑s) omega = Support.fluxCorrectedErrorRepresentative M (↑L) m s omega) (hb : omega ∈ Event → ∀ (L : ℤ), m ≤ L → ENNReal.ofReal (Support.fluxCorrectedError M L m (↑s) omega ^ 2) ≤ B) : Event.indicator (Support.fluxCorrectedErrorObservableSqSup M m s) omega ≤ B

The left-hand side, transferred. A uniform-in-L bound for the literal squared flux-corrected error on the good event bounds the indicator of the [0,infinity]-valued representative supremum, on the probability-one event where literal and representative agree for every L >= m.

Part E -- the assembled representative display

theorem Algsuperdiff.Section4.Provider.Annular.clauseOne_representative_display {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (Event : Set (Section3.Cutoff.CutoffSample d)) {C : ℝ} {E2 : Section3.Cutoff.CutoffSample d → ℤ → ℤ → ℝ} {A : Section3.Cutoff.CutoffSample d → ℤ → ℝ} (hC0 : 0 ≤ C) (hE0 : ∀ (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ), 0 ≤ E2 omega j n) (hbound : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Event → ∀ (L : ℤ), m ≤ L → IsClauseOneBound (Support.fluxCorrectedError M L m (↑s) omega ^ 2) (annDouble m fun (j n : ℤ) => 3 ^ (-(↑s * ↑(m - n))) * E2 omega j n) (M.gamma ^ 2 * |Real.log M.gamma| ^ 4) (gradTailSq M m omega) (∑' (v : ℕ), 3 ^ (-(↑s / 2) * ↑v) * A omega (m - ↑v) ^ 2) (↑s) (Section3.Disorder.cstar M) M.gamma C) (hE2dom : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → ENNReal.ofReal (E2 omega j n) ≤ ⨆ (v : ↑(Support.latticeAnnulusSet d n j (j - 1))), ENNReal.ofReal (Support.annularErrorObservable M n s (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n ↑v) omega) ^ 2)) (hG1bdom : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ENNReal.ofReal (∑' (v : ℕ), 3 ^ (-(↑s / 2) * ↑v) * A omega (m - ↑v) ^ 2) ≤ clauseOneTermFour M m s omega) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), Event.indicator (Support.fluxCorrectedErrorObservableSqSup M m s) omega ≤ ENNReal.ofReal (C * ↑s) * clauseOneTermOne M m s omega + ENNReal.ofReal (C * (↑s)⁻¹ ^ 3 * (Section3.Disorder.cstar M)⁻¹ ^ 4 * M.gamma ^ 2 * |Real.log M.gamma| ^ 4) + ENNReal.ofReal (C * (↑s)⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * clauseOneTermThree M m omega + ENNReal.ofReal (C * (↑s)⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * clauseOneTermFour M m s omega

The clause-(i) display at the representative observables, almost surely.

The pointwise literal chain of ClauseOne (hypothesis hbound, which clauseOne_bound produces at each L) is transported to the [0,infinity]-valued, almost-sure, representative-side display carried by the Section 4.1 statement.

Named slots, with their recorded gaps:

• hbound -- the pointwise chain; every input of clauseOne_bound;
• hE2dom -- domination of the real (2,2)-atom family by the [0,infinity]-valued lattice-annulus supremum;
• hG1bdom -- domination of ClauseOne's single shell sum by the display's n-then-k double block sum.