All-order flat realization of the physical Neumann action

L2NeumannAction.lean constructs every operator power by recursive Green convolution and checks the first nontrivial flat chain. Here the reusable weighted-path integrability theorem closes the Fubini induction at every order. The equality is correctly stated almost everywhere in the left endpoint: a fixed-endpoint flat chain may fail to be integrable on a diagonal, while its joint integrand is integrable and therefore has integrable sections almost everywhere.

noncomputable def Anderson4D.neumannActionPathWeight (m : C(T4, ℂ)) (β : Z4) (n : ℕ) : Fin (n + 1) → C(T4, ℂ)

The vertex weights of the order-n physical Neumann action: the first n vertices carry the continuous multiplier and the last vertex carries the input Fourier character.

Equations

• Anderson4D.neumannActionPathWeight m β n i = Fin.lastCases (Anderson4D.charT4Continuous β) (fun (x : Fin n) => m) i

@[simp]

theorem Anderson4D.neumannActionPathWeight_last (m : C(T4, ℂ)) (β : Z4) (n : ℕ) : neumannActionPathWeight m β n (Fin.last n) = charT4Continuous β

@[simp]

theorem Anderson4D.neumannActionPathWeight_castSucc (m : C(T4, ℂ)) (β : Z4) (n : ℕ) (i : Fin n) : neumannActionPathWeight m β n i.castSucc = m

@[simp]

theorem Anderson4D.neumannActionPathWeight_zero_succ (m : C(T4, ℂ)) (β : Z4) (n : ℕ) : neumannActionPathWeight m β (n + 1) 0 = m

@[simp]

theorem Anderson4D.neumannActionPathWeight_succ (m : C(T4, ℂ)) (β : Z4) (n : ℕ) (i : Fin (n + 1)) : neumannActionPathWeight m β (n + 1) i.succ = neumannActionPathWeight m β n i

theorem Anderson4D.weightedGreenPath_neumann_succ_cons (m : C(T4, ℂ)) (β : Z4) (n : ℕ) (x z : T4) (v : Fin (n + 1) → T4) : weightedGreenPath (neumannActionPathWeight m β (n + 1)) x (Fin.cons z v) = ↑(greenFn (x - z)) * m z * weightedGreenPath (neumannActionPathWeight m β n) z v

Removing the first vertex of the order-n+1 path leaves exactly the order-n path.

theorem Anderson4D.continuousNeumannAction_eq_weightedGreenPath_ae (m : C(T4, ℂ)) (β : Z4) (n : ℕ) : ∀ᵐ (x : T4) ∂paperMeasure, (continuousNeumannAction m β n) x = ∫ (v : Fin (n + 1) → T4), weightedGreenPath (neumannActionPathWeight m β n) x v ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure

Every recursive physical Neumann action is the corresponding flat Green-path integral for almost every left endpoint.

Identification with the paper's flat product

noncomputable def Anderson4D.continuousNeumannFlatIntegrand (m : C(T4, ℂ)) (β : Z4) (n : ℕ) (x y : T4) (v : Fin n → T4) : ℂ

Flat complex Green-chain integrand with a continuous multiplier. The final character is included as the last vertex weight.

Equations

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

theorem Anderson4D.assemble_cons_succ_path (n : ℕ) (x y z : T4) (v : Fin n → T4) (i : Fin (n + 2)) : assemble x y (Fin.cons z v) i.succ = assemble z y v i

Dropping the first internal point from an assembled nonempty chain turns that point into the new left endpoint.

theorem Anderson4D.continuousNeumannFlatIntegrand_succ_cons (m : C(T4, ℂ)) (β : Z4) (n : ℕ) (x z y : T4) (v : Fin n → T4) : continuousNeumannFlatIntegrand m β (n + 1) x y (Fin.cons z v) = ↑(greenFn (x - z)) * m z * continuousNeumannFlatIntegrand m β n z y v

A nonempty flat product separates into its first Green edge and multiplier followed by the shorter flat product.

theorem Anderson4D.weightedGreenPath_neumann_snoc (m : C(T4, ℂ)) (β : Z4) (n : ℕ) (x y : T4) (v : Fin n → T4) : weightedGreenPath (neumannActionPathWeight m β n) x (Fin.snoc v y) = continuousNeumannFlatIntegrand m β n x y v

The recursive weighted path is exactly the assembled flat product after the terminal vertex is separated.

theorem Anderson4D.continuousNeumannAction_eq_flatIntegral_ae (m : C(T4, ℂ)) (β : Z4) (n : ℕ) : ∀ᵐ (x : T4) ∂paperMeasure, (continuousNeumannAction m β n) x = ∫ (y : T4), ∫ (v : Fin n → T4), continuousNeumannFlatIntegrand m β n x y v ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure ∂paperMeasure

A.e. flat-product form of the recursive physical action.

theorem Anderson4D.continuousNeumannFlatIntegrand_eq_physical_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (β : Z4) (n : ℕ) (x y : T4) (v : Fin n → T4) : continuousNeumannFlatIntegrand (measurableMollifiedPotential M ρ lam ε ω) β n x y v = ↑((∏ e : Fin (n + 1), greenFn (assemble x y v e.castSucc - assemble x y v e.succ)) * ∏ i : Fin n, multFun M ρ lam ε (v i) ω) * charT4 β y

On an absolutely summable noise sample, the continuous flat product is exactly the integrand used in the paper's neumannTermKernel.

theorem Anderson4D.continuousNeumannAction_eq_neumannTermKernel_ae_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (β : Z4) (n : ℕ) : ∀ᵐ (x : T4) ∂paperMeasure, (continuousNeumannAction (measurableMollifiedPotential M ρ lam ε ω) β n) x = ∫ (y : T4), neumannTermKernel M ρ lam ε n x y ω * charT4 β y ∂paperMeasure

A.e. kernel form of every recursive physical Neumann action.

theorem Anderson4D.neumannTermKernelAction_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (β : Z4) (n : ℕ) : NeumannTermKernelAction M ρ lam ε n β ω

All-order physical/operator bridge. Absolute Fourier summability of the mollified sample implies the exact NeumannTermKernelAction at every order.

theorem Anderson4D.torusOperatorModeCoeffH_eq_neumannCoeff_tail_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (hK : ‖andersonK M ρ lam ε ω‖ < 1) : torusOperatorModeCoeffH M ρ lam ε α β ω = (↑paperTorusVolume)⁻¹ * ∑' (n : ℕ), neumannCoeff M ρ lam ε (n + 1) α β ω

Absolute Fourier summability discharges every kernel-action hypothesis in the Neumann-tail coefficient bridge.

theorem Anderson4D.torusOperatorModeCoeffH_eq_scaled_modeHcoeff_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (hK : ‖andersonK M ρ lam ε ω‖ < 1) (hLam : lamEps lam ε ≠ 0) : torusOperatorModeCoeffH M ρ lam ε α β ω = (lamEps lam ε / paperTorusVolume) • modeHcoeff M ρ lam ε α β ω

On an absolutely summable sample, the operator and coefficient routes to the recentered inverse agree with the exact normalization from the paper.

theorem Anderson4D.pow_andersonK_apply_char_ae_eq_weightedGreenPath_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (β : Z4) (n : ℕ) : ↑↑((andersonK M ρ lam ε ω ^ n * greenL2Op) (charT4Lp 2 β)) =ᵐ[haarT4] fun (x : T4) => ∫ (v : Fin (n + 1) → T4), weightedGreenPath (neumannActionPathWeight (measurableMollifiedPotential M ρ lam ε ω) β n) x v ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure

The all-order flat path is the a.e. representative of the operator-valued Neumann power.