Bounds for the periodized cutoff covariance

The torus covariance is written in DetParametrix.Kernels as a lattice periodization of the compactly supported Euclidean covariance. This file proves that, for 0 < ε ≤ 1, only a fixed finite box of period vectors can contribute. It then turns the Euclidean uniform bound into the paper-scale O(ε⁻⁴) torus bound without any summability hypothesis.

noncomputable def Anderson4D.SmoothCutoff.covariancePeriodRadius (ρ : SmoothCutoff) : ℤ

A fixed integer half-width containing every period vector which can meet the support of η_ε, uniformly for 0 < ε ≤ 1.

Equations

• ρ.covariancePeriodRadius = ⌈(2 * ρ.radius + Real.pi) / (2 * Real.pi)⌉

noncomputable def Anderson4D.SmoothCutoff.covariancePeriodBox (ρ : SmoothCutoff) : Finset Z4

The corresponding finite box in ℤ⁴.

Equations

• ρ.covariancePeriodBox = Fintype.piFinset fun (x : Fin Anderson4D.dim) => Finset.Icc (-ρ.covariancePeriodRadius) ρ.covariancePeriodRadius

noncomputable def Anderson4D.SmoothCutoff.etaPeriodTerm (ρ : SmoothCutoff) (ε : ℝ) (z : T4) (k : Z4) : ℝ

One summand in the lattice periodization defining etaEpsT4.

Equations

• ρ.etaPeriodTerm ε z k = ε⁻¹ ^ Anderson4D.dim * ρ.eta fun (i : Fin Anderson4D.dim) => ε⁻¹ * (Anderson4D.torusLift z i + 2 * Real.pi * ↑(k i))

theorem Anderson4D.SmoothCutoff.etaEpsT4_eq_tsum_etaPeriodTerm (ρ : SmoothCutoff) (ε : ℝ) (z : T4) : ρ.etaEpsT4 ε z = ∑' (k : Z4), ρ.etaPeriodTerm ε z k

theorem Anderson4D.SmoothCutoff.norm_periodizeR4_le (x : R4) : ‖periodizeR4 x‖ ≤ ‖x‖

Passing from a Euclidean representative to the product quotient does not increase the fixed sup norm.

theorem Anderson4D.SmoothCutoff.norm_le_periodicDisplacement (z : T4) (k : Z4) : ‖z‖ ≤ ‖periodicDisplacement z k‖

Every period representative of a torus point dominates its quotient norm.

theorem Anderson4D.SmoothCutoff.etaPeriodTerm_ne_zero_mem_covariancePeriodBox (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (z : T4) {k : Z4} (hk : ρ.etaPeriodTerm ε z k ≠ 0) : k ∈ ρ.covariancePeriodBox

A nonzero periodization term belongs to the fixed period box.

theorem Anderson4D.SmoothCutoff.etaEpsT4_eq_sum_covariancePeriodBox (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (z : T4) : ρ.etaEpsT4 ε z = ∑ k ∈ ρ.covariancePeriodBox, ρ.etaPeriodTerm ε z k

The lattice periodization is an actual finite sum on the fixed box.

theorem Anderson4D.SmoothCutoff.etaPeriodTerm_nonneg (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : T4) (k : Z4) : 0 ≤ ρ.etaPeriodTerm ε z k

Every periodization term is nonnegative at positive scale.

theorem Anderson4D.SmoothCutoff.etaEpsT4_nonneg (ρ : SmoothCutoff) (ε : ℝ) (z : T4) : 0 ≤ ρ.etaEpsT4 ε z

Positivity of the torus covariance. The fourth rescaling power is nonnegative even outside the theorem's positive-scale regime.

theorem Anderson4D.SmoothCutoff.norm_lt_two_radius_mul_of_etaEpsT4_ne_zero (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) {z : T4} (hz : ρ.etaEpsT4 ε z ≠ 0) : ‖z‖ < 2 * ρ.radius * ε

Nonvanishing of the periodized covariance forces the torus displacement into an explicit O(ε) neighbourhood of zero.

theorem Anderson4D.SmoothCutoff.torusDistSq_le_support_of_etaEpsT4_ne_zero (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) {z : T4} (hz : ρ.etaEpsT4 ε z ≠ 0) : torusDistSq z ≤ (4 * ρ.radius * ε) ^ 2

Squared support indicator in exactly the form used by Proposition 4.1. The factor 4 combines the product quotient norm and torusDistSq ≤ 4‖z‖².

theorem Anderson4D.SmoothCutoff.etaEpsT4_le_card_mul_of_eta_bound (ρ : SmoothCutoff) {ε C : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hC : ∀ (x : R4), ρ.eta x ≤ C) (z : T4) : ρ.etaEpsT4 ε z ≤ ↑ρ.covariancePeriodBox.card * (ε⁻¹ ^ dim * C)

A Euclidean bound η ≤ C yields the paper-scale torus bound, with the finite period-box cardinality kept explicit.

theorem Anderson4D.SmoothCutoff.exists_pos_etaEpsT4_uniform_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (z : T4), ρ.etaEpsT4 ε z ≤ ε⁻¹ ^ dim * C

Named positive constants give a uniform O(ε⁻⁴) bound for the torus covariance.