Global derivative bounds for the covariance periodization

Compact support gives a common finite lattice window near every point. Combining that geometry with the finite-window derivative formulas removes the local-window hypotheses from the coordinate C⁸ and derivative majorant statements.

noncomputable def Anderson4D.SmoothCutoff.etaPeriodLocalRadiusR4 (ρ : SmoothCutoff) (ε : ℝ) (x₀ : R4) : ℤ

A lattice radius large enough to contain every nonzero periodization term in the unit neighborhood of x₀.

Equations

• ρ.etaPeriodLocalRadiusR4 ε x₀ = ⌈(2 * ρ.radius * ε + ‖x₀‖ + 1) / (2 * Real.pi)⌉

noncomputable def Anderson4D.SmoothCutoff.etaPeriodLocalBoxR4 (ρ : SmoothCutoff) (ε : ℝ) (x₀ : R4) : Finset Z4

The corresponding finite lattice window.

Equations

• ρ.etaPeriodLocalBoxR4 ε x₀ = Fintype.piFinset fun (x : Fin Anderson4D.dim) => Finset.Icc (-ρ.etaPeriodLocalRadiusR4 ε x₀) (ρ.etaPeriodLocalRadiusR4 ε x₀)

theorem Anderson4D.SmoothCutoff.mem_etaPeriodLocalBoxR4_of_ne_zero (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x₀ x : R4) (hx : dist x x₀ < 1) {k : Z4} (hk : ρ.etaPeriodTermR4 ε x k ≠ 0) : k ∈ ρ.etaPeriodLocalBoxR4 ε x₀

Every nonzero periodization term in the unit neighborhood belongs to the explicit local box.

noncomputable def Anderson4D.SmoothCutoff.etaPeriodJointLocalBoxR4 (ρ : SmoothCutoff) (ε : ℝ) (x₀ : R4) : Finset Z4

A common window for the original cutoff and the auxiliary cutoff used in the derivative majorant.

Equations

• ρ.etaPeriodJointLocalBoxR4 ε x₀ = ρ.etaPeriodLocalBoxR4 ε x₀ ∪ ρ.auxiliaryCutoff.etaPeriodLocalBoxR4 ε x₀

theorem Anderson4D.SmoothCutoff.exists_etaPeriodizationR4_coordLine_jointLocalWindow (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : R4) (i : Fin dim) (t : ℝ) : ∃ (Q : Finset Z4), (∀ᶠ (s : ℝ) in nhds t, ∀ k ∉ Q, ρ.etaPeriodTermCoordLine ε x k i s = 0) ∧ ∀ k ∉ Q, ρ.auxiliaryCutoff.etaPeriodTermR4 ε (Function.update x i t) k = 0

Compact support supplies exactly the two window conditions required by abs_iteratedDeriv_etaPeriodizationR4_coordLine_le.

theorem Anderson4D.SmoothCutoff.contDiff_etaPeriodizationR4_coordLine_eight (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : R4) (i : Fin dim) : ContDiff ℝ 8 fun (t : ℝ) => ρ.etaPeriodizationR4 ε (Function.update x i t)

Every coordinate line of the true periodization is C⁸, with the finite lattice window constructed from compact support.

theorem Anderson4D.SmoothCutoff.abs_iteratedDeriv_etaPeriodizationR4_coordLine_le_global (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : R4) (i : Fin dim) (t : ℝ) {r : ℕ} (hr : r ≤ 8) : |iteratedDeriv r (fun (s : ℝ) => ρ.etaPeriodizationR4 ε (Function.update x i s)) t| ≤ ρ.etaDerivativeMajorantConstant * ε⁻¹ ^ r * ρ.auxiliaryCutoff.etaPeriodizationR4 ε (Function.update x i t)

Global coordinate-derivative majorant for the true periodization. There is no lattice-cardinality loss.