Fixed-truncation limits from Proposition 3.6

This file carries out the analytic normalization used in paper (3.36)--(3.37). The factor λ_ε^r in Proposition 3.6 is cancelled only on the positive side of zero, where λ_ε > 0.

def Anderson4D.FixedTruncationAtom.prop36Mode {s B : ℕ} (modes : Fin s → Z4 × Z4) (a : FixedTruncationAtom s B) : (Z4 × Z4) × ℕ

Proposition 3.6 mode/order data attached to one real-expansion atom.

Equations

• Anderson4D.FixedTruncationAtom.prop36Mode modes a = (Anderson4D.FixedTruncationAtom.modePair modes a, a.order)

def Anderson4D.fixedTruncationAssignmentModes {s B r : ℕ} (modes : Fin s → Z4 × Z4) (assignment : Fin r → FixedTruncationAtom s B) : Fin r → (Z4 × Z4) × ℕ

The Proposition 3.6 family attached to an assignment of atoms.

Equations

• Anderson4D.fixedTruncationAssignmentModes modes assignment i = Anderson4D.FixedTruncationAtom.prop36Mode modes (assignment i)

theorem Anderson4D.fixedTruncationAssignmentModes_valid {s B B' r : ℕ} (hBB' : B ≤ B') (modes : Fin s → Z4 × Z4) (assignment : Fin r → FixedTruncationAtom s B) (i : Fin r) : 1 ≤ (fixedTruncationAssignmentModes modes assignment i).2 ∧ (fixedTruncationAssignmentModes modes assignment i).2 ≤ B'

structure Anderson4D.Prop36FullData (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) (B r : ℕ) : Type

All clauses of Proposition 3.6 at one fixed order bound and family size, retaining the single coefficient table shared by every mode family.

• coeff : ℕ → ℕ → ℝ
• constant : ℝ
• constant_pos : 0 < self.constant
• coeff_bound (m₁ m₂ : ℕ) : 1 ≤ m₁ → 1 ≤ m₂ → |self.coeff m₁ m₂| ≤ self.constant * (self.constant * lam) ^ (m₁ + m₂ - 2)
• sum_identity (m : ℕ) : 2 ≤ m → positiveAntidiagonalSum self.coeff m = if Even m then prop36MomentBase lam ^ (m - 2) else 0
• family_clause (modes : Fin r → (Z4 × Z4) × ℕ) : (∀ (j : Fin r), 1 ≤ (modes j).2 ∧ (modes j).2 ≤ B) → (∀ (ε : ℝ) (j : Fin r), Measurable (pmCoeff M ρ lam ε (modes j).2 (modes j).1.1 (modes j).1.2)) ∧ (∀ (ε : ℝ), MeasureTheory.Integrable (fun (ω : M.Ω) => ∏ j : Fin r, pmCoeff M ρ lam ε (modes j).2 (modes j).1.1 (modes j).1.2 ω) MeasureTheory.volume) ∧ ∃ (C' : ℝ), 0 < C' ∧ ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖(∫ (ω : M.Ω), ∏ j : Fin r, pmCoeff M ρ lam ε (modes j).2 (modes j).1.1 (modes j).1.2 ω) - ∑ κ : PartialPairing (Fin r) with κ.IsFull, ∏ i ∈ κ.pairSupport with i < κ i, ∫ (ω : M.Ω), pmCoeff M ρ lam ε (modes i).2 (modes i).1.1 (modes i).1.2 ω * pmCoeff M ρ lam ε (modes (κ i)).2 (modes (κ i)).1.1 (modes (κ i)).1.2 ω‖ ≤ C' * lamEps lam ε ^ r / |Real.log ε| ∧ ∀ (m₁ m₂ : ℕ), 1 ≤ m₁ → m₁ ≤ B → 1 ≤ m₂ → m₂ ≤ B → ∀ (α₁ β₁ α₂ β₂ : Z4), ‖(∫ (ω : M.Ω), pmCoeff M ρ lam ε m₁ α₁ β₁ ω * pmCoeff M ρ lam ε m₂ α₂ β₂ ω) - (lamEps lam ε ^ 2 * self.coeff m₁ m₂) • fourPointHCoeff α₁ β₁ α₂ β₂‖ ≤ C' * lamEps lam ε ^ 2 / |Real.log ε|

noncomputable def Anderson4D.Prop36.fullData {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (B r : ℕ) : Prop36FullData M ρ lam B r

Canonical full Proposition 3.6 data at (B,r). Both the coefficient table and the uniform geometric constant are selected by the shared external-input choice functions.

Equations

• hP36.fullData B r = { coeff := hP36.coefficientTable B r, constant := hP36.boundConstant, constant_pos := ⋯, coeff_bound := ⋯, sum_identity := ⋯, family_clause := ⋯ }

theorem Anderson4D.Prop36.nonempty_fullData {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (B r : ℕ) : Nonempty (Prop36FullData M ρ lam B r)

Proposition 3.6 supplies full data at every (B,r).

theorem Anderson4D.tendsto_inv_lamEps_pow_mul_of_norm_sub_le {f : ℝ → ℂ} {z : ℂ} {lam C : ℝ} {r : ℕ} (hlam : 0 < lam) (hbound : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖f ε - ↑(lamEps lam ε) ^ r * z‖ ≤ C * lamEps lam ε ^ r / |Real.log ε|) : Filter.Tendsto (fun (ε : ℝ) => (↑(lamEps lam ε))⁻¹ ^ r * f ε) (nhdsWithin 0 (Set.Ioi 0)) (nhds z)

An O(λ_ε^r / |log ε|) complex error becomes o(1) after normalization by λ_ε^r.

theorem Anderson4D.tendsto_inv_lamEps_pow_mul_sub_of_norm_sub_le {f g : ℝ → ℂ} {lam C : ℝ} {r : ℕ} (hlam : 0 < lam) (hbound : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖f ε - g ε‖ ≤ C * lamEps lam ε ^ r / |Real.log ε|) : Filter.Tendsto (fun (ε : ℝ) => (↑(lamEps lam ε))⁻¹ ^ r * (f ε - g ε)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Difference form of the preceding normalization lemma.

theorem Anderson4D.tendsto_normalized_pmCoeff_pair (M : NoiseModel) (ρ : SmoothCutoff) {lam C X : ℝ} (hlam : 0 < lam) (m₁ m₂ : ℕ) (α₁ β₁ α₂ β₂ : Z4) (hbound : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖(∫ (ω : M.Ω), pmCoeff M ρ lam ε m₁ α₁ β₁ ω * pmCoeff M ρ lam ε m₂ α₂ β₂ ω) - (lamEps lam ε ^ 2 * X) • fourPointHCoeff α₁ β₁ α₂ β₂‖ ≤ C * lamEps lam ε ^ 2 / |Real.log ε|) : Filter.Tendsto (fun (ε : ℝ) => (↑(lamEps lam ε))⁻¹ ^ 2 * ∫ (ω : M.Ω), pmCoeff M ρ lam ε m₁ α₁ β₁ ω * pmCoeff M ρ lam ε m₂ α₂ β₂ ω) (nhdsWithin 0 (Set.Ioi 0)) (nhds (↑X * fourPointHCoeff α₁ β₁ α₂ β₂))

Covariance clause (3.27), after division by λ_ε².

noncomputable def Anderson4D.prop36PairMoment (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) {r : ℕ} (family : Fin r → (Z4 × Z4) × ℕ) (i j : Fin r) : ℂ

One pair covariance from a Proposition 3.6 family.

Equations

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

noncomputable def Anderson4D.prop36PairLimit (𝔛 : ℕ → ℕ → ℝ) {r : ℕ} (family : Fin r → (Z4 × Z4) × ℕ) (i j : Fin r) : ℂ

The limiting pair covariance specified by one coefficient table.

Equations

• Anderson4D.prop36PairLimit 𝔛 family i j = ↑(𝔛 (family i).2 (family j).2) * Anderson4D.fourPointHCoeff (family i).1.1 (family i).1.2 (family j).1.1 (family j).1.2

theorem Anderson4D.two_mul_card_fullPairingRepresentatives {r : ℕ} (κ : PartialPairing (Fin r)) (hκ : κ.IsFull) : 2 * {i ∈ κ.pairSupport | i < κ i}.card = r

A full pairing has one selected lower endpoint per pair, hence twice the number of displayed covariance factors is the family size.

theorem Anderson4D.tendsto_normalized_prop36PairMoment (M : NoiseModel) (ρ : SmoothCutoff) {lam C : ℝ} (hlam : 0 < lam) {B r : ℕ} (𝔛 : ℕ → ℕ → ℝ) (family : Fin r → (Z4 × Z4) × ℕ) (hvalid : ∀ (i : Fin r), 1 ≤ (family i).2 ∧ (family i).2 ≤ B) (hcov : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m₁ m₂ : ℕ), 1 ≤ m₁ → m₁ ≤ B → 1 ≤ m₂ → m₂ ≤ B → ∀ (α₁ β₁ α₂ β₂ : Z4), ‖(∫ (ω : M.Ω), pmCoeff M ρ lam ε m₁ α₁ β₁ ω * pmCoeff M ρ lam ε m₂ α₂ β₂ ω) - (lamEps lam ε ^ 2 * 𝔛 m₁ m₂) • fourPointHCoeff α₁ β₁ α₂ β₂‖ ≤ C * lamEps lam ε ^ 2 / |Real.log ε|) (i j : Fin r) : Filter.Tendsto (fun (ε : ℝ) => (↑(lamEps lam ε))⁻¹ ^ 2 * prop36PairMoment M ρ lam ε family i j) (nhdsWithin 0 (Set.Ioi 0)) (nhds (prop36PairLimit 𝔛 family i j))

Every normalized pair covariance in a fixed Proposition 3.6 family converges to the covariance prescribed by its coefficient table.

theorem Anderson4D.tendsto_normalized_fullPairingProduct (M : NoiseModel) (ρ : SmoothCutoff) {lam C : ℝ} (hlam : 0 < lam) {B r : ℕ} (𝔛 : ℕ → ℕ → ℝ) (family : Fin r → (Z4 × Z4) × ℕ) (hvalid : ∀ (i : Fin r), 1 ≤ (family i).2 ∧ (family i).2 ≤ B) (hcov : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m₁ m₂ : ℕ), 1 ≤ m₁ → m₁ ≤ B → 1 ≤ m₂ → m₂ ≤ B → ∀ (α₁ β₁ α₂ β₂ : Z4), ‖(∫ (ω : M.Ω), pmCoeff M ρ lam ε m₁ α₁ β₁ ω * pmCoeff M ρ lam ε m₂ α₂ β₂ ω) - (lamEps lam ε ^ 2 * 𝔛 m₁ m₂) • fourPointHCoeff α₁ β₁ α₂ β₂‖ ≤ C * lamEps lam ε ^ 2 / |Real.log ε|) (κ : PartialPairing (Fin r)) (hκ : κ.IsFull) : Filter.Tendsto (fun (ε : ℝ) => (↑(lamEps lam ε))⁻¹ ^ r * ∏ i ∈ κ.pairSupport with i < κ i, prop36PairMoment M ρ lam ε family i (κ i)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∏ i ∈ κ.pairSupport with i < κ i, prop36PairLimit 𝔛 family i (κ i)))

Termwise full-pairing limit after the exact λ_ε^r normalization ledger.

theorem Anderson4D.tendsto_normalized_fullPairingSum (M : NoiseModel) (ρ : SmoothCutoff) {lam C : ℝ} (hlam : 0 < lam) {B r : ℕ} (𝔛 : ℕ → ℕ → ℝ) (family : Fin r → (Z4 × Z4) × ℕ) (hvalid : ∀ (i : Fin r), 1 ≤ (family i).2 ∧ (family i).2 ≤ B) (hcov : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m₁ m₂ : ℕ), 1 ≤ m₁ → m₁ ≤ B → 1 ≤ m₂ → m₂ ≤ B → ∀ (α₁ β₁ α₂ β₂ : Z4), ‖(∫ (ω : M.Ω), pmCoeff M ρ lam ε m₁ α₁ β₁ ω * pmCoeff M ρ lam ε m₂ α₂ β₂ ω) - (lamEps lam ε ^ 2 * 𝔛 m₁ m₂) • fourPointHCoeff α₁ β₁ α₂ β₂‖ ≤ C * lamEps lam ε ^ 2 / |Real.log ε|) : Filter.Tendsto (fun (ε : ℝ) => (↑(lamEps lam ε))⁻¹ ^ r * ∑ κ : PartialPairing (Fin r) with κ.IsFull, ∏ i ∈ κ.pairSupport with i < κ i, prop36PairMoment M ρ lam ε family i (κ i)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∑ κ : PartialPairing (Fin r) with κ.IsFull, ∏ i ∈ κ.pairSupport with i < κ i, prop36PairLimit 𝔛 family i (κ i)))

Finite sum of all normalized full-pairing products.

theorem Anderson4D.tendsto_normalized_prop36Product (M : NoiseModel) (ρ : SmoothCutoff) {lam C : ℝ} (hlam : 0 < lam) {B r : ℕ} (𝔛 : ℕ → ℕ → ℝ) (family : Fin r → (Z4 × Z4) × ℕ) (hvalid : ∀ (i : Fin r), 1 ≤ (family i).2 ∧ (family i).2 ≤ B) (hfactor : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖(∫ (ω : M.Ω), ∏ j : Fin r, pmCoeff M ρ lam ε (family j).2 (family j).1.1 (family j).1.2 ω) - ∑ κ : PartialPairing (Fin r) with κ.IsFull, ∏ i ∈ κ.pairSupport with i < κ i, prop36PairMoment M ρ lam ε family i (κ i)‖ ≤ C * lamEps lam ε ^ r / |Real.log ε|) (hcov : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m₁ m₂ : ℕ), 1 ≤ m₁ → m₁ ≤ B → 1 ≤ m₂ → m₂ ≤ B → ∀ (α₁ β₁ α₂ β₂ : Z4), ‖(∫ (ω : M.Ω), pmCoeff M ρ lam ε m₁ α₁ β₁ ω * pmCoeff M ρ lam ε m₂ α₂ β₂ ω) - (lamEps lam ε ^ 2 * 𝔛 m₁ m₂) • fourPointHCoeff α₁ β₁ α₂ β₂‖ ≤ C * lamEps lam ε ^ 2 / |Real.log ε|) : Filter.Tendsto (fun (ε : ℝ) => (↑(lamEps lam ε))⁻¹ ^ r * ∫ (ω : M.Ω), ∏ j : Fin r, pmCoeff M ρ lam ε (family j).2 (family j).1.1 (family j).1.2 ω) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∑ κ : PartialPairing (Fin r) with κ.IsFull, ∏ i ∈ κ.pairSupport with i < κ i, prop36PairLimit 𝔛 family i (κ i)))

Proposition 3.6 Wick factorization (3.26) plus its covariance clause (3.27): a normalized joint product converges to the full-pairing sum of the prescribed limiting covariances.

theorem Anderson4D.Prop36FullData.tendsto_assignmentProduct {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hlam : 0 < lam) {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) {B s : ℕ} (hBB' : B ≤ B') (modes : Fin s → Z4 × Z4) (assignment : Fin r → FixedTruncationAtom s B) : Filter.Tendsto (fun (ε : ℝ) => (↑(lamEps lam ε))⁻¹ ^ r * ∫ (ω : M.Ω), ∏ j : Fin r, pmCoeff M ρ lam ε (assignment j).order (FixedTruncationAtom.modePair modes (assignment j)).1 (FixedTruncationAtom.modePair modes (assignment j)).2 ω) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∑ κ : PartialPairing (Fin r) with κ.IsFull, ∏ i ∈ κ.pairSupport with i < κ i, prop36PairLimit data.coeff (fixedTruncationAssignmentModes modes assignment) i (κ i)))

Direct assignment-level API from one coherent Proposition 3.6 data table.

noncomputable def Anderson4D.fixedTruncationMomentLimit {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ℂ

Complex presentation of the limiting r-th moment of a real fixed-truncation functional.

Equations

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

theorem Anderson4D.Prop36FullData.integrable_assignmentAtomProduct {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) {B s : ℕ} (hBB' : B ≤ B') (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (assignment : Fin r → FixedTruncationAtom s B) (ε : ℝ) : MeasureTheory.Integrable (fun (ω : M.Ω) => ∏ i : Fin r, fixedTruncationAtomTerm M ρ lam ε modes c (assignment i) ω) MeasureTheory.volume

Every atom-assignment product is integrable, using the regularity clause recorded with Proposition 3.6.

theorem Anderson4D.integral_assignmentAtomProduct {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B r s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (assignment : Fin r → FixedTruncationAtom s B) (ε : ℝ) : ∫ (ω : M.Ω), ∏ i : Fin r, fixedTruncationAtomTerm M ρ lam ε modes c (assignment i) ω = (∏ i : Fin r, FixedTruncationAtom.coeff c (assignment i)) * ((↑(lamEps lam ε))⁻¹ ^ r * ∫ (ω : M.Ω), ∏ i : Fin r, pmCoeff M ρ lam ε (assignment i).order (FixedTruncationAtom.modePair modes (assignment i)).1 (FixedTruncationAtom.modePair modes (assignment i)).2 ω)

Exact expectation ledger for one atom assignment.

theorem Anderson4D.Prop36FullData.integrable_fixedTruncationComplexPow {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) {B s : ℕ} (hBB' : B ≤ B') (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ε : ℝ) : MeasureTheory.Integrable (fun (ω : M.Ω) => ↑(fixedTruncationReal M ρ lam ε B s modes c ω) ^ r) MeasureTheory.volume

Integrability of every complexified fixed-truncation power.

theorem Anderson4D.Prop36FullData.integral_fixedTruncationComplexPow {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) {B s : ℕ} (hBB' : B ≤ B') (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ε : ℝ) : ∫ (ω : M.Ω), ↑(fixedTruncationReal M ρ lam ε B s modes c ω) ^ r = ∑ assignment : Fin r → FixedTruncationAtom s B, ∫ (ω : M.Ω), ∏ i : Fin r, fixedTruncationAtomTerm M ρ lam ε modes c (assignment i) ω

Integrating the finite assignment expansion is lossless.

theorem Anderson4D.Prop36FullData.tendsto_fixedTruncationComplexMoment {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hlam : 0 < lam) {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) {B s : ℕ} (hBB' : B ≤ B') (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (ω : M.Ω), ↑(fixedTruncationReal M ρ lam ε B s modes c ω) ^ r) (nhdsWithin 0 (Set.Ioi 0)) (nhds (fixedTruncationMomentLimit data B modes c))

Fixed-B convergence of every complexified raw moment, directly from Proposition 3.6.