The conditioned Hilbert--Schmidt resolvent difference

Mathlib does not presently expose a named Hilbert--Schmidt ideal API for bounded operators on the torus L² space. Following DESIGN §5.2, this file therefore uses square summability of the matrix in the complete torus Fourier basis as the certificate.

The central point is that this certificate is an operator ideal on the left: left composition by a bounded operator preserves the double square sum. The algebraic identity inverseGreen_sub_G can consequently transfer any honest certificate for G * M * G to the recentered inverse. No certificate is asserted for G itself.

def Anderson4D.TorusFourierHSCertificate (A : ↥TorusL2 →L[ℂ] ↥TorusL2) : Prop

Fourier-matrix replacement for a Hilbert--Schmidt certificate.

The product index is ordered (input, output), so Tonelli first sums the output Fourier coefficients of the image of one basis vector.

Equations

• Anderson4D.TorusFourierHSCertificate A = Summable fun (p : Anderson4D.Z4 × Anderson4D.Z4) => ‖Anderson4D.torusFourierMatrixCoeff A p.2 p.1‖ ^ 2

theorem Anderson4D.summable_normSq_torusFourierMatrixCoeff_column (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (β : Z4) : Summable fun (α : Z4) => ‖torusFourierMatrixCoeff A α β‖ ^ 2

Every fixed column of the Fourier matrix of a bounded operator is square summable. This is Parseval, not a Hilbert--Schmidt assertion: the outer sum over columns need not converge.

theorem Anderson4D.tsum_normSq_torusFourierMatrixCoeff_left_mul_le (L A : ↥TorusL2 →L[ℂ] ↥TorusL2) (β : Z4) : ∑' (α : Z4), ‖torusFourierMatrixCoeff (L * A) α β‖ ^ 2 ≤ ‖L‖ ^ 2 * ∑' (α : Z4), ‖torusFourierMatrixCoeff A α β‖ ^ 2

Quantitative column estimate under left composition.

theorem Anderson4D.torusFourierHSCertificate_left_mul (L A : ↥TorusL2 →L[ℂ] ↥TorusL2) (hA : TorusFourierHSCertificate A) : TorusFourierHSCertificate (L * A)

The Fourier square-summability certificate is preserved by left composition by an arbitrary bounded operator.

theorem Anderson4D.tsum_torusFourierMatrixCoeff_left_mul_le (L A : ↥TorusL2 →L[ℂ] ↥TorusL2) (hA : TorusFourierHSCertificate A) : ∑' (p : Z4 × Z4), ‖torusFourierMatrixCoeff (L * A) p.2 p.1‖ ^ 2 ≤ ‖L‖ ^ 2 * ∑' (p : Z4 × Z4), ‖torusFourierMatrixCoeff A p.2 p.1‖ ^ 2

Quantitative ideal estimate for the complete Fourier double sum.

theorem Anderson4D.inverseGreen_sub_G_torusFourierHSCertificate (G M : ↥TorusL2 →L[ℂ] ↥TorusL2) (h : LopInvertible G M) (hGMG : TorusFourierHSCertificate (G * M * G)) : TorusFourierHSCertificate (inverseGreen G M h - G)

Conditioned Hilbert--Schmidt difference checkpoint from DESIGN §5.2.

Only G * M * G is assumed square summable. The conclusion follows from the resolvent identity and bounded left composition; in particular this does not assume or claim that G itself has a square-summable Fourier matrix.

theorem Anderson4D.tsum_inverseGreen_sub_G_fourierMatrixCoeff_le (G M : ↥TorusL2 →L[ℂ] ↥TorusL2) (h : LopInvertible G M) (hGMG : TorusFourierHSCertificate (G * M * G)) : ∑' (p : Z4 × Z4), ‖torusFourierMatrixCoeff (inverseGreen G M h - G) p.2 p.1‖ ^ 2 ≤ ‖↑(IsUnit.unit h)⁻¹‖ ^ 2 * ∑' (p : Z4 × Z4), ‖torusFourierMatrixCoeff (G * M * G) p.2 p.1‖ ^ 2

Quantitative form of the conditioned difference checkpoint.

The Green sandwich and the critical Fourier condition

theorem Anderson4D.torusFourierMatrixCoeff_greenL2Op_mul_mul_greenL2Op (M : ↥TorusL2 →L[ℂ] ↥TorusL2) (α β : Z4) : torusFourierMatrixCoeff (greenL2Op * M * greenL2Op) α β = greenL2Symbol α * torusFourierMatrixCoeff M α β * greenL2Symbol β

The Fourier matrix of G * M * G has one Green symbol at each endpoint. This statement holds for every bounded M; multiplication structure is only used below to identify the middle coefficient as a function of the conserved frequency α + β.

def Anderson4D.HasMultiplicationFourierProfile (M : ↥TorusL2 →L[ℂ] ↥TorusL2) (a : Z4 → ℂ) : Prop

Fourier translation structure of a multiplication operator in the paper's non-conjugated (α, β) sign convention.

Equations

• Anderson4D.HasMultiplicationFourierProfile M a = ∀ (α β : Anderson4D.Z4), Anderson4D.torusFourierMatrixCoeff M α β = a (α + β)

noncomputable def Anderson4D.greenL2SquaredConvolutionSummand (γ α : Z4) : ℝ

The exact Green-square convolution whose critical four-dimensional estimate supplies the logarithm in DESIGN §5.2.

Equations

• Anderson4D.greenL2SquaredConvolutionSummand γ α = ‖Anderson4D.greenL2Symbol α‖ ^ 2 * ‖Anderson4D.greenL2Symbol (γ - α)‖ ^ 2

theorem Anderson4D.norm_greenL2Symbol_eq_paperSecondOrderModeDecay (k : Z4) : ‖greenL2Symbol k‖ = paperSecondOrderModeDecay k

theorem Anderson4D.normSq_greenL2Symbol_le_l2LatticeRadialWeight (k : Z4) : ‖greenL2Symbol k‖ ^ 2 ≤ 4 * l2LatticeRadialWeight 4 k

theorem Anderson4D.greenL2SquaredConvolutionSummand_le (γ α : Z4) : greenL2SquaredConvolutionSummand γ α ≤ 16 * (l2LatticeRadialWeight 4 α * l2LatticeRadialWeight 4 (γ - α))

theorem Anderson4D.summable_greenL2SquaredConvolutionSummand (γ : Z4) : Summable (greenL2SquaredConvolutionSummand γ)

The exact Green-square convolution is summable without any critical logarithmic estimate. Only its sharp decay in the conserved frequency remains separate below.

theorem Anderson4D.tsum_greenL2SquaredConvolutionSummand_le_coarse (γ : Z4) : ∑' (α : Z4), greenL2SquaredConvolutionSummand γ α ≤ 256 * l2LatticeRadialWeight 3 γ * ∑' (α : Z4), l2LatticeRadialWeight 5 α

An unconditional, deliberately non-sharp ⟨γ⟩⁻³ bound obtained from the existing lattice convolution library. DESIGN §5.2 needs the sharper critical ⟨γ⟩⁻⁴(1+log⟨γ⟩) estimate isolated below.

noncomputable def Anderson4D.designJapaneseBracket (γ : Z4) : ℝ

The Euclidean Japanese bracket ⟨γ⟩ = (1 + |γ|²)^(1/2).

Equations

• Anderson4D.designJapaneseBracket γ = √(1 + ∑ i : Fin Anderson4D.dim, ↑(γ i) ^ 2)

theorem Anderson4D.one_le_designJapaneseBracket (γ : Z4) : 1 ≤ designJapaneseBracket γ

noncomputable def Anderson4D.designCriticalHSWeight (γ : Z4) : ℝ

The literal sufficient weight from DESIGN §5.2: ⟨γ⟩⁻⁴ (1 + log ⟨γ⟩).

Equations

• Anderson4D.designCriticalHSWeight γ = (Anderson4D.designJapaneseBracket γ ^ 4)⁻¹ * (1 + Real.log (Anderson4D.designJapaneseBracket γ))

theorem Anderson4D.designCriticalHSWeight_nonneg (γ : Z4) : 0 ≤ designCriticalHSWeight γ

def Anderson4D.CriticalGreenSquaredConvolutionEstimate (C : ℝ) : Prop

The isolated critical lattice estimate needed to turn the exact Green convolution into the logarithmic sufficient condition. It is deliberately separate from the operator conclusion: this is the remaining scalar four-dimensional convolution lemma, not a disguised Hilbert--Schmidt assumption.

Equations

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

def Anderson4D.torusHSInputOutputShear : Z4 × Z4 ≃ Z4 × Z4

Input/output coordinates followed by the conserved-frequency shear: (β, α) ↦ (α + β, α).

Equations

• Anderson4D.torusHSInputOutputShear = (Equiv.prodComm Anderson4D.Z4 Anderson4D.Z4).trans Anderson4D.l2LatticePairShear

theorem Anderson4D.torusFourierHSCertificate_greenL2Op_mul_mul_greenL2Op (M : ↥TorusL2 →L[ℂ] ↥TorusL2) (a : Z4 → ℂ) (C : ℝ) (hprofile : HasMultiplicationFourierProfile M a) (hcritical : CriticalGreenSquaredConvolutionEstimate C) (ha : Summable fun (γ : Z4) => ‖a γ‖ ^ 2 * designCriticalHSWeight γ) : TorusFourierHSCertificate (greenL2Op * M * greenL2Op)

The DESIGN §5.2 logarithmic Fourier condition is sufficient for the Green sandwich to have a square-summable Fourier matrix, once the independent critical scalar convolution estimate is available.

theorem Anderson4D.inverseGreen_sub_greenL2Op_torusFourierHSCertificate (M : ↥TorusL2 →L[ℂ] ↥TorusL2) (a : Z4 → ℂ) (C : ℝ) (h : LopInvertible greenL2Op M) (hprofile : HasMultiplicationFourierProfile M a) (hcritical : CriticalGreenSquaredConvolutionEstimate C) (ha : Summable fun (γ : Z4) => ‖a γ‖ ^ 2 * designCriticalHSWeight γ) : TorusFourierHSCertificate (inverseGreen greenL2Op M h - greenL2Op)

Concrete conditioned resolvent-difference consequence of the logarithmic Fourier sufficient condition.