Global Green-chain integrability

The Fourier-coefficient form of Proposition 3.4 integrates both external kernel variables. At that level every finite Green chain is genuinely integrable, even though a fixed-endpoint section can fail on the diagonal in four dimensions. This file records the measure-preserving change of variables from recursive weighted paths to the paper's flat (x,y,internal variables) coordinates.

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

Separate the terminal coordinate of a finite path, retaining the preceding coordinates in their original order.

Equations

• Anderson4D.globalPathLastEquiv n = MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => Anderson4D.T4) (Fin.last n)

@[simp]

theorem Anderson4D.globalPathLastEquiv_symm_apply (n : ℕ) (y : T4) (v : Fin n → T4) : (globalPathLastEquiv n).symm (y, v) = Fin.snoc v y

theorem Anderson4D.measurePreserving_globalPathLastEquiv (n : ℕ) : MeasureTheory.MeasurePreserving (⇑(globalPathLastEquiv n)) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))

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

Apply the terminal-coordinate equivalence under a separate left endpoint.

Equations

• Anderson4D.globalFlatPathEquiv n = (MeasurableEquiv.refl Anderson4D.T4).prodCongr (Anderson4D.globalPathLastEquiv n)

theorem Anderson4D.measurePreserving_globalFlatPathEquiv (n : ℕ) : MeasureTheory.MeasurePreserving (⇑(globalFlatPathEquiv n)) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)))

theorem Anderson4D.integrable_continuousNeumannFlatIntegrand_joint (m : C(T4, ℂ)) (β : Z4) (n : ℕ) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin n → T4)) => continuousNeumannFlatIntegrand m β n p.1 p.2.1 p.2.2) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)))

Every flat Green chain with continuous vertex weights is jointly integrable in both endpoints and all internal vertices.

theorem Anderson4D.integrable_flatGreenChain_joint (n : ℕ) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin n → T4)) => ∏ e : Fin (n + 1), ↑(greenFn (assemble p.1 p.2.1 p.2.2 e.castSucc - assemble p.1 p.2.1 p.2.2 e.succ))) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)))

The unweighted flat Green chain is the universal integrable majorant used for globally integrated random kernels.

theorem Anderson4D.integrable_bounded_mul_flatGreenChain_joint (n : ℕ) (weight : T4 × T4 × (Fin n → T4) → ℂ) (hweight : MeasureTheory.AEStronglyMeasurable weight (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)))) (C : ℝ) (hbound : ∀ᵐ (p : T4 × T4 × (Fin n → T4)) ∂paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)), ‖weight p‖ ≤ C) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin n → T4)) => weight p * ∏ e : Fin (n + 1), ↑(greenFn (assemble p.1 p.2.1 p.2.2 e.castSucc - assemble p.1 p.2.1 p.2.2 e.succ))) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)))

Any uniformly bounded measurable factor may be multiplied into the universal Green chain without losing integrability.