Explicit boundary algebra for the parametrix error

This file identifies the two concrete factor residuals with the finite boundary sums in paper (3.21). The argument is entirely algebraic: graded compositions are classified by their first or last block, and the resulting recurrence is inserted into the already proved finite telescope.

No inverse of the Green operator and no pointwise kernel realization is used here.

The one-block operators

noncomputable def Anderson4D.PartialPairing.gradedBlockL2Factor (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (d : ℕ) : ↥TorusL2 →L[ℂ] ↥TorusL2

The bounded operator carried by one graded block.

Equations

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

noncomputable def Anderson4D.PartialPairing.gradedNoiseL2Factor (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ↥TorusL2 →L[ℂ] ↥TorusL2

The degree-one (mollified-noise) block.

Equations

• Anderson4D.PartialPairing.gradedNoiseL2Factor M ρ lam ε ω hξ = Anderson4D.PartialPairing.gradedBlockL2Factor M ρ lam ε ω hξ 1

noncomputable def Anderson4D.PartialPairing.gradedCountertermL2Factor (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (q : ℕ) : ↥TorusL2 →L[ℂ] ↥TorusL2

The positive counterterm operator. The sign is chosen so that a graded block of size 2q is its negative.

Equations

• Anderson4D.PartialPairing.gradedCountertermL2Factor M ρ lam ε ω hξ q = -Anderson4D.PartialPairing.gradedBlockL2Factor M ρ lam ε ω hξ (2 * q)

@[simp]

theorem Anderson4D.PartialPairing.renormWordL2Factor_cons (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (d : ℕ) (word : List ℕ) : renormWordL2Factor M ρ lam ε ω hξ (d :: word) = gradedBlockL2Factor M ρ lam ε ω hξ d * renormWordL2Factor M ρ lam ε ω hξ word

@[simp]

theorem Anderson4D.PartialPairing.gradedBlockL2Factor_one (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : gradedBlockL2Factor M ρ lam ε ω hξ 1 = gradedNoiseL2Factor M ρ lam ε ω hξ

theorem Anderson4D.PartialPairing.gradedBlockL2Factor_even (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) {d : ℕ} (hd : Even d) : gradedBlockL2Factor M ρ lam ε ω hξ d = -gradedCountertermL2Factor M ρ lam ε ω hξ (d / 2)

theorem Anderson4D.PartialPairing.gradedBlockL2Factor_eq_zero (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) {d : ℕ} (hone : d ≠ 1) (hodd : ¬Even d) : gradedBlockL2Factor M ρ lam ε ω hξ d = 0

The mollified potential is the finite sum of graded blocks

theorem Anderson4D.PartialPairing.mollifiedPotentialContinuousMap_eq_gradedWeights (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : mollifiedPotentialContinuousMap M ρ lam ε ω hξ = renormWordWeightContinuousMap M ρ lam ε ω hξ 1 + ∑ q ∈ Finset.Icc 1 (truncOrder ε), renormWordWeightContinuousMap M ρ lam ε ω hξ (2 * q)

theorem Anderson4D.PartialPairing.mollifiedPotentialL2Op_eq_gradedBlocks (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : Kop greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω) = gradedNoiseL2Factor M ρ lam ε ω hξ - ∑ q ∈ Finset.Icc 1 (truncOrder ε), gradedCountertermL2Factor M ρ lam ε ω hξ q

Head and tail classification of operator words

def Anderson4D.PartialPairing.compositionReverseEquiv (n : ℕ) : Composition n ≃ Composition n

Reverse is packaged as an equivalence so that it can be composed with compositionHeadEquiv.

Equations

• Anderson4D.PartialPairing.compositionReverseEquiv n = { toFun := Composition.reverse, invFun := Composition.reverse, left_inv := ⋯, right_inv := ⋯ }

def Anderson4D.PartialPairing.compositionTailEquiv (n : ℕ) : Composition (n + 1) ≃ (k : Fin (n + 1)) × Composition (n - ↑k)

Classify a nonempty composition by its last block.

Equations

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

theorem Anderson4D.PartialPairing.compositionTailEquiv_symm_blocks (n : ℕ) (k : Fin (n + 1)) (c : Composition (n - ↑k)) : ((compositionTailEquiv n).symm ⟨k, c⟩).blocks = c.blocks ++ [↑k + 1]

theorem Anderson4D.PartialPairing.renormWordL2Factor_append_single (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (word : List ℕ) (d : ℕ) : renormWordL2Factor M ρ lam ε ω hξ (word ++ [d]) = renormWordL2Factor M ρ lam ε ω hξ word * gradedBlockL2Factor M ρ lam ε ω hξ d

Appending one last block appends its operator on the right.

theorem Anderson4D.PartialPairing.gradedParametrixL2FactorOrder_succ_eq_sum_head (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (n : ℕ) : gradedParametrixL2FactorOrder M ρ lam ε ω hξ (n + 1) = ∑ k : Fin (n + 1), gradedBlockL2Factor M ρ lam ε ω hξ (↑k + 1) * gradedParametrixL2FactorOrder M ρ lam ε ω hξ (n - ↑k)

Operator order n+1, classified by the first block.

theorem Anderson4D.PartialPairing.gradedParametrixL2FactorOrder_succ_eq_sum_tail (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (n : ℕ) : gradedParametrixL2FactorOrder M ρ lam ε ω hξ (n + 1) = ∑ k : Fin (n + 1), gradedParametrixL2FactorOrder M ρ lam ε ω hξ (n - ↑k) * gradedBlockL2Factor M ρ lam ε ω hξ (↑k + 1)

Operator order n+1, classified by the last block.

The two operator recurrences

theorem Anderson4D.PartialPairing.headSelector_sum_addCommGroup {R : Type u_1} [AddCommGroup R] (n : ℕ) (A : R) (B : ℕ → R) : (∑ k : Fin (n + 1), if ↑k = 0 then A else if Even (↑k + 1) then -B ((↑k + 1) / 2) else 0) = A - ∑ q ∈ Finset.Icc 1 ((n + 1) / 2), B q

headSelector_sum needs only additive group structure. This version applies to the noncommutative operator ring.

theorem Anderson4D.PartialPairing.gradedParametrixL2FactorOrder_succ_eq_noise_sub_counterterms (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (n : ℕ) : gradedParametrixL2FactorOrder M ρ lam ε ω hξ (n + 1) = gradedNoiseL2Factor M ρ lam ε ω hξ * gradedParametrixL2FactorOrder M ρ lam ε ω hξ n - ∑ q ∈ Finset.Icc 1 ((n + 1) / 2), gradedCountertermL2Factor M ρ lam ε ω hξ q * gradedParametrixL2FactorOrder M ρ lam ε ω hξ (n + 1 - 2 * q)

First-block recurrence for the graded operator orders.

theorem Anderson4D.PartialPairing.gradedParametrixL2FactorOrder_succ_eq_noise_sub_counterterms_right (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (n : ℕ) : gradedParametrixL2FactorOrder M ρ lam ε ω hξ (n + 1) = gradedParametrixL2FactorOrder M ρ lam ε ω hξ n * gradedNoiseL2Factor M ρ lam ε ω hξ - ∑ q ∈ Finset.Icc 1 ((n + 1) / 2), gradedParametrixL2FactorOrder M ρ lam ε ω hξ (n + 1 - 2 * q) * gradedCountertermL2Factor M ρ lam ε ω hξ q

Last-block recurrence, needed for the residual on the other side.

The explicit boundary residuals

noncomputable def Anderson4D.PartialPairing.gradedPerrRightBoundary (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (A : ℕ) : ↥TorusL2 →L[ℂ] ↥TorusL2

First-block boundary sum in (3.21), corresponding to (1 - K) Q - 1.

Equations

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

noncomputable def Anderson4D.PartialPairing.gradedPerrLeftBoundary (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (A : ℕ) : ↥TorusL2 →L[ℂ] ↥TorusL2

Last-block boundary sum in (3.21), corresponding to Q (1 - K) - 1.

Equations

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

theorem Anderson4D.PartialPairing.gradedPerrRightResidual_eq_boundary (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (A : ℕ) (hA : A = truncOrder ε) : (1 - Kop greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω)) * gradedTruncatedParametrixL2Factor M ρ lam ε ω hξ A - 1 = gradedPerrRightBoundary M ρ lam ε ω hξ A

theorem Anderson4D.PartialPairing.gradedPerrLeftResidual_eq_boundary (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (A : ℕ) (hA : A = truncOrder ε) : gradedTruncatedParametrixL2Factor M ρ lam ε ω hξ A * (1 - Kop greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω)) - 1 = gradedPerrLeftBoundary M ρ lam ε ω hξ A

Proof-independent boundary random variables

noncomputable def Anderson4D.PartialPairing.canonicalPerrRightBoundary (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

Totalized explicit first-block boundary residual.

Equations

• Anderson4D.PartialPairing.canonicalPerrRightBoundary M ρ lam ε A ω = if hξ : Continuous (M.xiEps ρ ε ω) then Anderson4D.PartialPairing.gradedPerrRightBoundary M ρ lam ε ω hξ A else 0

noncomputable def Anderson4D.PartialPairing.canonicalPerrLeftBoundary (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

Totalized explicit last-block boundary residual.

Equations

• Anderson4D.PartialPairing.canonicalPerrLeftBoundary M ρ lam ε A ω = if hξ : Continuous (M.xiEps ρ ε ω) then Anderson4D.PartialPairing.gradedPerrLeftBoundary M ρ lam ε ω hξ A else 0

theorem Anderson4D.PartialPairing.canonicalPerrRightRemainder_eq_boundary_of_continuous (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (hA : A = truncOrder ε) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : canonicalPerrRightRemainder M ρ lam ε A ω = canonicalPerrRightBoundary M ρ lam ε A ω

theorem Anderson4D.PartialPairing.canonicalPerrLeftRemainder_eq_boundary_of_continuous (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (hA : A = truncOrder ε) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : canonicalPerrLeftRemainder M ρ lam ε A ω = canonicalPerrLeftBoundary M ρ lam ε A ω

theorem Anderson4D.PartialPairing.ae_canonicalPerrRemainders_eq_boundaries (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (ω : M.Ω), canonicalPerrRightRemainder M ρ lam ε (truncOrder ε) ω = canonicalPerrRightBoundary M ρ lam ε (truncOrder ε) ω ∧ canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε) ω = canonicalPerrLeftBoundary M ρ lam ε (truncOrder ε) ω

At positive scale both canonical residuals are almost surely the explicit boundary sums from (3.21).

theorem Anderson4D.PartialPairing.measureReal_compl_canonicalConstructedL2ParametrixGoodEvent_le_of_boundaries {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} (hfubini : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε (truncOrder ε) ω) (hintBoundary : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖canonicalPerrLeftBoundary M ρ lam ε (truncOrder ε) ω‖ + ‖canonicalPerrRightBoundary M ρ lam ε (truncOrder ε) ω‖) MeasureTheory.volume) (δR : ℝ) (hfirstBoundary : ∫ (ω : M.Ω), ‖canonicalPerrLeftBoundary M ρ lam ε (truncOrder ε) ω‖ + ‖canonicalPerrRightBoundary M ρ lam ε (truncOrder ε) ω‖ ≤ δR) : MeasureTheory.volume.real (canonicalL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)) (canonicalPerrRightRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε (truncOrder ε) / (ε ^ (-14)) ^ 2 + δR / ε ^ 28

The canonical good-event estimate now asks for a first-moment bound only on the explicit boundary sums of (3.21), rather than on opaque residual variables.