Fourier coefficients of the Fredholm resolvent

The coefficient called modeHcoeff in the original coefficient layer is the totalized Neumann tail. It agrees with the inverse resolvent only in a regime where that Neumann expansion is known to converge. In particular, Fredholm invertibility of 1 - K alone does not imply such convergence.

This file gives the operator-route coefficient which is valid on the one-sided Fredholm good event. The normalization is chosen so that it agrees with modeHcoeff whenever the existing norm-small Neumann bridge does apply:

Ĥ(α,β) = |T⁴| / λ_ε · ⟪e_{-α}, (G_ε-G)e_β⟫.

No smallness assumption on ‖K‖ occurs in the Fredholm statements below.

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

The true resolvent Fourier coefficient, totalized to zero off the invertibility locus. This is the operator-route replacement for using an unconditionally totalized Neumann series as the definition of the full resolvent.

Equations

• Anderson4D.fredholmModeHcoeff M ρ lam ε α β ω = ↑Anderson4D.paperTorusVolume * (↑(Anderson4D.lamEps lam ε))⁻¹ * Anderson4D.torusOperatorModeCoeffH M ρ lam ε α β ω

theorem Anderson4D.measurable_ringInverse_torusL2Operator : Measurable Ring.inverse

The totalized ring inverse is Borel measurable on the Banach algebra of torus operators. It is continuous on the open unit locus and is identically zero on its closed complement.

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

A manifestly measurable version of the recentered Fredholm resolvent. It uses the preferred measurable realization of the random potential and is zero off the open invertibility locus.

Equations

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

theorem Anderson4D.measurable_measurableFredholmRecenteredInverse (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) : Measurable (measurableFredholmRecenteredInverse M ρ lam ε)

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

The measurable full Fredholm coefficient.

Equations

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

theorem Anderson4D.measurable_measurableFredholmModeHcoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) : Measurable (measurableFredholmModeHcoeff M ρ lam ε α β)

theorem Anderson4D.ae_measurableFredholmModeHcoeff_eq_fredholmModeHcoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (α β : Z4) : measurableFredholmModeHcoeff M ρ lam ε α β =ᵐ[MeasureTheory.volume] fredholmModeHcoeff M ρ lam ε α β

The measurable realization agrees almost surely with the samplewise Fredholm coefficient at every positive mollification scale.

theorem Anderson4D.aemeasurable_fredholmModeHcoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (α β : Z4) : AEMeasurable (fredholmModeHcoeff M ρ lam ε α β) MeasureTheory.volume

noncomputable def Anderson4D.fredholmFiniteModeReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) : ℝ

A finite real Fourier test of the true samplewise Fredholm resolvent.

Equations

• Anderson4D.fredholmFiniteModeReal M ρ lam ε s modes c ω = (∑ j : Fin s, c j * Anderson4D.fredholmModeHcoeff M ρ lam ε (modes j).1 (modes j).2 ω).re

noncomputable def Anderson4D.measurableFredholmFiniteModeReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) : ℝ

The manifestly measurable version of the same finite Fourier test.

Equations

• Anderson4D.measurableFredholmFiniteModeReal M ρ lam ε s modes c ω = (∑ j : Fin s, c j * Anderson4D.measurableFredholmModeHcoeff M ρ lam ε (modes j).1 (modes j).2 ω).re

theorem Anderson4D.measurable_measurableFredholmFiniteModeReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Measurable (measurableFredholmFiniteModeReal M ρ lam ε s modes c)

theorem Anderson4D.ae_measurableFredholmFiniteModeReal_eq_fredholmFiniteModeReal (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : measurableFredholmFiniteModeReal M ρ lam ε s modes c =ᵐ[MeasureTheory.volume] fredholmFiniteModeReal M ρ lam ε s modes c

theorem Anderson4D.norm_torusFourierMatrixCoeff_le (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (α β : Z4) : ‖torusFourierMatrixCoeff A α β‖ ≤ ‖A‖

A signed Fourier matrix coefficient is bounded by the operator norm. Both Fourier basis vectors have norm one.

theorem Anderson4D.fredholmModeHcoeff_eq_inverseGreen (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) (hinv : LopInvertible greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω)) : fredholmModeHcoeff M ρ lam ε α β ω = ↑paperTorusVolume * (↑(lamEps lam ε))⁻¹ * torusFourierMatrixCoeff (inverseGreen greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω) hinv - greenL2Op) α β

On any invertible sample, fredholmModeHcoeff is literally the normalized matrix coefficient of the selected two-sided inverse. The statement is proof-independent because LopInvertible is a proposition.

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

In the norm-small regime, where the Neumann tail is genuinely summable, the Fredholm/operator route agrees with the original coefficient route. This is a compatibility theorem, not a hypothesis used by the one-sided Fredholm bridge.

theorem Anderson4D.norm_parametrixCoeff_sub_fredholmModeHcoeff_le (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (ω : M.Ω) (P : ↥TorusL2 →L[ℂ] ↥TorusL2) (hinv : LopInvertible greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω)) : ‖↑paperTorusVolume * (↑(lamEps lam ε))⁻¹ * torusFourierMatrixCoeff (P - greenL2Op) α β - fredholmModeHcoeff M ρ lam ε α β ω‖ ≤ ‖↑paperTorusVolume * (↑(lamEps lam ε))⁻¹‖ * ‖P - inverseGreen greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω) hinv‖

Operator-norm proximity to a physical parametrix gives the correctly normalized fixed-mode proximity to the true Fredholm resolvent.

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

The normalized positive-order coefficient of the finite physical parametrix. This is the single-mode summand used by the moving truncation, kept here in a parametrix-layer form.

Equations

• Anderson4D.truncatedParametrixModeHcoeff M ρ lam ε A α β ω = (↑(Anderson4D.lamEps lam ε))⁻¹ * ∑ n : Fin A, Anderson4D.pmCoeff M ρ lam ε (↑n + 1) α β ω

noncomputable def Anderson4D.truncatedParametrixFiniteModeReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) : ℝ

The finite real Fourier test of the physical parametrix.

Equations

• Anderson4D.truncatedParametrixFiniteModeReal M ρ lam ε A s modes c ω = (∑ j : Fin s, c j * Anderson4D.truncatedParametrixModeHcoeff M ρ lam ε A (modes j).1 (modes j).2 ω).re

theorem Anderson4D.canonicalPhysicalTruncatedParametrixL2Operator_sub_green (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (ω : M.Ω) : canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω - greenL2Op = canonicalPositiveTruncatedParametrixL2Operator M ρ lam ε A ω

The finite physical parametrix is G plus its canonical positive-order operator.

theorem Anderson4D.scaled_canonicalPhysicalCoeff_eq_truncatedParametrixModeHcoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (α β : Z4) (ω : M.Ω) (hcoeff : torusFourierMatrixCoeff (canonicalPositiveTruncatedParametrixL2Operator M ρ lam ε A ω) α β = (↑paperTorusVolume)⁻¹ * ∑ n ∈ Finset.range A, pmCoeff M ρ lam ε (n + 1) α β ω) : ↑paperTorusVolume * (↑(lamEps lam ε))⁻¹ * torusFourierMatrixCoeff (canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω - greenL2Op) α β = truncatedParametrixModeHcoeff M ρ lam ε A α β ω

Exact normalization ledger between the positive physical operator and the finite coefficient truncation.

theorem Anderson4D.norm_truncatedParametrixModeHcoeff_sub_fredholmModeHcoeff_le_on_good (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (Qfactor Rleft : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (α β : Z4) (ω : M.Ω) (hεpos : 0 < ε) (hεsmall : 2 * ε ^ 2 ≤ 1) (hεpow : ε ^ 28 < 1 / 2) (hω : ω ∈ PartialPairing.canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε A Qfactor Rleft) (hcoeff : torusFourierMatrixCoeff (canonicalPositiveTruncatedParametrixL2Operator M ρ lam ε A ω) α β = (↑paperTorusVolume)⁻¹ * ∑ n ∈ Finset.range A, pmCoeff M ρ lam ε (n + 1) α β ω) : ‖truncatedParametrixModeHcoeff M ρ lam ε A α β ω - fredholmModeHcoeff M ρ lam ε α β ω‖ ≤ ‖↑paperTorusVolume * (↑(lamEps lam ε))⁻¹‖ * ε ^ 12

Fredholm fixed-mode replacement. On the paper's one-sided good event, the normalized finite parametrix coefficient is close to the true inverse-resolvent coefficient. The proof uses only the Fredholm inverse constructed from the small residual; there is no assumption on ‖K‖.

The coefficient-realization premise is the already-proved almost-sure output of canonicalPositiveTruncatedParametrixL2Operator_coeff; callers may intersect that full-measure set with the quantitative good event.

theorem Anderson4D.norm_truncatedParametrixFiniteModeReal_sub_fredholmFiniteModeReal_le_on_good (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (Qfactor Rleft : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) (hεpos : 0 < ε) (hεsmall : 2 * ε ^ 2 ≤ 1) (hεpow : ε ^ 28 < 1 / 2) (hω : ω ∈ PartialPairing.canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε A Qfactor Rleft) (hcoeff : ∀ (j : Fin s), torusFourierMatrixCoeff (canonicalPositiveTruncatedParametrixL2Operator M ρ lam ε A ω) (modes j).1 (modes j).2 = (↑paperTorusVolume)⁻¹ * ∑ n ∈ Finset.range A, pmCoeff M ρ lam ε (n + 1) (modes j).1 (modes j).2 ω) : ‖truncatedParametrixFiniteModeReal M ρ lam ε A s modes c ω - fredholmFiniteModeReal M ρ lam ε s modes c ω‖ ≤ ∑ j : Fin s, ‖c j‖ * (‖↑paperTorusVolume * (↑(lamEps lam ε))⁻¹‖ * ε ^ 12)

Finite-family form of the Fredholm replacement estimate.