Concrete bounded operators on torus L²

This file realizes the abstract bounded-operator layer used in paper §3.4, Step 1, on L²(𝕋⁴, haarT4).

The Green operator is the Fourier multiplier with symbol (1 + |k|²)⁻¹. Multiplication by a measurable essentially bounded function is constructed directly on L², with its pointwise action and operator-norm bound exposed. The mollified Anderson potential is then an instance whenever its almost-sure continuity (hence boundedness on the compact torus) is supplied.

@[reducible, inline]

noncomputable abbrev Anderson4D.TorusL2 : AddSubgroup (T4 →ₘ[haarT4] ℂ)

The Hilbert space used by the bounded resolvent realization.

Equations

• Anderson4D.TorusL2 = MeasureTheory.Lp ℂ 2 Anderson4D.haarT4

The Green Fourier multiplier

noncomputable def Anderson4D.greenL2Symbol (k : Z4) : ℂ

Fourier symbol of (1 - Δ)⁻¹ on the four-dimensional torus.

Equations

• Anderson4D.greenL2Symbol k = ↑(1 + ∑ i : Fin Anderson4D.dim, ↑(k i) ^ 2)⁻¹

theorem Anderson4D.greenL2Symbol_norm_le_one (k : Z4) : ‖greenL2Symbol k‖ ≤ 1

noncomputable def Anderson4D.greenL2Op : ↥TorusL2 →L[ℂ] ↥TorusL2

The bounded Green operator on torus L², defined by its Fourier multiplier rather than by an ill-defined pointwise Fourier series.

Equations

• Anderson4D.greenL2Op = Anderson4D.torusL2MultiplierCLM Anderson4D.greenL2Symbol 1 ⋯ Anderson4D.greenL2Symbol_norm_le_one

@[simp]

theorem Anderson4D.torusFourierCoeff_greenL2Op (f : ↥TorusL2) (k : Z4) : torusFourierCoeff (↑↑(greenL2Op f)) k = greenL2Symbol k * torusFourierCoeff (↑↑f) k

theorem Anderson4D.norm_greenL2Op_le_one : ‖greenL2Op‖ ≤ 1

theorem Anderson4D.paperFourierCoeff_greenFn_eq_greenL2Symbol (k : Z4) : ∫ (z : T4), charT4 k z * ↑(greenFn z) ∂paperMeasure = greenL2Symbol k

The concrete multiplier symbol agrees with the coefficient of the heat-kernel definition of greenFn against the paper measure.

Multiplication by an essentially bounded function

theorem Anderson4D.memLp_bounded_mul (m : T4 → ℂ) (C : ℝ) (hm : MeasureTheory.AEStronglyMeasurable m haarT4) (hC : ∀ᵐ (x : T4) ∂haarT4, ‖m x‖ ≤ C) (f : ↥TorusL2) : MeasureTheory.MemLp (fun (x : T4) => m x * ↑↑f x) 2 haarT4

A pointwise bound turns multiplication by m into an L² function.

noncomputable def Anderson4D.boundedMultiplicationLM (m : T4 → ℂ) (C : ℝ) (hm : MeasureTheory.AEStronglyMeasurable m haarT4) (hC : ∀ᵐ (x : T4) ∂haarT4, ‖m x‖ ≤ C) : ↥TorusL2 →ₗ[ℂ] ↥TorusL2

Multiplication by a measurable function bounded by C, as a linear map on torus L².

Equations

• Anderson4D.boundedMultiplicationLM m C hm hC = { toFun := fun (f : ↥Anderson4D.TorusL2) => MeasureTheory.MemLp.toLp (fun (x : Anderson4D.T4) => m x * ↑↑f x) ⋯, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Anderson4D.boundedMultiplicationLM_apply_ae (m : T4 → ℂ) (C : ℝ) (hm : MeasureTheory.AEStronglyMeasurable m haarT4) (hC : ∀ᵐ (x : T4) ∂haarT4, ‖m x‖ ≤ C) (f : ↥TorusL2) : ↑↑((boundedMultiplicationLM m C hm hC) f) =ᵐ[haarT4] fun (x : T4) => m x * ↑↑f x

theorem Anderson4D.norm_boundedMultiplicationLM_apply_le (m : T4 → ℂ) (C : ℝ) (hm : MeasureTheory.AEStronglyMeasurable m haarT4) (hC : ∀ᵐ (x : T4) ∂haarT4, ‖m x‖ ≤ C) (f : ↥TorusL2) : ‖(boundedMultiplicationLM m C hm hC) f‖ ≤ C * ‖f‖

noncomputable def Anderson4D.boundedMultiplicationCLM (m : T4 → ℂ) (C : ℝ) (_hC0 : 0 ≤ C) (hm : MeasureTheory.AEStronglyMeasurable m haarT4) (hC : ∀ᵐ (x : T4) ∂haarT4, ‖m x‖ ≤ C) : ↥TorusL2 →L[ℂ] ↥TorusL2

Multiplication by an essentially bounded function, as a continuous linear map on torus L².

Equations

• Anderson4D.boundedMultiplicationCLM m C _hC0 hm hC = (Anderson4D.boundedMultiplicationLM m C hm hC).mkContinuous C ⋯

@[simp]

theorem Anderson4D.boundedMultiplicationCLM_apply_ae (m : T4 → ℂ) (C : ℝ) (hC0 : 0 ≤ C) (hm : MeasureTheory.AEStronglyMeasurable m haarT4) (hC : ∀ᵐ (x : T4) ∂haarT4, ‖m x‖ ≤ C) (f : ↥TorusL2) : ↑↑((boundedMultiplicationCLM m C hC0 hm hC) f) =ᵐ[haarT4] fun (x : T4) => m x * ↑↑f x

theorem Anderson4D.boundedMultiplicationCLM_norm_le (m : T4 → ℂ) (C : ℝ) (hC0 : 0 ≤ C) (hm : MeasureTheory.AEStronglyMeasurable m haarT4) (hC : ∀ᵐ (x : T4) ∂haarT4, ‖m x‖ ≤ C) : ‖boundedMultiplicationCLM m C hC0 hm hC‖ ≤ C

The mollified Anderson potential

noncomputable def Anderson4D.mollifiedPotentialC (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (x : T4) : ℂ

The real mollified potential, embedded into ℂ for its action on the complex Hilbert space.

Equations

• Anderson4D.mollifiedPotentialC M ρ lam ε ω x = ↑(Anderson4D.multFun M ρ lam ε x ω)

theorem Anderson4D.continuous_mollifiedPotentialC (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : Continuous (mollifiedPotentialC M ρ lam ε ω)

noncomputable def Anderson4D.mollifiedPotentialContinuousMap (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : C(T4, ℂ)

Continuous-map packaging of a sample of the mollified potential. Its norm is the concrete L∞ bound used below.

Equations

• Anderson4D.mollifiedPotentialContinuousMap M ρ lam ε ω hξ = { toFun := Anderson4D.mollifiedPotentialC M ρ lam ε ω, continuous_toFun := ⋯ }

noncomputable def Anderson4D.mollifiedPotentialL2Op (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ↥TorusL2 →L[ℂ] ↥TorusL2

Multiplication by the mollified potential on L², with a junk-zero value on the exceptional samples where the totalized Fourier series is not continuous. Positive scales lie in the non-junk branch almost surely.

Equations

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

theorem Anderson4D.mollifiedPotentialL2Op_apply_ae_of_continuous (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) (f : ↥TorusL2) : ↑↑((mollifiedPotentialL2Op M ρ lam ε ω) f) =ᵐ[haarT4] fun (x : T4) => mollifiedPotentialC M ρ lam ε ω x * ↑↑f x

theorem Anderson4D.mollifiedPotentialL2Op_norm_le_of_continuous (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ‖mollifiedPotentialL2Op M ρ lam ε ω‖ ≤ ‖mollifiedPotentialContinuousMap M ρ lam ε ω hξ‖

theorem Anderson4D.ae_mollifiedPotentialL2Op_apply_ae (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (f : ↥TorusL2) : ∀ᵐ (ω : M.Ω), ↑↑((mollifiedPotentialL2Op M ρ lam ε ω) f) =ᵐ[haarT4] fun (x : T4) => mollifiedPotentialC M ρ lam ε ω x * ↑↑f x

At positive scale, the concrete multiplier acts by the intended potential almost surely in the noise sample.

The concrete random K = G M and good event

noncomputable def Anderson4D.andersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ↥TorusL2 →L[ℂ] ↥TorusL2

The bounded random operator Kε = G ∘ Mε of DESIGN §5.2.

Equations

• Anderson4D.andersonK M ρ lam ε ω = Anderson4D.Kop Anderson4D.greenL2Op (Anderson4D.mollifiedPotentialL2Op M ρ lam ε ω)

@[simp]

theorem Anderson4D.andersonK_apply (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (f : ↥TorusL2) : (andersonK M ρ lam ε ω) f = greenL2Op ((mollifiedPotentialL2Op M ρ lam ε ω) f)

@[simp]

theorem Anderson4D.torusFourierCoeff_andersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (f : ↥TorusL2) (k : Z4) : torusFourierCoeff (↑↑((andersonK M ρ lam ε ω) f)) k = greenL2Symbol k * torusFourierCoeff (↑↑((mollifiedPotentialL2Op M ρ lam ε ω) f)) k

theorem Anderson4D.norm_andersonK_le_potential (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ‖andersonK M ρ lam ε ω‖ ≤ ‖mollifiedPotentialL2Op M ρ lam ε ω‖

def Anderson4D.andersonResolventGoodEvent (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) : Set M.Ω

The concrete half-ball event on which the resolvent exists.

Equations

• Anderson4D.andersonResolventGoodEvent M ρ lam ε = Anderson4D.resolventGoodEvent Anderson4D.greenL2Op (Anderson4D.mollifiedPotentialL2Op M ρ lam ε)

theorem Anderson4D.lopInvertible_on_andersonResolventGoodEvent (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) {ω : M.Ω} (hω : ω ∈ andersonResolventGoodEvent M ρ lam ε) : LopInvertible greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω)

noncomputable def Anderson4D.andersonRecenteredInverse (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) : ↥TorusL2 →L[ℂ] ↥TorusL2

The recentered inverse, totalized to zero off the invertibility event. This is the operator whose fixed matrix coefficients enter the finite-mode convergence statement.

Equations

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

theorem Anderson4D.andersonRecenteredInverse_eq_on_good (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) {ω : M.Ω} (hω : ω ∈ andersonResolventGoodEvent M ρ lam ε) : andersonRecenteredInverse M ρ lam ε ω = inverseGreen greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω) ⋯ - greenL2Op

noncomputable def Anderson4D.torusOperatorModeCoeffH (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) : ℂ

(3.23)-signed Fourier matrix coefficient of the concrete recentered inverse.

Equations

• Anderson4D.torusOperatorModeCoeffH M ρ lam ε α β ω = inner ℂ (Anderson4D.charT4Lp 2 (-α)) ((Anderson4D.andersonRecenteredInverse M ρ lam ε ω) (Anderson4D.charT4Lp 2 β))

theorem Anderson4D.torusOperatorModeCoeffH_eq_abstract (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) : torusOperatorModeCoeffH M ρ lam ε α β ω = operatorModeCoeffH greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω) (charT4Lp 2) α β

theorem Anderson4D.inverseGreen_eq_neumann_andersonK (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (ω : M.Ω) (hK : ‖andersonK M ρ lam ε ω‖ < 1) : inverseGreen greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω) ⋯ = neumannInverse (andersonK M ρ lam ε ω) hK * greenL2Op

In the norm-small regime, the selected inverse is the actual operator-valued Neumann series followed by G.

theorem Anderson4D.measureReal_compl_andersonResolventGoodEvent_le (M : NoiseModel) (ρ : SmoothCutoff) (lam ε δ : ℝ) (hint : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖andersonK M ρ lam ε ω‖ ^ 2) MeasureTheory.volume) (hsecond : ∫ (ω : M.Ω), ‖andersonK M ρ lam ε ω‖ ^ 2 ≤ δ) : MeasureTheory.volume.real (andersonResolventGoodEvent M ρ lam ε)ᶜ ≤ 4 * δ

The abstract second-moment/Markov estimate specialized to the concrete torus operators. Establishing its two analytic premises is the remaining estimate in P-L2, not an operator-definition gap.