Finite-window derivatives of the covariance periodization

Finite lattice windows may be differentiated without any summability argument. This file proves the exact formula and its termwise auxiliary majorant, then gives local-finiteness interfaces which transfer those facts to etaPeriodizationR4. The geometric construction of a suitable window is intentionally left to the support-localization layer.

noncomputable def Anderson4D.SmoothCutoff.etaPeriodizationCoordLineWindow (ρ : SmoothCutoff) (Q : Finset Z4) (ε : ℝ) (x : R4) (i : Fin dim) (t : ℝ) : ℝ

A finite lattice window of the coordinate-line periodization.

Equations

• ρ.etaPeriodizationCoordLineWindow Q ε x i t = ∑ k ∈ Q, ρ.etaPeriodTermCoordLine ε x k i t

theorem Anderson4D.SmoothCutoff.etaPeriodizationCoordLineWindow_eq (ρ : SmoothCutoff) (Q : Finset Z4) (ε : ℝ) (x : R4) (i : Fin dim) (t : ℝ) : ρ.etaPeriodizationCoordLineWindow Q ε x i t = ∑ k ∈ Q, ρ.etaPeriodTermR4 ε (Function.update x i t) k

The coordinate-line window is the corresponding finite sum of the existing arbitrary-representative periodization terms.

theorem Anderson4D.SmoothCutoff.contDiff_etaPeriodizationCoordLineWindow_eight (ρ : SmoothCutoff) (Q : Finset Z4) (ε : ℝ) (x : R4) (i : Fin dim) : ContDiff ℝ 8 (ρ.etaPeriodizationCoordLineWindow Q ε x i)

Every finite coordinate-line window is C⁸.

theorem Anderson4D.SmoothCutoff.iteratedDeriv_etaPeriodizationCoordLineWindow_eq_sum (ρ : SmoothCutoff) (Q : Finset Z4) (ε : ℝ) (x : R4) (i : Fin dim) (t : ℝ) {r : ℕ} (hr : r ≤ 8) : iteratedDeriv r (ρ.etaPeriodizationCoordLineWindow Q ε x i) t = ∑ k ∈ Q, iteratedDeriv r (ρ.etaPeriodTermCoordLine ε x k i) t

Iterated differentiation commutes with a finite lattice window.

theorem Anderson4D.SmoothCutoff.iteratedDeriv_etaPeriodizationCoordLineWindow (ρ : SmoothCutoff) (Q : Finset Z4) {ε : ℝ} (hε : 0 < ε) (x : R4) (i : Fin dim) (t : ℝ) {r : ℕ} (hr : r ≤ 8) : iteratedDeriv r (ρ.etaPeriodizationCoordLineWindow Q ε x i) t = ∑ k ∈ Q, ε⁻¹ ^ dim * ε⁻¹ ^ r * ρ.etaCoordDerivative r i fun (j : Fin dim) => ε⁻¹ * (Function.update x i t j + covariancePeriodVector k j)

Exact finite-sum formula for the repeated coordinate derivative.

theorem Anderson4D.SmoothCutoff.abs_iteratedDeriv_etaPeriodizationCoordLineWindow_le (ρ : SmoothCutoff) (Q : Finset Z4) {ε : ℝ} (hε : 0 < ε) (x : R4) (i : Fin dim) (t : ℝ) {r : ℕ} (hr : r ≤ 8) : |iteratedDeriv r (ρ.etaPeriodizationCoordLineWindow Q ε x i) t| ≤ ρ.etaDerivativeMajorantConstant * ε⁻¹ ^ r * ∑ k ∈ Q, ρ.auxiliaryCutoff.etaPeriodTermR4 ε (Function.update x i t) k

The finite-window derivative is bounded by the matching auxiliary finite sum, with no lattice-cardinality factor.

theorem Anderson4D.SmoothCutoff.etaPeriodizationR4_eq_sum_of_outside_eq_zero (ρ : SmoothCutoff) (Q : Finset Z4) (ε : ℝ) (y : R4) (hout : ∀ k ∉ Q, ρ.etaPeriodTermR4 ε y k = 0) : ρ.etaPeriodizationR4 ε y = ∑ k ∈ Q, ρ.etaPeriodTermR4 ε y k

An arbitrary-representative periodization equals a finite window once all terms outside that window vanish.

theorem Anderson4D.SmoothCutoff.eventuallyEq_etaPeriodizationCoordLineWindow (ρ : SmoothCutoff) (Q : Finset Z4) (ε : ℝ) (x : R4) (i : Fin dim) (t : ℝ) (hout : ∀ᶠ (s : ℝ) in nhds t, ∀ k ∉ Q, ρ.etaPeriodTermCoordLine ε x k i s = 0) : (fun (s : ℝ) => ρ.etaPeriodizationR4 ε (Function.update x i s)) =ᶠ[nhds t] ρ.etaPeriodizationCoordLineWindow Q ε x i

A neighborhood-wise vanishing condition gives the local finite representation needed for differentiation.

theorem Anderson4D.SmoothCutoff.contDiff_etaPeriodizationR4_coordLine_eight_of_local_windows (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (i : Fin dim) (hlocal : ∀ (t : ℝ), ∃ (Q : Finset Z4), ∀ᶠ (s : ℝ) in nhds t, ∀ k ∉ Q, ρ.etaPeriodTermCoordLine ε x k i s = 0) : ContDiff ℝ 8 fun (t : ℝ) => ρ.etaPeriodizationR4 ε (Function.update x i t)

Local finite representations at every point imply global C⁸ regularity of the arbitrary-representative coordinate line.

theorem Anderson4D.SmoothCutoff.iteratedDeriv_etaPeriodizationR4_coordLine_eq_sum (ρ : SmoothCutoff) (Q : Finset Z4) (ε : ℝ) (x : R4) (i : Fin dim) (t : ℝ) {r : ℕ} (hr : r ≤ 8) (hout : ∀ᶠ (s : ℝ) in nhds t, ∀ k ∉ Q, ρ.etaPeriodTermCoordLine ε x k i s = 0) : iteratedDeriv r (fun (s : ℝ) => ρ.etaPeriodizationR4 ε (Function.update x i s)) t = ∑ k ∈ Q, iteratedDeriv r (ρ.etaPeriodTermCoordLine ε x k i) t

Exact derivative of the true periodization under a local finite-window condition.

theorem Anderson4D.SmoothCutoff.abs_iteratedDeriv_etaPeriodizationR4_coordLine_le (ρ : SmoothCutoff) (Q : Finset Z4) {ε : ℝ} (hε : 0 < ε) (x : R4) (i : Fin dim) (t : ℝ) {r : ℕ} (hr : r ≤ 8) (hout : ∀ᶠ (s : ℝ) in nhds t, ∀ k ∉ Q, ρ.etaPeriodTermCoordLine ε x k i s = 0) (houtAux : ∀ k ∉ Q, ρ.auxiliaryCutoff.etaPeriodTermR4 ε (Function.update x i t) k = 0) : |iteratedDeriv r (fun (s : ℝ) => ρ.etaPeriodizationR4 ε (Function.update x i s)) t| ≤ ρ.etaDerivativeMajorantConstant * ε⁻¹ ^ r * ρ.auxiliaryCutoff.etaPeriodizationR4 ε (Function.update x i t)

The true periodization inherits the auxiliary majorant whenever the same window is locally valid for the original terms and pointwise valid for the auxiliary terms.