Compactness of the torus Green multiplier

The multiplier (1 + |k|²)⁻¹ is the operator-norm limit of its finite Fourier-cube truncations. This supplies the compactness input required by the one-sided Fredholm parametrix argument.

Finite Fourier cubes

noncomputable def Anderson4D.z4Cube (N : ℕ) : Finset Z4

The integer-frequency cube [-N,N]⁴.

Equations

• Anderson4D.z4Cube N = Fintype.piFinset fun (x : Fin Anderson4D.dim) => Finset.Icc (-↑N) ↑N

@[simp]

theorem Anderson4D.mem_z4Cube (N : ℕ) (k : Z4) : k ∈ z4Cube N ↔ ∀ (i : Fin dim), -↑N ≤ k i ∧ k i ≤ ↑N

theorem Anderson4D.exists_coord_abs_gt_of_not_mem_z4Cube (N : ℕ) (k : Z4) (hk : k ∉ z4Cube N) : ∃ (i : Fin dim), ↑N < |k i|

noncomputable def Anderson4D.greenL2TruncatedSymbol (N : ℕ) (k : Z4) : ℂ

Green symbol cut off to the finite frequency cube.

Equations

• Anderson4D.greenL2TruncatedSymbol N k = if k ∈ Anderson4D.z4Cube N then Anderson4D.greenL2Symbol k else 0

theorem Anderson4D.greenL2TruncatedSymbol_norm_le_one (N : ℕ) (k : Z4) : ‖greenL2TruncatedSymbol N k‖ ≤ 1

noncomputable def Anderson4D.greenL2TruncatedOp (N : ℕ) : ↥TorusL2 →L[ℂ] ↥TorusL2

The finite Fourier-cube truncation of greenL2Op.

Equations

• Anderson4D.greenL2TruncatedOp N = Anderson4D.torusL2MultiplierCLM (Anderson4D.greenL2TruncatedSymbol N) 1 ⋯ ⋯

@[simp]

theorem Anderson4D.torusFourierCoeff_greenL2TruncatedOp (N : ℕ) (f : ↥TorusL2) (k : Z4) : torusFourierCoeff (↑↑((greenL2TruncatedOp N) f)) k = greenL2TruncatedSymbol N k * torusFourierCoeff (↑↑f) k

Finite-rank compactness

theorem Anderson4D.isCompactOperator_torus_rankOne (k : Z4) : IsCompactOperator ⇑(((InnerProductSpace.rankOne ℂ) (torusFourierBasis k)) (torusFourierBasis k))

@[simp]

theorem Anderson4D.torusFourierCoeff_rankOne_basis (k l : Z4) (f : ↥TorusL2) : torusFourierCoeff (↑↑((((InnerProductSpace.rankOne ℂ) (torusFourierBasis k)) (torusFourierBasis k)) f)) l = if l = k then torusFourierCoeff (↑↑f) k else 0

theorem Anderson4D.greenL2TruncatedOp_eq_rankOne_sum (N : ℕ) : greenL2TruncatedOp N = ∑ k ∈ z4Cube N, greenL2Symbol k • ((InnerProductSpace.rankOne ℂ) (torusFourierBasis k)) (torusFourierBasis k)

theorem Anderson4D.isCompactOperator_finset_sum_torus {ι : Type u_1} (s : Finset ι) (F : ι → ↥TorusL2 →L[ℂ] ↥TorusL2) (hF : ∀ i ∈ s, IsCompactOperator ⇑(F i)) : IsCompactOperator ⇑(∑ i ∈ s, F i)

theorem Anderson4D.isCompactOperator_greenL2TruncatedOp (N : ℕ) : IsCompactOperator ⇑(greenL2TruncatedOp N)

Uniform tail control

noncomputable def Anderson4D.greenL2TailBound (N : ℕ) : ℝ

Uniform bound for frequencies outside z4Cube N.

Equations

• Anderson4D.greenL2TailBound N = (1 + ↑N ^ 2)⁻¹

theorem Anderson4D.greenL2TailBound_nonneg (N : ℕ) : 0 ≤ greenL2TailBound N

noncomputable def Anderson4D.greenL2TailSymbol (N : ℕ) (k : Z4) : ℂ

Symbol of the Fourier tail discarded by the finite truncation.

Equations

• Anderson4D.greenL2TailSymbol N k = if k ∈ Anderson4D.z4Cube N then 0 else Anderson4D.greenL2Symbol k

theorem Anderson4D.greenL2TailSymbol_norm_le (N : ℕ) (k : Z4) : ‖greenL2TailSymbol N k‖ ≤ greenL2TailBound N

theorem Anderson4D.tendsto_greenL2TailBound : Filter.Tendsto greenL2TailBound Filter.atTop (nhds 0)

noncomputable def Anderson4D.greenL2TailOp (N : ℕ) : ↥TorusL2 →L[ℂ] ↥TorusL2

The discarded Fourier tail as a bounded operator.

Equations

• Anderson4D.greenL2TailOp N = Anderson4D.torusL2MultiplierCLM (Anderson4D.greenL2TailSymbol N) (Anderson4D.greenL2TailBound N) ⋯ ⋯

@[simp]

theorem Anderson4D.torusFourierCoeff_greenL2TailOp (N : ℕ) (f : ↥TorusL2) (k : Z4) : torusFourierCoeff (↑↑((greenL2TailOp N) f)) k = greenL2TailSymbol N k * torusFourierCoeff (↑↑f) k

theorem Anderson4D.torusFourierCoeff_sub (f g : ↥TorusL2) (k : Z4) : torusFourierCoeff (↑↑(f - g)) k = torusFourierCoeff (↑↑f) k - torusFourierCoeff (↑↑g) k

theorem Anderson4D.greenL2Op_sub_truncated_eq_tail (N : ℕ) : greenL2Op - greenL2TruncatedOp N = greenL2TailOp N

theorem Anderson4D.norm_greenL2Op_sub_truncated_le (N : ℕ) : ‖greenL2Op - greenL2TruncatedOp N‖ ≤ greenL2TailBound N

theorem Anderson4D.tendsto_greenL2TruncatedOp : Filter.Tendsto greenL2TruncatedOp Filter.atTop (nhds greenL2Op)

theorem Anderson4D.isCompactOperator_greenL2Op : IsCompactOperator ⇑greenL2Op

The torus Green operator is compact.

theorem Anderson4D.isCompactOperator_Kop_greenL2Op (M : ↥TorusL2 →L[ℂ] ↥TorusL2) : IsCompactOperator ⇑(Kop greenL2Op M)

Composing the compact Green operator with an arbitrary bounded multiplication operator preserves compactness.