Removing the fixed perturbative truncation

This file carries out the B → ∞ part of paper (3.38)--(3.39). The finite square m₁,m₂ ≤ B is separated into a coefficient rectangle and a mode-dependent four-point form. Proposition 3.6's global antidiagonal identity evaluates the triangular part, while its uniform geometric coefficient bound controls the two corner tails.

def Anderson4D.prop36RectangleSum (X : ℕ → ℕ → ℝ) (B : ℕ) : ℝ

The square coefficient sum 𝔛_B used immediately before (3.36).

Equations

• Anderson4D.prop36RectangleSum X B = ∑ m₁ : Fin B, ∑ m₂ : Fin B, X (↑m₁ + 1) (↑m₂ + 1)

@[reducible, inline]

abbrev Anderson4D.FixedModeSign (s : ℕ) : Type

A mode together with the Boolean choice in the real-part expansion.

Equations

• Anderson4D.FixedModeSign s = (Fin s × Bool)

def Anderson4D.fixedModeSignPair {s : ℕ} (modes : Fin s → Z4 × Z4) (u : FixedModeSign s) : Z4 × Z4

Equations

• Anderson4D.fixedModeSignPair modes u = if u.2 = true then (-(modes u.1).1, -(modes u.1).2) else modes u.1

noncomputable def Anderson4D.fixedModeSignCoeff {s : ℕ} (c : Fin s → ℂ) (u : FixedModeSign s) : ℂ

Equations

• Anderson4D.fixedModeSignCoeff c u = if u.2 = true then (starRingEnd ℂ) (c u.1) / 2 else c u.1 / 2

noncomputable def Anderson4D.fixedModePairVariance {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ℂ

The mode-dependent four-point form left after the perturbative orders have been summed out.

Equations

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

def Anderson4D.FixedTruncationAtom.equivOrderMode (s B : ℕ) : FixedTruncationAtom s B ≃ Fin B × FixedModeSign s

Reindex an atom by its perturbative order first and its signed mode second.

Equations

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

@[simp]

theorem Anderson4D.FixedTruncationAtom.equivOrderMode_symm_apply {s B : ℕ} (p : Fin B × FixedModeSign s) : (equivOrderMode s B).symm p = { mode := p.2.1, orderIndex := p.1, conjugated := p.2.2 }

def Anderson4D.FixedTruncationAtom.pairEquivOrderMode (s B : ℕ) : FixedTruncationAtom s B × FixedTruncationAtom s B ≃ (Fin B × Fin B) × FixedModeSign s × FixedModeSign s

Simultaneously regroup two atoms into an order pair and a signed mode pair.

Equations

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

@[simp]

theorem Anderson4D.FixedTruncationAtom.pairEquivOrderMode_symm_apply {s B : ℕ} (p : (Fin B × Fin B) × FixedModeSign s × FixedModeSign s) : (pairEquivOrderMode s B).symm p = ({ mode := p.2.1.1, orderIndex := p.1.1, conjugated := p.2.1.2 }, { mode := p.2.2.1, orderIndex := p.1.2, conjugated := p.2.2.2 })

theorem Anderson4D.fixedTruncationPairVariance_eq_rectangle_mul (X : ℕ → ℕ → ℝ) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : fixedTruncationPairVariance X B modes c = ↑(prop36RectangleSum X B) * fixedModePairVariance modes c

Exact separation of the perturbative rectangle from the signed mode covariance.

theorem Anderson4D.fourPointHCoeff_neg_all (α₁ β₁ α₂ β₂ : Z4) : fourPointHCoeff (-α₁) (-β₁) (-α₂) (-β₂) = fourPointHCoeff α₁ β₁ α₂ β₂

Simultaneously negating all four external modes leaves the real four-point coefficient unchanged.

theorem Anderson4D.fourPointHCoeff_neg_left_eq_neg_right (α₁ β₁ α₂ β₂ : Z4) : fourPointHCoeff (-α₁) (-β₁) α₂ β₂ = fourPointHCoeff α₁ β₁ (-α₂) (-β₂)

Moving a simultaneous sign change from the first mode pair to the second preserves the coefficient.

theorem Anderson4D.conj_fourPointHCoeff (α₁ β₁ α₂ β₂ : Z4) : (starRingEnd ℂ) (fourPointHCoeff α₁ β₁ α₂ β₂) = fourPointHCoeff α₁ β₁ α₂ β₂

theorem Anderson4D.sum_div_two_mul_div_two {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : ι → ℂ) (b : κ → ℂ) (H : ι → κ → ℂ) : ∑ i : ι, ∑ j : κ, a i / 2 * (b j / 2) * H i j = (∑ i : ι, ∑ j : κ, a i * b j * H i j) * (1 / 4)

noncomputable def Anderson4D.unscaledLimitVariance {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ℝ

The four-point quadratic form before multiplication by the geometric limiting prefactor.

Equations

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

theorem Anderson4D.limitVar_eq_prefactor_mul_unscaled (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : limitVar lam modes c = limitPrefactor lam * unscaledLimitVariance modes c

theorem Anderson4D.fixedModePairVariance_eq_unscaled {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : fixedModePairVariance modes c = ↑(unscaledLimitVariance modes c)

The Boolean signed-mode expansion is exactly the real unscaled four-point variance.

The coefficient rectangle and its corner tail

def Anderson4D.prop36RectanglePairs (B : ℕ) : Finset (ℕ × ℕ)

Equations

• Anderson4D.prop36RectanglePairs B = (Finset.Ico 1 (B + 1)).product (Finset.Ico 1 (B + 1))

def Anderson4D.prop36TrianglePairs (B : ℕ) : Finset (ℕ × ℕ)

Equations

• Anderson4D.prop36TrianglePairs B = {p ∈ (Finset.Ico 1 (2 * B + 1)).product (Finset.Ico 1 (2 * B + 1)) | p.1 + p.2 ≤ 2 * B}

def Anderson4D.prop36CornerPairs (B : ℕ) : Finset (ℕ × ℕ)

Equations

• Anderson4D.prop36CornerPairs B = Anderson4D.prop36TrianglePairs B \ Anderson4D.prop36RectanglePairs B

theorem Anderson4D.prop36RectanglePairs_subset_triangle (B : ℕ) : prop36RectanglePairs B ⊆ prop36TrianglePairs B

theorem Anderson4D.prop36RectangleSum_eq_sum_pairs (X : ℕ → ℕ → ℝ) (B : ℕ) : prop36RectangleSum X B = ∑ p ∈ prop36RectanglePairs B, X p.1 p.2

def Anderson4D.prop36TriangleAntidiagonalSum (X : ℕ → ℕ → ℝ) (B : ℕ) : ℝ

The finite sum of all positive antidiagonals through total order 2B.

Equations

• Anderson4D.prop36TriangleAntidiagonalSum X B = ∑ m ∈ Finset.range (2 * B + 1), Anderson4D.positiveAntidiagonalSum X m

theorem Anderson4D.positiveAntidiagonalSum_one (X : ℕ → ℕ → ℝ) : positiveAntidiagonalSum X 1 = 0

theorem Anderson4D.positiveAntidiagonalSum_zero (X : ℕ → ℕ → ℝ) : positiveAntidiagonalSum X 0 = 0

theorem Anderson4D.Prop36FullData.triangleAntidiagonalSum_eq_partialSum {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) (B : ℕ) : prop36TriangleAntidiagonalSum data.coeff B = prop36EvenPartialSum lam B

Global (3.28) evaluates every finite positive triangle as the corresponding even geometric partial sum.

theorem Anderson4D.sum_prop36TrianglePairs_eq_antidiagonal (X : ℕ → ℕ → ℝ) (B : ℕ) : ∑ p ∈ prop36TrianglePairs B, X p.1 p.2 = prop36TriangleAntidiagonalSum X B

Summing the positive antidiagonal fibers of the triangle is the same as summing the triangle directly.

theorem Anderson4D.Prop36FullData.rectangle_add_corner_eq_partialSum {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) (B : ℕ) : prop36RectangleSum data.coeff B + ∑ p ∈ prop36CornerPairs B, data.coeff p.1 p.2 = prop36EvenPartialSum lam B

The coefficient rectangle plus its two corners is exactly the geometric partial sum dictated by (3.28).

theorem Anderson4D.prop36CornerPairs_card_le (B : ℕ) : (prop36CornerPairs B).card ≤ (2 * B) ^ 2

def Anderson4D.prop36CornerBound (C q : ℝ) (B : ℕ) : ℝ

A convenient polynomial-times-geometric envelope for both corner tails.

Equations

• Anderson4D.prop36CornerBound C q B = 4 * C * ↑B ^ 2 * q ^ B

theorem Anderson4D.Prop36FullData.abs_coeff_le_cornerBound {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) {B : ℕ} {p : ℕ × ℕ} (hp : p ∈ prop36CornerPairs B) (hq0 : 0 ≤ data.constant * lam) (hq1 : data.constant * lam ≤ 1) : |data.coeff p.1 p.2| ≤ data.constant * (data.constant * lam) ^ B

theorem Anderson4D.Prop36FullData.abs_cornerSum_le {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) (B : ℕ) (hq0 : 0 ≤ data.constant * lam) (hq1 : data.constant * lam ≤ 1) : |∑ p ∈ prop36CornerPairs B, data.coeff p.1 p.2| ≤ prop36CornerBound data.constant (data.constant * lam) B

theorem Anderson4D.tendsto_prop36CornerBound {C q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) : Filter.Tendsto (prop36CornerBound C q) Filter.atTop (nhds 0)

theorem Anderson4D.Prop36.abs_rectangle_sub_partialSum_le {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (hsmall : hP36.boundConstant * lam < 1) (B : ℕ) : |prop36RectangleSum (hP36.fullData B 2).coeff B - prop36EvenPartialSum lam B| ≤ prop36CornerBound hP36.boundConstant (hP36.boundConstant * lam) B

theorem Anderson4D.Prop36.tendsto_rectangleSum {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (hsmall : hP36.boundConstant * lam < 1) (hsub : lam ^ 2 < 2 * Real.pi ^ 2) : Filter.Tendsto (fun (B : ℕ) => prop36RectangleSum (hP36.fullData B 2).coeff B) Filter.atTop (nhds (limitPrefactor lam))

The square coefficient sums 𝔛_B converge to the explicit geometric prefactor.

theorem Anderson4D.Prop36.ofReal_fixedTruncationGaussianVariance_eq {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ↑(fixedTruncationGaussianVariance hP36 hlam B modes c) = prop36RectangleSum (hP36.fullData B 2).coeff B * unscaledLimitVariance modes c

The finite Gaussian variance is the coefficient rectangle times the mode-dependent unscaled variance.

theorem Anderson4D.Prop36.tendsto_fixedTruncationGaussianVariance_real {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (hsmall : hP36.boundConstant * lam < 1) (hsub : lam ^ 2 < 2 * Real.pi ^ 2) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Filter.Tendsto (fun (B : ℕ) => ↑(fixedTruncationGaussianVariance hP36 hlam B modes c)) Filter.atTop (nhds (limitVar lam modes c))

After the perturbative cutoff is removed, the canonical finite Gaussian variances converge to limitVar.

noncomputable def Anderson4D.limitGaussianVarianceNNReal (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (hsub : lam ^ 2 < 2 * Real.pi ^ 2) (c : Fin s → ℂ) : NNReal

The limiting nonnegative scalar variance.

Equations

• Anderson4D.limitGaussianVarianceNNReal lam modes hsub c = ⟨Anderson4D.limitVar lam modes c, ⋯⟩

theorem Anderson4D.Prop36.tendsto_fixedTruncationGaussianVariance {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (hsmall : hP36.boundConstant * lam < 1) (hsub : lam ^ 2 < 2 * Real.pi ^ 2) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Filter.Tendsto (fun (B : ℕ) => fixedTruncationGaussianVariance hP36 hlam B modes c) Filter.atTop (nhds (limitGaussianVarianceNNReal lam modes hsub c))

theorem Anderson4D.Prop36.tendsto_fixedGaussianCharFun_atTop {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (hsmall : hP36.boundConstant * lam < 1) (hsub : lam ^ 2 < 2 * Real.pi ^ 2) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Filter.Tendsto (fun (B : ℕ) => MeasureTheory.charFun (ProbabilityTheory.gaussianReal 0 (fixedTruncationGaussianVariance hP36 hlam B modes c)) 1) Filter.atTop (nhds (Complex.exp (-(↑(limitVar lam modes c) / 2))))

The characteristic functions of the canonical fixed-truncation Gaussians converge to the characteristic function prescribed by the explicit limiting variance.