Right parametrix identity from kernel symmetry

The random Schrödinger kernel and every finite parametrix order are symmetric in their external variables. This module isolates the exact consequence needed for paper (3.17): once that orderwise symmetry is available, the right-composition identity is the left-composition identity with the external variables exchanged. Thus the Wick head-case analysis does not have to be duplicated at the tail of the chain.

def Anderson4D.PartialPairing.ParametrixKernelSymmetric (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (ω : M.Ω) : Prop

Symmetry of one random parametrix order in its two external variables.

Equations

• Anderson4D.PartialPairing.ParametrixKernelSymmetric M ρ lam ε n ω = ∀ (x y : Anderson4D.T4), Anderson4D.parametrixP M ρ lam ε n x y ω = Anderson4D.parametrixP M ρ lam ε n y x ω

def Anderson4D.PartialPairing.ParametrixKernelSymmetricThrough (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (N : ℕ) (ω : M.Ω) : Prop

Orderwise symmetry through a fixed truncation order.

Equations

• Anderson4D.PartialPairing.ParametrixKernelSymmetricThrough M ρ lam ε N ω = ∀ n ≤ N, Anderson4D.PartialPairing.ParametrixKernelSymmetric M ρ lam ε n ω

theorem Anderson4D.PartialPairing.rightParametrixNoiseSource_eq_left_swap (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hsymm : ParametrixKernelSymmetric M ρ lam ε n ω) : rightParametrixNoiseSource M ρ lam ε n x y ω = leftParametrixNoiseSource M ρ lam ε n y x ω

The right noise composition is the left noise composition with the external variables exchanged.

theorem Anderson4D.PartialPairing.caseThreeRightCountertermBlock_eq_left_swap (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) (hsymm : ParametrixKernelSymmetric M ρ lam ε r ω) : caseThreeRightCountertermBlock M ρ lam ε q r x y ω = caseThreeCountertermBlock M ρ lam ε q r y x ω

The right counterterm block is the transposed left counterterm block.

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

The fixed-order right counterterm sum, in the same range as paper (3.16)--(3.17).

Equations

• Anderson4D.PartialPairing.rightOrderCountertermSum M ρ lam ε n x y ω = ∑ q ∈ Finset.Icc 1 ((n + 1) / 2), Anderson4D.caseThreeRightCountertermBlock M ρ lam ε q (n + 1 - 2 * q) x y ω

theorem Anderson4D.PartialPairing.rightParametrixNoiseSource_eq_parametrix_succ_add_counterterms_of_left (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hsymm : ParametrixKernelSymmetricThrough M ρ lam ε (n + 1) ω) (hleft : leftParametrixNoiseSource M ρ lam ε n y x ω = parametrixP M ρ lam ε (n + 1) y x ω + leftOrderCountertermSum M ρ lam ε n y x ω) : rightParametrixNoiseSource M ρ lam ε n x y ω = parametrixP M ρ lam ε (n + 1) x y ω + rightOrderCountertermSum M ρ lam ε n x y ω

Transpose the complete fixed-order left identity to obtain the right identity. Symmetry is only required through the new order n+1.

theorem Anderson4D.PartialPairing.rightPreconditionedParametrixAction_eq_green_add_remainder_of_left (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) (hsymm : ParametrixKernelSymmetricThrough M ρ lam ε A ω) (hleft : ∀ m ∈ Finset.Icc 1 A, leftParametrixNoiseSource M ρ lam ε (m - 1) y x ω = parametrixP M ρ lam ε m y x ω + leftOrderCountertermSum M ρ lam ε (m - 1) y x ω) : rightPreconditionedParametrixAction M ρ lam ε A x y ω = greenFn (x - y) + rightPreconditionedRemainder M ρ lam ε A x y ω

The complete postconditioned remainder identity follows from the left fixed-order identities and symmetry through the truncation order.