analytic tails after arbitrary ordered derivatives

The analyticity bounds control every ordered coordinate derivative. This module keeps the order explicit and applies the existing Fourier tail estimate to the derivative before taking its spectral complement.

def AVenhance.Infra.Section5.RelativeError.orderedRealDerivative : List (Fin 2) → (Homogenization.Vec 2 → ℝ) → Homogenization.Vec 2 → ℝ

Iterate real spatial directional derivatives in the order prescribed by a word.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section5.RelativeError.orderedRealDerivative [] x✝ = x✝

def AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.complexDirectionIter : List (Fin 2) → (Homogenization.Vec 2 → ℂ) → Homogenization.Vec 2 → ℂ

Iterate complex coordinate derivatives in the order prescribed by a word.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.complexDirectionIter [] x✝ = x✝

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.orderedRealDerivative_contDiff_top (is : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (orderedRealDerivative is f)

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.complexDirectionIter_contDiff_top (is : List (Fin 2)) {f : Homogenization.Vec 2 → ℂ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (complexDirectionIter is f)

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.orderedRealDerivative_periodic (is : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : IsZ2Periodic f) : IsZ2Periodic (orderedRealDerivative is f)

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.complexDirectionIter_periodic (is : List (Fin 2)) {f : Homogenization.Vec 2 → ℂ} (hf : Torus.IsZdPeriodic f) : Torus.IsZdPeriodic (complexDirectionIter is f)

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.coordDeriv_realCast {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin 2) (x : Homogenization.Vec 2) : Torus.coordDeriv i (fun (y : Homogenization.Vec 2) => ↑(f y)) x = ↑((fderiv ℝ f x) (Homogenization.basisVec i))

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.complexDirectionIter_realCast (is : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : (complexDirectionIter is fun (x : Homogenization.Vec 2) => ↑(f x)) = fun (x : Homogenization.Vec 2) => ↑(orderedRealDerivative is f x)

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.orderedRealDerivative_eq_iteratedFDeriv (is : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) : orderedRealDerivative is f x = (iteratedFDeriv ℝ is.length f x) fun (j : Fin is.length) => Homogenization.basisVec (is.get j)

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.coordDerivIter_append (is : List (Fin 2)) (i : Fin 2) (m : ℕ) {f : Homogenization.Vec 2 → ℂ} : Ergodic.coordDerivIter i m (complexDirectionIter is f) = complexDirectionIter (List.replicate m i ++ is) f

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.factorial_add_le_pow_mul (m n : ℕ) : (m + n).factorial ≤ 2 ^ (m + n) * n.factorial * m.factorial

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.analytic_factorial_shift {m n : ℕ} {R N : ℝ} (hR : 0 < R) (hN : 0 ≤ N) : N * ↑(m + n).factorial / R ^ (m + n) ≤ 2 ^ n * ↑n.factorial * N / R ^ n * (↑m.factorial / (R / 2) ^ m)

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.torusCharacter_line_eq_local {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (z : Homogenization.Vec n) (t : ℝ) : Torus.torusCharacter k (i.insertNth t z) = (fourier (-k i)) ↑t * ∏ j : Fin n, (fourier (-k (i.succAbove j))) ↑(z j)

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.torusCharacter_line_hasDerivAt_local {n : ℕ} (i : Fin (n + 1)) (k : Fin (n + 1) → ℤ) (z : Homogenization.Vec n) (t : ℝ) : HasDerivAt (fun (s : ℝ) => Torus.torusCharacter k (i.insertNth s z)) (-2 * ↑Real.pi * Complex.I * ↑(k i) * Torus.torusCharacter k (i.insertNth t z)) t

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.coordDeriv_torusCharacter_local (i : Fin 2) (k : Fin 2 → ℤ) (x : Homogenization.Vec 2) : Torus.coordDeriv i (Torus.torusCharacter k) x = -2 * ↑Real.pi * Complex.I * ↑(k i) * Torus.torusCharacter k x

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.lowProjection_coordinateDerivative {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) (M : ℕ) (i : Fin 2) : (fun (x : Homogenization.Vec 2) => (fderiv ℝ (Ergodic.lowProjection f M) x) (Homogenization.basisVec i)) = Ergodic.lowProjection (fun (x : Homogenization.Vec 2) => (fderiv ℝ f x) (Homogenization.basisVec i)) M

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.orderedRealDerivative_lowProjection (is : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) (M : ℕ) : orderedRealDerivative is (Ergodic.lowProjection f M) = Ergodic.lowProjection (orderedRealDerivative is f) M

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.orderedRealDerivative_sub (is : List (Fin 2)) {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : (orderedRealDerivative is fun (x : Homogenization.Vec 2) => f x - g x) = fun (x : Homogenization.Vec 2) => orderedRealDerivative is f x - orderedRealDerivative is g x

theorem AVenhance.Infra.Section5.RelativeError.AnalyticDerivativeTail.orderedRealDerivative_highRemainder_eq (is : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZ2Periodic f) (M : ℕ) : orderedRealDerivative is (Ergodic.highRemainder f M) = Ergodic.highRemainder (orderedRealDerivative is f) M

theorem AVenhance.Infra.Section5.RelativeError.thetaAnalytic_orderedDerivative_hasCoordinateAnalyticL2Bounds {g : Homogenization.Vec 2 → ℝ} {R : ℝ} (hg : ContDiff ℝ (↑⊤) g) (hper : IsZ2Periodic g) (hθ : IsThetaAnalytic R g) (hR : 0 < R) (is : List (Fin 2)) (his : 0 < is.length) : Ergodic.HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec 2) => ↑(orderedRealDerivative is g x)) (2 ^ is.length * ↑is.length.factorial * √(l2NormSq g) / R ^ is.length) (R / 2)

The ordered derivative bounds imply the coordinate analytic Fourier bounds for every fixed ordered derivative, with half the analytic radius. The loss is explicit: order n costs 2^n n! R^{-n}.

theorem AVenhance.Infra.Section5.RelativeError.thetaAnalytic_orderedDerivative_highRemainderL2_le {g : Homogenization.Vec 2 → ℝ} {R : ℝ} (hg : ContDiff ℝ (↑⊤) g) (hper : IsZ2Periodic g) (hθ : IsThetaAnalytic R g) (hR : 0 < R) (is : List (Fin 2)) (his : 0 < is.length) (M : ℕ) (hscale : 1 ≤ R / 2 * (↑M + 1)) : (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Ergodic.highRemainder (orderedRealDerivative is g) M x ^ 2) ^ (1 / 2) ≤ 3072 * (2 ^ is.length * ↑is.length.factorial * √(l2NormSq g) / R ^ is.length) * Real.exp (-(R / 2) * (↑M + 1) / 512)

analyticity gives an exponential high-frequency tail after any ordered derivative of positive order. The Euclidean cube cutoff is the same cutoff used by Ergodic.highRemainder.

theorem AVenhance.Infra.Section5.RelativeError.thetaAnalytic_derivative_highFrequencyRemainderL2_le {g : Homogenization.Vec 2 → ℝ} {R : ℝ} (hg : ContDiff ℝ (↑⊤) g) (hper : IsZ2Periodic g) (hθ : IsThetaAnalytic R g) (hR : 0 < R) (is : List (Fin 2)) (his : 0 < is.length) (M : ℕ) (hscale : 1 ≤ R / 2 * (↑M + 1)) : (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, orderedRealDerivative is (Ergodic.highRemainder g M) x ^ 2) ^ (1 / 2) ≤ 3072 * (2 ^ is.length * ↑is.length.factorial * √(l2NormSq g) / R ^ is.length) * Real.exp (-(R / 2) * (↑M + 1) / 512)

The ordered derivative commutes with the finite Fourier cutoff, so the previous estimate is the tail of the derivative of (1 - P_M) g itself.