bridge analyticity to Fourier derivative bounds

This module connects the ordered directional derivative bounds to the coordinate derivative bounds used by the existing Parseval tail estimate.

def AVenhance.Infra.Section5.RelativeError.AnalyticTail.realCoordIter (i : Fin 2) : ℕ → (Homogenization.Vec 2 → ℝ) → Homogenization.Vec 2 → ℝ

Iterate real differentiation in a fixed spatial coordinate.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section5.RelativeError.AnalyticTail.realCoordIter i 0 x✝ = x✝

theorem AVenhance.Infra.Section5.RelativeError.AnalyticTail.realCoordIter_contDiff_top (i : Fin 2) (n : ℕ) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (realCoordIter i n f)

theorem AVenhance.Infra.Section5.RelativeError.AnalyticTail.realCoordIter_eq_iteratedFDeriv (i : Fin 2) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : Homogenization.Vec 2) : realCoordIter i n f x = (iteratedFDeriv ℝ n f x) fun (x : Fin n) => Homogenization.basisVec i

theorem AVenhance.Infra.Section5.RelativeError.AnalyticTail.coordDerivIter_realToComplex (i : Fin 2) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : Ergodic.coordDerivIter i n (Torus.realToComplex f) = fun (x : Homogenization.Vec 2) => ↑(realCoordIter i n f x)