Integrability of boundedly weighted Green paths

The parametrix and physical Neumann expansions repeatedly use a chain of four-dimensional Green kernels with bounded vertex weights. Pointwise integrability at fixed endpoints is false on exceptional diagonals (G² has the borderline singularity |x|⁻⁴). The correct reusable statement is joint integrability after the left endpoint and all path vertices are integrated. Fubini then supplies the required section integrability almost everywhere.

This file proves that statement for an arbitrary finite family of continuous vertex weights. It is the analytic base for the a.e. Fubini ledgers in Proposition 3.4 and for flattening the L² Neumann action.

theorem Anderson4D.integrable_greenFn_two_center_of_ne {x y : T4} (hxy : x ≠ y) : MeasureTheory.Integrable (fun (z : T4) => ↑(greenFn (x - z)) * ↑(greenFn (z - y))) paperMeasure

The critical two-edge Green chain is integrable precisely away from coincident fixed endpoints.

def Anderson4D.weightedGreenPath {n : ℕ} : (Fin n → C(T4, ℂ)) → T4 → (Fin n → T4) → ℂ

A recursively written Green path. The i-th vertex contributes weight i; there is one Green edge from the fixed left endpoint to the first vertex and between every two successive vertices.

Equations

• Anderson4D.weightedGreenPath x_4 x✝ x_6 = 1
• Anderson4D.weightedGreenPath weight x✝ v = ↑(Anderson4D.greenFn (x✝ - v 0)) * (weight 0) (v 0) * Anderson4D.weightedGreenPath (fun (i : Fin n) => weight i.succ) (v 0) (Fin.tail v)

@[simp]

theorem Anderson4D.weightedGreenPath_zero (weight : Fin 0 → C(T4, ℂ)) (x : T4) (v : Fin 0 → T4) : weightedGreenPath weight x v = 1

@[simp]

theorem Anderson4D.weightedGreenPath_succ {n : ℕ} (weight : Fin (n + 1) → C(T4, ℂ)) (x : T4) (v : Fin (n + 1) → T4) : weightedGreenPath weight x v = ↑(greenFn (x - v 0)) * (weight 0) (v 0) * weightedGreenPath (fun (i : Fin n) => weight i.succ) (v 0) (Fin.tail v)

theorem Anderson4D.integral_pathHeadTail {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (f : (Fin (n + 1) → T4) → E) (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 first vertex of a finite path from all remaining vertices. The explicit integrability hypothesis is essential: fixed-endpoint Green paths can fail to be integrable on exceptional diagonals in four dimensions.

theorem Anderson4D.integral_pathLast {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (f : (Fin (n + 1) → T4) → E) (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) = ∫ (y : T4), ∫ (v : Fin n → T4), f (Fin.snoc v y) ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure ∂paperMeasure

Fubini after separating the terminal vertex from the preceding vertices. This is the product-measure order used by the physical Neumann kernel: terminal point outside, internal chain variables inside.

theorem Anderson4D.integrable_weightedGreenPath_joint {n : ℕ} (weight : Fin n → C(T4, ℂ)) : MeasureTheory.Integrable (fun (p : T4 × (Fin n → T4)) => weightedGreenPath weight p.1 p.2) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))

Joint integrability of every finite Green path with continuous vertex weights. In particular, Fubini gives integrability of the path variables for almost every left endpoint.

theorem Anderson4D.ae_integrable_weightedGreenPath {n : ℕ} (weight : Fin n → C(T4, ℂ)) : ∀ᵐ (x : T4) ∂paperMeasure, MeasureTheory.Integrable (weightedGreenPath weight x) (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)

The section form used by Fubini: all path variables are integrable for almost every value of the left endpoint.