The left noise source in the parametrix identity

This module integrates the Wick creation--contraction formula against the new Green edge. It keeps analytic linearity hypotheses explicit: the finite pairing and contraction sums are exchanged with Bochner integrals only under the corresponding termwise integrability facts.

noncomputable def Anderson4D.PartialPairing.leftNoisePairingCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (κ : PartialPairing (Fin n)) (z y : T4) (v : Fin n → T4) (ω : M.Ω) : ℝ

The unintegrated left-composition source attached to one old pairing.

Equations

• Anderson4D.PartialPairing.leftNoisePairingCore M ρ ε κ z y v ω = M.xiEps ρ ε ω z * Anderson4D.randIntegrand M ρ ε κ (Anderson4D.assemble z y v) ω

noncomputable def Anderson4D.PartialPairing.leftCreationCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (κ : PartialPairing (Fin n)) (z y : T4) (v : Fin n → T4) (ω : M.Ω) : ℝ

The creation summand before multiplication by the outer Green kernel.

Equations

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

noncomputable def Anderson4D.PartialPairing.leftRankedContractionCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) (z y : T4) (v : Fin n → T4) (ω : M.Ω) : ℝ

The contraction summand at an increasing rank before multiplication by the outer Green kernel.

Equations

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

def Anderson4D.PartialPairing.wickRankEquiv {n : ℕ} (κ : PartialPairing (Fin n)) (xt : Fin (n + 2) → T4) : Fin κ.singles.card ≃ Fin (wickAtSingleLabels κ xt).length

Increasing-rank transport between the cardinality of the single set and the definitionally equal Wick-label length.

Equations

• κ.wickRankEquiv xt = (Fin.castOrderIso ⋯).toEquiv

@[simp]

theorem Anderson4D.PartialPairing.wickRankEquiv_apply {n : ℕ} (κ : PartialPairing (Fin n)) (xt : Fin (n + 2) → T4) (j : Fin κ.singles.card) : (κ.wickRankEquiv xt) j = κ.wickRankIndex xt j

theorem Anderson4D.PartialPairing.leftNoisePairingCore_eq_create_add_contract (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (κ : PartialPairing (Fin n)) (z y : T4) (v : Fin n → T4) (ω : M.Ω) : leftNoisePairingCore M ρ ε κ z y v ω = leftCreationCore M ρ ε κ z y v ω + ∑ j : Fin κ.singles.card, leftRankedContractionCore M ρ ε κ j z y v ω

Pointwise Wick creation--contraction, with the recursive list index reindexed to the increasing rank of an ambient single.

noncomputable def Anderson4D.PartialPairing.leftCreationWeightedCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (κ : PartialPairing (Fin n)) (x z y : T4) (v : Fin n → T4) (ω : M.Ω) : ℝ

The creation core with the new outer Green edge.

Equations

• Anderson4D.PartialPairing.leftCreationWeightedCore M ρ ε κ x z y v ω = Anderson4D.greenFn (x - z) * Anderson4D.PartialPairing.leftCreationCore M ρ ε κ z y v ω

noncomputable def Anderson4D.PartialPairing.leftRankedContractionWeightedCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) (x z y : T4) (v : Fin n → T4) (ω : M.Ω) : ℝ

A ranked contraction core with the new outer Green edge.

Equations

• Anderson4D.PartialPairing.leftRankedContractionWeightedCore M ρ ε κ j x z y v ω = Anderson4D.greenFn (x - z) * Anderson4D.PartialPairing.leftRankedContractionCore M ρ ε κ j z y v ω

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

The actual left-composition source for one old pairing, before the finite sum over old pairings.

Equations

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

structure Anderson4D.PartialPairing.LeftPairingSplitIntegrability (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (x y : T4) (ω : M.Ω) : Prop

Exact analytic hypotheses for distributing the two nested integrals over the creation term and the finite contraction sum.

The inner conditions are deliberately almost-everywhere in the outer variable. This is both the precise Fubini hypothesis used below and the correct four-dimensional statement: on exceptional endpoint diagonals a two-Green product can have the borderline singularity |x|⁻⁴.

• creation_inner : ∀ᵐ (z : T4) ∂paperMeasure, MeasureTheory.Integrable (fun (v : Fin n → T4) => leftCreationWeightedCore M ρ ε κ x z y v ω) (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)
• contraction_inner : ∀ᵐ (z : T4) ∂paperMeasure, ∀ (j : Fin κ.singles.card), MeasureTheory.Integrable (fun (v : Fin n → T4) => leftRankedContractionWeightedCore M ρ ε κ j x z y v ω) (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)
• creation_outer : MeasureTheory.Integrable (fun (z : T4) => ∫ (v : Fin n → T4), leftCreationWeightedCore M ρ ε κ x z y v ω ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure) paperMeasure
• contraction_outer (j : Fin κ.singles.card) : MeasureTheory.Integrable (fun (z : T4) => ∫ (v : Fin n → T4), leftRankedContractionWeightedCore M ρ ε κ j x z y v ω ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure) paperMeasure

theorem Anderson4D.PartialPairing.leftNoisePairingContribution_eq_create_add_contract (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (x y : T4) (ω : M.Ω) (hint : LeftPairingSplitIntegrability M ρ ε n κ x y ω) : leftNoisePairingContribution M ρ lam ε n κ x y ω = headSingleCreationContribution M ρ lam ε n κ x y ω + ∑ j : Fin κ.singles.card, rankedContractionContribution M ρ lam ε n κ j x y ω

The integrated left source for one old pairing is its Wick creation contribution plus every ranked contraction contribution.

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

The full left noise source at old order n, summed over all old partial pairings.

Equations

• Anderson4D.PartialPairing.leftNoiseOrderContribution M ρ lam ε n x y ω = ∑ κ : Anderson4D.PartialPairing (Fin n), Anderson4D.PartialPairing.leftNoisePairingContribution M ρ lam ε n κ x y ω

theorem Anderson4D.PartialPairing.leftNoiseOrderContribution_eq_create_add_contract (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hint : ∀ (κ : PartialPairing (Fin n)), LeftPairingSplitIntegrability M ρ ε n κ x y ω) : leftNoiseOrderContribution M ρ lam ε n x y ω = ∑ κ : PartialPairing (Fin n), headSingleCreationContribution M ρ lam ε n κ x y ω + ∑ κ : PartialPairing (Fin n), ∑ j : Fin κ.singles.card, rankedContractionContribution M ρ lam ε n κ j x y ω

Summing the termwise Wick split gives the creation sum plus the nested ranked-contraction sum.

theorem Anderson4D.PartialPairing.leftNoiseOrderContribution_eq_headSingle_add_contractions (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)) : leftNoiseOrderContribution M ρ lam ε n x y ω = ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadIsSingle }, randRI M ρ lam ε (n + 1) (↑κ) x y ω + ∑ κ : PartialPairing (Fin n), ∑ j : Fin κ.singles.card, rankedContractionContribution M ρ lam ε n κ j x y ω

Case (1) is now completely identified inside the full left source; the remaining nested sum consists precisely of paired-head terms.

def Anderson4D.PartialPairing.markedHasHeadPrefix {n : ℕ} (d : MarkedSingle (Fin n)) : Prop

Predicate separating the two paired-head branches after adjoining the new head to marked-single data.

Equations

• Anderson4D.PartialPairing.markedHasHeadPrefix d = ((Anderson4D.PartialPairing.wickHeadEquiv n) (Sum.inr d)).HasFullyPairedHeadPrefix

@[implicit_reducible]

noncomputable instance Anderson4D.PartialPairing.instDecidablePredMarkedSingleFinMarkedHasHeadPrefix {n : ℕ} : DecidablePred markedHasHeadPrefix

Equations

• Anderson4D.PartialPairing.instDecidablePredMarkedSingleFinMarkedHasHeadPrefix x✝ = Classical.dec (Anderson4D.PartialPairing.markedHasHeadPrefix x✝)

theorem Anderson4D.PartialPairing.sum_markedSingle_noPrefix_add_withPrefix {n : ℕ} {R : Type u_1} [AddCommMonoid R] (f : MarkedSingle (Fin n) → R) : ∑ d : MarkedSingle (Fin n), f d = ∑ d : { d : MarkedSingle (Fin n) // ¬markedHasHeadPrefix d }, f ↑d + ∑ d : { d : MarkedSingle (Fin n) // markedHasHeadPrefix d }, f ↑d

Any finite sum over marked singles splits into the no-prefix and with-prefix branches.

theorem Anderson4D.PartialPairing.sum_rankedContractionContribution_eq_headBranches (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : ∑ κ : PartialPairing (Fin n), ∑ j : Fin κ.singles.card, rankedContractionContribution M ρ lam ε n κ j x y ω = ∑ d : { d : MarkedSingle (Fin n) // ¬markedHasHeadPrefix d }, headPairedContractionContribution M ρ lam ε n (↑d) x y ω + ∑ d : { d : MarkedSingle (Fin n) // markedHasHeadPrefix d }, headPairedContractionContribution M ρ lam ε n (↑d) x y ω

The nested Wick ranks reindex to marked singles and then split into paper cases (2) and (3), without changing multiplicities.

def Anderson4D.PartialPairing.noPrefixMarkedPredicateEquiv (n : ℕ) : { d : MarkedSingle (Fin n) // ¬markedHasHeadPrefix d } ≃ { d : MarkedSingle (Fin n) // ((wickHeadEquiv n) (Sum.inr d)).HeadPairedNoPrefix }

The predicate-only no-prefix subtype is canonically the HeadPairedNoPrefix subtype used by the paper-facing pairing split.

Equations

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

theorem Anderson4D.PartialPairing.sum_markedNoPrefixContribution_eq_randRI (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hint : ∀ (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)) : ∑ d : { d : MarkedSingle (Fin n) // ¬markedHasHeadPrefix d }, headPairedContractionContribution M ρ lam ε n (↑d) x y ω = ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix }, randRI M ρ lam ε (n + 1) (↑κ) x y ω

The whole no-prefix marked branch is the case-(2) random-kernel sum.

theorem Anderson4D.PartialPairing.leftNoiseOrderContribution_eq_caseOne_caseTwo_add_caseThreeSource (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)) : leftNoiseOrderContribution M ρ lam ε n x y ω = ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadIsSingle }, randRI M ρ lam ε (n + 1) (↑κ) x y ω + ∑ κ : { κ : PartialPairing (Fin (n + 1)) // κ.HeadPairedNoPrefix }, randRI M ρ lam ε (n + 1) (↑κ) x y ω + ∑ d : { d : MarkedSingle (Fin n) // markedHasHeadPrefix d }, headPairedContractionContribution M ρ lam ε n (↑d) x y ω

Left source after closing cases (1) and (2). The sole remaining summand is the with-prefix branch handled by the case-(3) block factorization.