Kernel-to-operator normalization bridge on torus L²

The physical coefficients in paper (3.23) integrate both external variables against the unnormalized torus measure paperMeasure, while TorusL2 uses probability Haar measure. Therefore a kernel acting by integration against paperMeasure has

paperKernelCoeff K α β = volume(T⁴) * ⟪e_{-α}, T_K e_β⟫.

This factor is essential. The file packages that ledger identity, defines the physical Neumann-term kernel, and states the exact kernel-action interface required to identify it with the bounded operator power K^n G.

noncomputable def Anderson4D.paperTorusVolume : ℝ

Total mass of the paper's four-dimensional torus measure.

Equations

• Anderson4D.paperTorusVolume = (2 * Real.pi) ^ Anderson4D.dim

theorem Anderson4D.paperTorusVolume_pos : 0 < paperTorusVolume

theorem Anderson4D.paperTorusVolume_ne_zero : paperTorusVolume ≠ 0

Generic kernel action

theorem Anderson4D.paperKernelCoeff_eq_volume_mul_inner_of_action (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (kernel : T4 → T4 → ℂ) (α β : Z4) (hAction : ↑↑(A (charT4Lp 2 β)) =ᵐ[haarT4] fun (x : T4) => ∫ (y : T4), kernel x y * charT4 β y ∂paperMeasure) : paperKernelCoeff kernel α β = ↑paperTorusVolume * inner ℂ (charT4Lp 2 (-α)) (A (charT4Lp 2 β))

It suffices to know the action of a kernel operator on one Fourier character in order to identify the corresponding matrix coefficient. No Fubini hypothesis is hidden here: both sides use the same iterated integral order.

theorem Anderson4D.inner_eq_volume_inv_mul_paperKernelCoeff_of_action (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (kernel : T4 → T4 → ℂ) (α β : Z4) (hAction : ↑↑(A (charT4Lp 2 β)) =ᵐ[haarT4] fun (x : T4) => ∫ (y : T4), kernel x y * charT4 β y ∂paperMeasure) : inner ℂ (charT4Lp 2 (-α)) (A (charT4Lp 2 β)) = (↑paperTorusVolume)⁻¹ * paperKernelCoeff kernel α β

Division form of the normalization ledger.

Physical Neumann kernels

noncomputable def Anderson4D.neumannTermKernel (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : ℂ

Kernel of the n-th physical Neumann term, with all n multiplication points integrated against the paper measure.

Equations

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

theorem Anderson4D.neumannCoeff_eq_paperKernelCoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (α β : Z4) (ω : M.Ω) : neumannCoeff M ρ lam ε n α β ω = paperKernelCoeff (fun (x1 x2 : T4) => neumannTermKernel M ρ lam ε n x1 x2 ω) α β

def Anderson4D.NeumannTermKernelAction (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (β : Z4) (ω : M.Ω) : Prop

The exact upstream interface for the physical/operator bridge: K^n G acts on a Fourier character by the chain kernel from neumannCoeff.

Equations

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

theorem Anderson4D.inner_pow_andersonK_mul_green_eq_neumannCoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (α β : Z4) (ω : M.Ω) (hAction : NeumannTermKernelAction M ρ lam ε n β ω) : inner ℂ (charT4Lp 2 (-α)) ((andersonK M ρ lam ε ω ^ n * greenL2Op) (charT4Lp 2 β)) = (↑paperTorusVolume)⁻¹ * neumannCoeff M ρ lam ε n α β ω

Once the kernel-action identity is available, the matrix coefficient is the physical Neumann coefficient divided by exactly one torus-volume factor.

The order-zero sanity check

@[simp]

theorem Anderson4D.greenL2Symbol_neg (k : Z4) : greenL2Symbol (-k) = greenL2Symbol k

theorem Anderson4D.greenL2Op_char (k : Z4) : greenL2Op (charT4Lp 2 k) = greenL2Symbol k • charT4Lp 2 k

The Fourier multiplier acts diagonally on a character.

theorem Anderson4D.charT4_sub_apply (k : Z4) (x y : T4) : charT4 k (x - y) = charT4 k x * (starRingEnd ℂ) (charT4 k y)

A character turns spatial subtraction into multiplication by its conjugate.

theorem Anderson4D.integral_greenFn_sub_mul_char (k : Z4) (x : T4) : ∫ (y : T4), ↑(greenFn (x - y)) * charT4 k y ∂paperMeasure = greenL2Symbol k * charT4 k x

The heat-kernel Green function, integrated against the paper measure, realizes the same multiplier on a single character.

theorem Anderson4D.greenL2Op_char_action (k : Z4) : ↑↑(greenL2Op (charT4Lp 2 k)) =ᵐ[haarT4] fun (x : T4) => ∫ (y : T4), ↑(greenFn (x - y)) * charT4 k y ∂paperMeasure

Concrete kernel action for the zeroth Neumann term.

@[simp]

theorem Anderson4D.neumannTermKernel_zero (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (x y : T4) (ω : M.Ω) : neumannTermKernel M ρ lam ε 0 x y ω = ↑(greenFn (x - y))

theorem Anderson4D.neumannTermKernelAction_zero (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (β : Z4) (ω : M.Ω) : NeumannTermKernelAction M ρ lam ε 0 β ω

The physical/operator bridge is unconditional at order zero.

theorem Anderson4D.inner_greenL2Op_eq_neumannCoeff_zero (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) : inner ℂ (charT4Lp 2 (-α)) (greenL2Op (charT4Lp 2 β)) = (↑paperTorusVolume)⁻¹ * neumannCoeff M ρ lam ε 0 α β ω

The norm-small Neumann tail

theorem Anderson4D.neumannInverse_mul_apply_sub_eq_tsum_tail (K G : ↥TorusL2 →L[ℂ] ↥TorusL2) (hK : ‖K‖ < 1) (f : ↥TorusL2) : (neumannInverse K hK * G - G) f = ∑' (n : ℕ), (K ^ (n + 1) * G) f

Pointwise subtraction of the zeroth term from the operator-valued Neumann series.

theorem Anderson4D.inner_neumannInverse_mul_apply_sub_eq_tsum_tail (K G : ↥TorusL2 →L[ℂ] ↥TorusL2) (hK : ‖K‖ < 1) (e f : ↥TorusL2) : inner ℂ e ((neumannInverse K hK * G - G) f) = ∑' (n : ℕ), inner ℂ e ((K ^ (n + 1) * G) f)

Taking a fixed Hilbert-space matrix coefficient commutes with the norm-small Neumann tail.

theorem Anderson4D.inner_neumannInverse_mul_green_sub_eq_neumannCoeff_tail (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) (hK : ‖andersonK M ρ lam ε ω‖ < 1) (hAction : ∀ (n : ℕ), NeumannTermKernelAction M ρ lam ε (n + 1) β ω) : inner ℂ (charT4Lp 2 (-α)) ((neumannInverse (andersonK M ρ lam ε ω) hK * greenL2Op - greenL2Op) (charT4Lp 2 β)) = (↑paperTorusVolume)⁻¹ * ∑' (n : ℕ), neumannCoeff M ρ lam ε (n + 1) α β ω

If the physical chain kernel realizes every positive operator power on the chosen input mode, the full recentered Neumann matrix coefficient is the physical coefficient tail divided by one torus volume.

theorem Anderson4D.torusOperatorModeCoeffH_eq_neumannCoeff_tail (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) (hK : ‖andersonK M ρ lam ε ω‖ < 1) (hAction : ∀ (n : ℕ), NeumannTermKernelAction M ρ lam ε (n + 1) β ω) : torusOperatorModeCoeffH M ρ lam ε α β ω = (↑paperTorusVolume)⁻¹ * ∑' (n : ℕ), neumannCoeff M ρ lam ε (n + 1) α β ω

On the norm-small event, the project's totalized concrete inverse selects the Neumann inverse, so its Fourier matrix coefficient equals the physical coefficient tail with the normalization ledger applied.

theorem Anderson4D.torusOperatorModeCoeffH_eq_scaled_modeHcoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) (hK : ‖andersonK M ρ lam ε ω‖ < 1) (hLam : lamEps lam ε ≠ 0) (hAction : ∀ (n : ℕ), NeumannTermKernelAction M ρ lam ε (n + 1) β ω) : torusOperatorModeCoeffH M ρ lam ε α β ω = (lamEps lam ε / paperTorusVolume) • modeHcoeff M ρ lam ε α β ω

Exact comparison with the paper's coefficient-route definition. There are two indispensable scalars: lamEps because modeHcoeff describes lamEps⁻¹ (Gε - G), and paperTorusVolume⁻¹ because the physical coefficient uses the unnormalized torus measure in both external variables while TorusL2 uses probability Haar.