Vanishing of the Fredholm fixed-mode error

The one-sided operator comparison gives the normalized fixed-mode error

|T⁴| · |λ_ε⁻¹| · ε¹².

Since λ_ε = λ / sqrt |log ε|, this is a constant multiple of sqrt |log ε| · ε¹² and therefore vanishes as ε ↓ 0.

noncomputable def Anderson4D.fredholmModeErrorScale (lam ε : ℝ) : ℝ

The scalar error in the Fredholm coefficient bridge.

Equations

• Anderson4D.fredholmModeErrorScale lam ε = ‖↑Anderson4D.paperTorusVolume * (↑(Anderson4D.lamEps lam ε))⁻¹‖ * ε ^ 12

theorem Anderson4D.fredholmModeErrorScale_nonneg (lam ε : ℝ) : 0 ≤ fredholmModeErrorScale lam ε

theorem Anderson4D.tendsto_abs_log_mul_pow_twelve_nhdsGT_zero : Filter.Tendsto (fun (ε : ℝ) => |Real.log ε| * ε ^ 12) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

A polynomial beats one absolute logarithm at the positive side of zero.

theorem Anderson4D.tendsto_sqrt_abs_log_mul_pow_twelve_nhdsGT_zero : Filter.Tendsto (fun (ε : ℝ) => √|Real.log ε| * ε ^ 12) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The square-root logarithmic loss is also absorbed by ε¹².

theorem Anderson4D.tendsto_fredholmModeErrorScale_nhdsGT_zero {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fredholmModeErrorScale lam) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

For every positive coupling, the exact normalized Fredholm fixed-mode error tends to zero.

theorem Anderson4D.sum_norm_mul_fredholmModeErrorScale_nonneg {s : ℕ} (c : Fin s → ℂ) (lam ε : ℝ) : 0 ≤ ∑ j : Fin s, ‖c j‖ * fredholmModeErrorScale lam ε

The finite-family error used by the Cramér--Wold test is nonnegative.

theorem Anderson4D.tendsto_sum_norm_mul_fredholmModeErrorScale_nhdsGT_zero {s : ℕ} (c : Fin s → ℂ) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (fun (ε : ℝ) => ∑ j : Fin s, ‖c j‖ * fredholmModeErrorScale lam ε) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

A fixed finite coefficient family preserves the vanishing Fredholm error.