The head-single branch of the parametrix identity

This file identifies Wick creation with case (1) in the proof of Proposition 3.4. Adjoining the new noise variable is the same as prepending one fixed point to the old partial pairing.

@[simp]

theorem Anderson4D.PartialPairing.wickHeadEquiv_creation_zero (n : ℕ) (κ : PartialPairing (Fin n)) : ((wickHeadEquiv n) (Sum.inl κ)) 0 = 0

@[simp]

theorem Anderson4D.PartialPairing.wickHeadEquiv_creation_succ (n : ℕ) (κ : PartialPairing (Fin n)) (i : Fin n) : ((wickHeadEquiv n) (Sum.inl κ)) i.succ = (κ i).succ

theorem Anderson4D.PartialPairing.wickHeadEquiv_creation_eq_append (n : ℕ) (κ : PartialPairing (Fin n)) : (wickHeadEquiv n) (Sum.inl κ) = appendPairingTo ⋯ PartialPairing.id κ

The creation pairing is the consecutive append of a singleton fixed head and the old pairing.

@[simp]

theorem Anderson4D.PartialPairing.extract_id_fin_one : extract PartialPairing.id = []

theorem Anderson4D.PartialPairing.chainProduct_wickHeadEquiv_creation (n : ℕ) (κ : PartialPairing (Fin n)) (xt : Fin (n + 3) → T4) : (∏ e : Fin (n + 2), if ↑e ∈ List.map (fun (p : Fin (n + 1) × Fin (n + 1)) => ↑p.2 + 1) (extract ((wickHeadEquiv n) (Sum.inl κ))) then 1 else greenFn (xt e.castSucc - xt e.succ)) = greenFn (xt 0 - xt 1) * ∏ e : Fin (n + 1), if ↑e ∈ List.map (fun (p : Fin n × Fin n) => ↑p.2 + 1) (extract κ) then 1 else greenFn (ambientTailTuple ⋯ xt e.castSucc - ambientTailTuple ⋯ xt e.succ)

Prepending a fixed point only adds the new first Green edge to the chain product.

theorem Anderson4D.PartialPairing.detIntegrand_wickHeadEquiv_creation (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (xt : Fin (n + 3) → T4) : detIntegrand ρ ε (n + 1) ((wickHeadEquiv n) (Sum.inl κ)) xt = greenFn (xt 0 - xt 1) * detIntegrand ρ ε n κ (ambientTailTuple ⋯ xt)

The deterministic closed form for a created pairing is the old closed form preceded by the new free Green edge.

theorem Anderson4D.PartialPairing.singles_wickHeadEquiv_creation (n : ℕ) (κ : PartialPairing (Fin n)) : ((wickHeadEquiv n) (Sum.inl κ)).singles = insert 0 (Finset.map (Fin.succEmb n) κ.singles)

The singles of a creation pairing are the new zero followed by the shifted old singles.

theorem Anderson4D.PartialPairing.wickAtSingleLabels_eq_sort_map {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : wickAtSingleLabels κ xt = List.map (fun (i : Fin m) => xt (varIdx i)) (κ.singles.sort fun (a b : Fin m) => a ≤ b)

The ordered list of values attached to the singles is the sorted singles finset mapped through the ambient tuple.

theorem Anderson4D.PartialPairing.wickAtSingleLabels_wickHeadEquiv_creation (n : ℕ) (κ : PartialPairing (Fin n)) (xt : Fin (n + 3) → T4) : wickAtSingleLabels ((wickHeadEquiv n) (Sum.inl κ)) xt = xt 1 :: wickAtSingleLabels κ (ambientTailTuple ⋯ xt)

Creation prepends the new head value to the old ordered list of single labels.

theorem Anderson4D.PartialPairing.wickAt_wickHeadEquiv_creation (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (xt : Fin (n + 3) → T4) (ω : M.Ω) : wickAt M ρ ε ((wickHeadEquiv n) (Sum.inl κ)) xt ω = wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) (xt 1 :: wickAtSingleLabels κ (ambientTailTuple ⋯ xt)) ω

The Wick factor of the created pairing is exactly the creation term in the head recursion.

theorem Anderson4D.PartialPairing.headSingleCreationTerm_eq_randIntegrand (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (xt : Fin (n + 3) → T4) (ω : M.Ω) : greenFn (xt 0 - xt 1) * (detIntegrand ρ ε n κ (ambientTailTuple ⋯ xt) * wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) (xt 1 :: wickAtSingleLabels κ (ambientTailTuple ⋯ xt)) ω) = randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inl κ)) xt ω

Pointwise case (1) of Proposition 3.4: the Wick-creation source term is the random integrand indexed by the corresponding head-single pairing.

Splitting the new integration variable

noncomputable def Anderson4D.PartialPairing.headTailVariablesEquiv (n : ℕ) : (Fin (n + 1) → T4) ≃ᵐ T4 × (Fin n → T4)

Measurable separation of the first coordinate from a tuple of n+1 internal variables.

Equations

• Anderson4D.PartialPairing.headTailVariablesEquiv n = MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => Anderson4D.T4) 0

@[simp]

theorem Anderson4D.PartialPairing.headTailVariablesEquiv_symm_apply (n : ℕ) (z : T4) (v : Fin n → T4) : (headTailVariablesEquiv n).symm (z, v) = Fin.cons z v

theorem Anderson4D.PartialPairing.integral_headTailVariables (n : ℕ) (f : (Fin (n + 1) → T4) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) : (∫ (u : Fin (n + 1) → T4), f u ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure) = ∫ (z : T4), ∫ (v : Fin n → T4), f (Fin.cons z v) ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure ∂paperMeasure

Fubini after separating the new head variable from the old internal variables.

@[simp]

theorem Anderson4D.PartialPairing.assemble_cons_first_internal (n : ℕ) (x z y : T4) (v : Fin n → T4) : assemble x y (Fin.cons z v) 1 = z

theorem Anderson4D.PartialPairing.ambientTailTuple_assemble_cons (n : ℕ) (x z y : T4) (v : Fin n → T4) : ambientTailTuple ⋯ (assemble x y (Fin.cons z v)) = assemble z y v

Removing the first internal variable from an assembled ambient tuple leaves the old assembled tuple.

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

The integrated Wick-creation source attached to one old pairing.

Equations

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

theorem Anderson4D.PartialPairing.headSingleCreationContribution_eq_randRI (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (x y : T4) (ω : M.Ω) (hint : 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)) : headSingleCreationContribution M ρ lam ε n κ x y ω = randRI M ρ lam ε (n + 1) ((wickHeadEquiv n) (Sum.inl κ)) x y ω

Integrated case (1) of Proposition 3.4. Under exactly the integrability needed for Fubini, the creation source is the random kernel indexed by the head-single pairing.

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

Summed case (1) of Proposition 3.4. Wick creation enumerates the head-single class with multiplicity one.