Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum

derivative control for the finite low-frequency trace mode #

The finite Fourier cutoff has no derivative loss beyond its physical frequency radius. Parseval compares every nonempty ordered derivative with the full gradient energy of the same cutoff.

source
def AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.complexWordDerivative :
List (Fin 2) → (Homogenization.Vec 2 → ℂ) → Homogenization.Vec 2 → ℂ

Ordered complex coordinate derivatives used in the trace spectrum estimate.

Equations
Instances For
    source
    theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.complexWordDerivative_contDiff (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℂ} (hf : ContDiff ℝ (↑⊤) f) :
    ContDiff ℝ (↑⊤) (complexWordDerivative w f)
    source
    theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.complexWordDerivative_periodic (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℂ} (hf : Torus.IsZdPeriodic f) :
    Torus.IsZdPeriodic (complexWordDerivative w f)
    source
    theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.orderedRealDerivative_contDiff (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) :
    ContDiff ℝ (↑⊤) (orderedRealDerivative w f)
    source
    theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.orderedRealDerivative_periodic (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : IsZ2Periodic f) :
    IsZ2Periodic (orderedRealDerivative w f)
    source
    theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.complexWordDerivative_realCast (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) :
    complexWordDerivative w (Torus.realToComplex f) = Torus.realToComplex (orderedRealDerivative w f)
    source
    def AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.wordFourierMultiplier :
    List (Fin 2) → (Fin 2 → ℤ) → ℂ

    Product Fourier multiplier associated with a spatial derivative word.

    Equations
    Instances For
      source
      theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.complexWordDerivative_fourierCoeff (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hper : Torus.IsZdPeriodic f) (k : Fin 2 → ℤ) :
      Torus.smoothFourierCoeff (complexWordDerivative w f) k = wordFourierMultiplier w k * Torus.smoothFourierCoeff f k
      source
      theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.wordFourierMultiplier_norm_le (w : List (Fin 2)) {k : Fin 2 → ℤ} {M K : ℝ} (hK : 0 ≤ K) (hfreq : ‖k‖ ≤ M) (hphys : 2 * Real.pi * M ≤ K) :
      ‖wordFourierMultiplier w k‖ ≤ K ^ w.length
      source
      theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceSpectrum.lowProjection_complexFourierCoeff {g : Homogenization.Vec 2 → ℝ} (M : ℕ) (k : Fin 2 → ℤ) :
      Torus.smoothFourierCoeff (Torus.realToComplex (Ergodic.lowProjection g M)) k = if k ∈ Ergodic.frequencyBall M then Torus.smoothFourierCoeff (Torus.realToComplex g) k else 0
      source
      theorem AVenhance.Infra.Section5.RelativeError.lowProjection_orderedDerivative_l2_le {g : Homogenization.Vec 2 → ℝ} (w : List (Fin 2)) (hw : 1 ≤ w.length) (M : ℕ) :
      √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, orderedRealDerivative w (Ergodic.lowProjection g M) x ^ 2) ≤ (2 * Real.pi * √2 * ↑M) ^ (w.length - 1) * √(gradNormSq (spaceGrad (Ergodic.lowProjection g M)))

      Every positive-order real coordinate derivative of the cutoff is bounded in cell L² by its full gradient energy and the physical cutoff radius.