FrequencyBounded

formal source

  41the derivative f'(t) = Σ_k i ω_k c_k exp(i ω_k t) satisfies
  42|f'(t)| ≤ Ω × Σ_k |c_k|. -/
  43
  44def FrequencyBounded (ω : ℕ → ℝ) (n : ℕ) (Ω : ℝ) : Prop :=
  45  ∀ k, k < n → |ω k| ≤ Ω
  46
  47theorem frequency_bound_nonneg (ω : ℕ → ℝ) (n : ℕ) (Ω : ℝ)
  48    (h : FrequencyBounded ω n Ω) (hn : 0 < n) :
  49    0 ≤ Ω := by
  50  have h0 := h 0 hn
  51  exact le_trans (abs_nonneg _) h0
  52
  53/-! ## Derivative Magnitude Bound (Structural)
  54
  55The key structural result: differentiation multiplies each frequency
  56component by its frequency. For bounded frequencies, this gives
  57the Bernstein bound. -/
  58
  59structure BernsteinBound where
  60  bandwidth : ℝ
  61  bandwidth_pos : 0 < bandwidth
  62  derivative_bound : ℝ
  63  bound_eq : derivative_bound = 2 * Real.pi * bandwidth
  64
  65theorem bernstein_bound_pos (b : BernsteinBound) : 0 < b.derivative_bound := by
  66  rw [b.bound_eq]
  67  exact mul_pos (mul_pos two_pos Real.pi_pos) b.bandwidth_pos
  68
  69/-! ## Amplitude Bound for Finite Sums
  70
  71For f(t) = Σ_{k=0}^{n-1} a_k × cos(ω_k × t + φ_k), we have:
  72|f(t)| ≤ Σ_k |a_k| (triangle inequality). -/
  73
  74def amplitude_sum (a : ℕ → ℝ) (n : ℕ) : ℝ :=