The left preconditioned parametrix remainder

This module instantiates the finite telescope of paper (3.20)--(3.21) with the actual random kernels. The only input is the order-by-order preconditioned form of Proposition 3.4; all finite reindexing and boundary cancellation is proved in RemainderAlgebra.

noncomputable def Anderson4D.PartialPairing.truncatedParametrixKernel (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) : ℝ

The kernel of the order-A truncated parametrix P_ε = ∑_{m=0}^A P_m.

Equations

• Anderson4D.PartialPairing.truncatedParametrixKernel M ρ lam ε A x y ω = ∑ m ∈ Finset.range (A + 1), Anderson4D.parametrixP M ρ lam ε m x y ω

noncomputable def Anderson4D.PartialPairing.leftPreconditionedParametrixAction (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) : ℝ

The free-Green-preconditioned left action G L_ε P_ε, expanded into the parametrix, noise, and counterterm pieces.

Equations

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

noncomputable def Anderson4D.PartialPairing.leftPreconditionedRemainder (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) : ℝ

The preconditioned left remainder from paper (3.21): the terminal noise composition plus exactly the counterterms crossing the truncation boundary.

Equations

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

theorem Anderson4D.PartialPairing.leftPreconditionedParametrixAction_eq_green_add_remainder (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) (horder : ∀ m ∈ Finset.Icc 1 A, leftParametrixNoiseSource M ρ lam ε (m - 1) x y ω = parametrixP M ρ lam ε m x y ω + ∑ q ∈ Finset.Icc 1 (m / 2), caseThreeCountertermBlock M ρ lam ε q (m - 2 * q) x y ω) : leftPreconditionedParametrixAction M ρ lam ε A x y ω = greenFn (x - y) + leftPreconditionedRemainder M ρ lam ε A x y ω

Paper (3.20)--(3.21), after applying the free Green operator on the left. The hypothesis is precisely the preconditioned order-m identity (3.16), with no estimate or extra identity bundled into it.

Right-composition counterpart

noncomputable def Anderson4D.PartialPairing.rightParametrixNoiseSource (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : ℝ

The right noise part of Pₙ (λ_ε ξ_ε) G, i.e. the free-Green-postconditioned source in paper (3.17).

Equations

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

noncomputable def Anderson4D.PartialPairing.rightPreconditionedParametrixAction (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) : ℝ

The free-Green-postconditioned right action P_ε L_ε G, expanded into its three finite pieces.

Equations

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

noncomputable def Anderson4D.PartialPairing.rightPreconditionedRemainder (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) : ℝ

The postconditioned right remainder from paper (3.21).

Equations

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

theorem Anderson4D.PartialPairing.rightPreconditionedParametrixAction_eq_green_add_remainder (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) (horder : ∀ m ∈ Finset.Icc 1 A, rightParametrixNoiseSource M ρ lam ε (m - 1) x y ω = parametrixP M ρ lam ε m x y ω + ∑ q ∈ Finset.Icc 1 (m / 2), caseThreeRightCountertermBlock M ρ lam ε q (m - 2 * q) x y ω) : rightPreconditionedParametrixAction M ρ lam ε A x y ω = greenFn (x - y) + rightPreconditionedRemainder M ρ lam ε A x y ω

Right counterpart of (3.20)--(3.21), after applying the free Green operator on the right.