Recursive physical realization of the L² Neumann powers

This file iterates the Green-convolution theorem. For a continuous multiplier m, it packages the alternating sequence

G eβ, G(m G eβ), G(m G(m G eβ)), ...

as continuous functions and proves that their L² classes are exactly (G M_m)^n G eβ. For samples on which the mollified Fourier series is absolutely summable, the multiplier is pointwise the paper's multFun, and the measurable and samplewise operator realizations coincide.

theorem Anderson4D.instPaperMeasureIsAddRightInvariantNeumannAction : paperMeasure.IsAddRightInvariant

theorem Anderson4D.continuousMultiplicationOp_toLp (m f : C(T4, ℂ)) : (continuousMultiplicationOp m) ((ContinuousMap.toLp 2 haarT4 ℂ) f) = (ContinuousMap.toLp 2 haarT4 ℂ) (m * f)

Multiplication of two continuous functions commutes with passage to L².

def Anderson4D.continuousNeumannAction (m : C(T4, ℂ)) (β : Z4) : ℕ → C(T4, ℂ)

Recursive continuous representative of the physical Neumann action with multiplier m.

Equations

• Anderson4D.continuousNeumannAction m β 0 = Anderson4D.greenPhysicalConvolution (Anderson4D.charT4Continuous β)
• Anderson4D.continuousNeumannAction m β n.succ = Anderson4D.greenPhysicalConvolution (m * Anderson4D.continuousNeumannAction m β n)

@[simp]

theorem Anderson4D.continuousNeumannAction_zero (m : C(T4, ℂ)) (β : Z4) : continuousNeumannAction m β 0 = greenPhysicalConvolution (charT4Continuous β)

@[simp]

theorem Anderson4D.continuousNeumannAction_succ (m : C(T4, ℂ)) (β : Z4) (n : ℕ) : continuousNeumannAction m β (n + 1) = greenPhysicalConvolution (m * continuousNeumannAction m β n)

theorem Anderson4D.continuousNeumannAction_zero_apply (m : C(T4, ℂ)) (β : Z4) (x : T4) : (continuousNeumannAction m β 0) x = ∫ (y : T4), ↑(greenFn (x - y)) * charT4 β y ∂paperMeasure

theorem Anderson4D.continuousNeumannAction_succ_apply (m : C(T4, ℂ)) (β : Z4) (n : ℕ) (x : T4) : (continuousNeumannAction m β (n + 1)) x = ∫ (y : T4), ↑(greenFn (x - y)) * (m y * (continuousNeumannAction m β n) y) ∂paperMeasure

theorem Anderson4D.pow_green_mul_continuousMultiplication_apply_char (m : C(T4, ℂ)) (β : Z4) (n : ℕ) : (Kop greenL2Op (continuousMultiplicationOp m) ^ n * greenL2Op) (charT4Lp 2 β) = (ContinuousMap.toLp 2 haarT4 ℂ) (continuousNeumannAction m β n)

Exact operator realization of every recursive physical Neumann action.

theorem Anderson4D.pow_measurableAndersonK_apply_char (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (β : Z4) (n : ℕ) : (measurableAndersonK M ρ lam ε ω ^ n * greenL2Op) (charT4Lp 2 β) = (ContinuousMap.toLp 2 haarT4 ℂ) (continuousNeumannAction (measurableMollifiedPotential M ρ lam ε ω) β n)

The continuous totalization of the random potential gives the same formula for the preferred measurable random operator.

theorem Anderson4D.continuous_xiEps_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) : Continuous (M.xiEps ρ ε ω)

Absolute Fourier summability forces the original real field totalization to be continuous.

theorem Anderson4D.measurableMollifiedPotentialL2Op_eq_mollifiedPotentialL2Op (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) : measurableMollifiedPotentialL2Op M ρ lam ε ω = mollifiedPotentialL2Op M ρ lam ε ω

On an absolutely summable sample, the measurable continuous-map multiplier equals the original samplewise multiplication operator.

theorem Anderson4D.continuousNeumannAction_succ_apply_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (β : Z4) (n : ℕ) (x : T4) : (continuousNeumannAction (measurableMollifiedPotential M ρ lam ε ω) β (n + 1)) x = ∫ (y : T4), ↑(greenFn (x - y)) * (↑(multFun M ρ lam ε y ω) * (continuousNeumannAction (measurableMollifiedPotential M ρ lam ε ω) β n) y) ∂paperMeasure

theorem Anderson4D.measurableAndersonK_eq_andersonK_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) : measurableAndersonK M ρ lam ε ω = andersonK M ρ lam ε ω

theorem Anderson4D.pow_andersonK_apply_char_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) (β : Z4) (n : ℕ) : (andersonK M ρ lam ε ω ^ n * greenL2Op) (charT4Lp 2 β) = (ContinuousMap.toLp 2 haarT4 ℂ) (continuousNeumannAction (measurableMollifiedPotential M ρ lam ε ω) β n)

Every samplewise operator power has the explicit recursive physical-convolution representative on the full-measure Fourier summability event.

theorem Anderson4D.pow_andersonK_apply_char_ae_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] ⇑(continuousNeumannAction (measurableMollifiedPotential M ρ lam ε ω) β n)

Almost-everywhere pointwise form of the recursive action.

The first nontrivial flat-chain check

theorem Anderson4D.continuousNeumannAction_one_eq_flat (m : C(T4, ℂ)) (β : Z4) (x : T4) : (continuousNeumannAction m β 1) x = ∫ (y : T4), (∫ (z : T4), ↑(greenFn (x - z)) * m z * ↑(greenFn (z - y)) ∂paperMeasure) * charT4 β y ∂paperMeasure

The first recursive action is the Fubini flattening of its two-Green chain.

theorem Anderson4D.neumannTermKernel_one (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (x y : T4) (ω : M.Ω) : neumannTermKernel M ρ lam ε 1 x y ω = ∫ (z : T4), ↑(greenFn (x - z) * multFun M ρ lam ε z ω * greenFn (z - y)) ∂paperMeasure

Closed form of the one-internal-vertex flat kernel.

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

The physical/operator kernel bridge is unconditional at the first nontrivial order on every absolutely summable noise sample.