Assembly of the left parametrix identity

This module combines the already closed head-single and no-prefix branches with one exact statement for the with-prefix branch. It produces the paper-facing, free-Green-preconditioned form of Proposition 3.4.

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

The still-unreduced with-prefix Wick-contraction sum at old order n.

Equations

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

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

The ambient random kernels whose new head belongs to a fully paired prefix.

Equations

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

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

All fixed-prefix counterterm blocks at new order n+1, in exactly the range of paper (3.16).

Equations

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

theorem Anderson4D.PartialPairing.leftNoiseOrderContribution_eq_parametrix_succ_add_counterterms (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hsplit : ∀ (κ : PartialPairing (Fin n)), LeftPairingSplitIntegrability M ρ ε n κ x y ω) (hcreation : ∀ (κ : PartialPairing (Fin n)), MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inl κ)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) (hnoPrefix : ∀ (d : { d : MarkedSingle (Fin n) // ¬markedHasHeadPrefix d }), MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inr ↑d)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) (hcaseThree : leftWithPrefixContractionSum M ρ lam ε n x y ω = leftWithPrefixRandRISum M ρ lam ε n x y ω + leftOrderCountertermSum M ρ lam ε n x y ω) : leftNoiseOrderContribution M ρ lam ε n x y ω = parametrixP M ρ lam ε (n + 1) x y ω + leftOrderCountertermSum M ρ lam ε n x y ω

Once the with-prefix Wick source has been identified with its ambient random kernels plus fixed-prefix counterterms, the three head classes assemble to P_{n+1} with multiplicity one.

theorem Anderson4D.PartialPairing.leftParametrixNoiseSource_eq_parametrix_succ_add_counterterms (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hsource : LeftOrderSourceIntegrability M ρ lam ε n x y ω) (hsplit : ∀ (κ : PartialPairing (Fin n)), LeftPairingSplitIntegrability M ρ ε n κ x y ω) (hcreation : ∀ (κ : PartialPairing (Fin n)), MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inl κ)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) (hnoPrefix : ∀ (d : { d : MarkedSingle (Fin n) // ¬markedHasHeadPrefix d }), MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inr ↑d)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) (hcaseThree : leftWithPrefixContractionSum M ρ lam ε n x y ω = leftWithPrefixRandRISum M ρ lam ε n x y ω + leftOrderCountertermSum M ρ lam ε n x y ω) : leftParametrixNoiseSource M ρ lam ε n x y ω = parametrixP M ρ lam ε (n + 1) x y ω + leftOrderCountertermSum M ρ lam ε n x y ω

Preconditioned Proposition 3.4, left form.

This is paper (3.16) after applying (1-Δ)⁻¹ on the left. All integration hypotheses are explicit; the sole branch-specific input is the exact with-prefix equality above.

theorem Anderson4D.PartialPairing.leftPreconditionedParametrixAction_eq_green_add_remainder_of_headCases (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (x y : T4) (ω : M.Ω) (hsource : ∀ n ∈ Finset.range A, LeftOrderSourceIntegrability M ρ lam ε n x y ω) (hsplit : ∀ n ∈ Finset.range A, ∀ (κ : PartialPairing (Fin n)), LeftPairingSplitIntegrability M ρ ε n κ x y ω) (hcreation : ∀ n ∈ Finset.range A, ∀ (κ : PartialPairing (Fin n)), MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inl κ)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) (hnoPrefix : ∀ n ∈ Finset.range A, ∀ (d : { d : MarkedSingle (Fin n) // ¬markedHasHeadPrefix d }), MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inr ↑d)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) (hcaseThree : ∀ n ∈ Finset.range A, leftWithPrefixContractionSum M ρ lam ε n x y ω = leftWithPrefixRandRISum M ρ lam ε n x y ω + leftOrderCountertermSum M ρ lam ε n x y ω) : leftPreconditionedParametrixAction M ρ lam ε A x y ω = greenFn (x - y) + leftPreconditionedRemainder M ρ lam ε A x y ω

The complete left preconditioned remainder identity follows from the analytic head-case data for precisely the orders below the truncation. The terminal order A appears only in the remainder and requires no extra use of Proposition 3.4.