Coordinate derivatives of one covariance-periodization term

This file differentiates one lattice summand along one scalar coordinate line. It deliberately stops before summing over the period lattice, so the derivative majorant is termwise and carries no finite-box cardinality.

def Anderson4D.SmoothCutoff.etaCoordLineMap (c : ℝ) (i : Fin dim) : ℝ →L[ℝ] R4

The continuous linear coordinate line t ↦ (c t) eᵢ.

Equations

• Anderson4D.SmoothCutoff.etaCoordLineMap c i = (c • 1).smulRight (Anderson4D.SmoothCutoff.etaCoordDirection i)

@[simp]

theorem Anderson4D.SmoothCutoff.etaCoordLineMap_apply (c t : ℝ) (i : Fin dim) : (etaCoordLineMap c i) t = (c * t) • etaCoordDirection i

noncomputable def Anderson4D.SmoothCutoff.etaPeriodCoordBase (ε : ℝ) (x : R4) (k : Z4) (i : Fin dim) : R4

The part of a scaled periodization argument independent of the distinguished coordinate value.

Equations

• Anderson4D.SmoothCutoff.etaPeriodCoordBase ε x k i j = ε⁻¹ * (Function.update x i 0 j + Anderson4D.SmoothCutoff.covariancePeriodVector k j)

noncomputable def Anderson4D.SmoothCutoff.etaPeriodCoordArgument (ε : ℝ) (x : R4) (k : Z4) (i : Fin dim) (t : ℝ) : R4

The scaled Euclidean argument of a periodization term, written as an affine scalar coordinate line.

Equations

• Anderson4D.SmoothCutoff.etaPeriodCoordArgument ε x k i t = Anderson4D.SmoothCutoff.etaPeriodCoordBase ε x k i + (Anderson4D.SmoothCutoff.etaCoordLineMap ε⁻¹ i) t

theorem Anderson4D.SmoothCutoff.etaPeriodCoordArgument_eq (ε : ℝ) (x : R4) (k : Z4) (i : Fin dim) (t : ℝ) : etaPeriodCoordArgument ε x k i t = fun (j : Fin dim) => ε⁻¹ * (Function.update x i t j + covariancePeriodVector k j)

noncomputable def Anderson4D.SmoothCutoff.etaPeriodTermCoordLine (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (k : Z4) (i : Fin dim) (t : ℝ) : ℝ

One periodization summand restricted to a scalar coordinate line.

Equations

• ρ.etaPeriodTermCoordLine ε x k i t = ε⁻¹ ^ Anderson4D.dim * ρ.eta (Anderson4D.SmoothCutoff.etaPeriodCoordArgument ε x k i t)

theorem Anderson4D.SmoothCutoff.etaPeriodTermCoordLine_eq (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (k : Z4) (i : Fin dim) (t : ℝ) : ρ.etaPeriodTermCoordLine ε x k i t = ρ.etaPeriodTermR4 ε (Function.update x i t) k

The affine-line definition is exactly the existing periodization term at the representative whose i-th coordinate is t.

theorem Anderson4D.SmoothCutoff.contDiff_etaPeriodTermCoordLine_eight (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (k : Z4) (i : Fin dim) : ContDiff ℝ 8 (ρ.etaPeriodTermCoordLine ε x k i)

A scalar coordinate line in one periodization term is C⁸.

theorem Anderson4D.SmoothCutoff.iteratedDeriv_etaPeriodTermCoordLine (ρ : SmoothCutoff) {ε : ℝ} (_hε : 0 < ε) (r : ℕ) (x : R4) (k : Z4) (i : Fin dim) (t : ℝ) : iteratedDeriv r (ρ.etaPeriodTermCoordLine ε x k i) t = ε⁻¹ ^ dim * ε⁻¹ ^ r * ρ.etaCoordDerivative r i fun (j : Fin dim) => ε⁻¹ * (Function.update x i t j + covariancePeriodVector k j)

Exact repeated coordinate derivative of a single periodization term.

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

The derivative of one summand is bounded by the corresponding auxiliary-cutoff summand, with exactly the expected ε⁻ʳ loss.