Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Ergodic.FourierDecay

Fourier decay from averaged derivative bounds #

source
def AVenhance.Infra.Ergodic.coordDerivIter {d : ℕ} (i : Fin d) :
ℕ → (Homogenization.Vec d → ℂ) → Homogenization.Vec d → ℂ

Iterate differentiation in one coordinate direction.

Equations
Instances For
    source
    theorem AVenhance.Infra.Ergodic.FourierDecay.coordDeriv_contDiff_top {d : ℕ} (i : Fin d) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) :
    ContDiff ℝ (↑⊤) (Torus.coordDeriv i f)
    source
    theorem AVenhance.Infra.Ergodic.coordDerivIter_contDiff_top {d : ℕ} (i : Fin d) (n : ℕ) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) :
    ContDiff ℝ (↑⊤) (coordDerivIter i n f)
    source
    theorem AVenhance.Infra.Ergodic.FourierDecay.coordDeriv_periodic {d : ℕ} (i : Fin d) {f : Homogenization.Vec d → ℂ} (hf : Torus.IsZdPeriodic f) :
    Torus.IsZdPeriodic (Torus.coordDeriv i f)
    source
    theorem AVenhance.Infra.Ergodic.coordDerivIter_periodic {d : ℕ} (i : Fin d) (n : ℕ) {f : Homogenization.Vec d → ℂ} (hf : Torus.IsZdPeriodic f) :
    Torus.IsZdPeriodic (coordDerivIter i n f)
    source
    theorem AVenhance.Infra.Ergodic.smoothFourierCoeff_norm_le_integral_norm {d : ℕ} {f : Homogenization.Vec d → ℂ} (k : Fin d → ℤ) :
    ‖Torus.smoothFourierCoeff f k‖ ≤ ∫ (x : Homogenization.Vec d) in Torus.unitCell d, ‖f x‖
    source
    theorem AVenhance.Infra.Ergodic.smoothFourierCoeff_coordDerivIter {d : ℕ} (hd : 0 < d) (i : Fin d) (n : ℕ) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hper : Torus.IsZdPeriodic f) (k : Fin d → ℤ) :
    Torus.smoothFourierCoeff (coordDerivIter i n f) k = (2 * ↑Real.pi * Complex.I * ↑(k i)) ^ n * Torus.smoothFourierCoeff f k
    source
    def AVenhance.Infra.Ergodic.HasCoordinateAnalyticL1Bounds {d : ℕ} (f : Homogenization.Vec d → ℂ) (Cf r : ℝ) :
    Prop

    Factorial analytic bounds for positive-order coordinate derivatives in L¹.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AVenhance.Infra.Ergodic.smoothFourierCoeff_le_derivative_average {d : ℕ} (hd : 0 < d) (i : Fin d) (n : ℕ) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hper : Torus.IsZdPeriodic f) (M : ℝ) (hM : ∫ (x : Homogenization.Vec d) in Torus.unitCell d, ‖coordDerivIter i n f x‖ ≤ M) (k : Fin d → ℤ) (hki : k i ≠ 0) :
      ‖Torus.smoothFourierCoeff f k‖ ≤ M / (2 * Real.pi * ‖k i‖) ^ n

      Repeatedly applying the coordinate Fourier multiplier bounds a Fourier coefficient by the averaged derivative of the same order.

      source
      theorem AVenhance.Infra.Ergodic.FourierDecay.factorial_fourier_decay_optimization {x : ℝ} (hx : 1 ≤ x) :
      ∃ (n : ℕ), 0 < n ∧ ↑n.factorial / (2 * Real.pi * x) ^ n ≤ 512 * Real.exp (-x / 512)
      source
      theorem AVenhance.Infra.Ergodic.factorial_fourier_decay_optimization_exists {x : ℝ} (hx : 1 ≤ x) :
      ∃ (n : ℕ), 0 < n ∧ ↑n.factorial / (2 * Real.pi * x) ^ n ≤ 512 * Real.exp (-x / 512)

      The factorial optimization used to pass from iterated derivative bounds to exponential decay; exported for Parseval tail estimates.

      source
      theorem AVenhance.Infra.Ergodic.smoothFourierCoeff_expDecay_of_coordinateAnalyticL1Bounds {d : ℕ} (hd : 0 < d) {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (hper : Torus.IsZdPeriodic f) (Cf r : ℝ) (hCf : 0 ≤ Cf) (_hr : 0 < r) (hderiv : HasCoordinateAnalyticL1Bounds f Cf r) (k : Fin d → ℤ) (hk : k ≠ 0) (hlarge : 1 ≤ r * ‖k‖) :
      ‖Torus.smoothFourierCoeff f k‖ ≤ 512 * Cf * Real.exp (-r * ‖k‖ / 512)

      Exponential decay of nonzero Fourier modes from averaged bounds on every positive-order repeated coordinate derivative. The lower-frequency condition is the one used in l.averages: r * ‖k‖ ≥ 1.