BernsteinBound

formal source

  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 : ℕ) : ℝ :=
  75  (Finset.range n).sum (fun k => |a k|)
  76
  77theorem amplitude_sum_nonneg (a : ℕ → ℝ) (n : ℕ) :
  78    0 ≤ amplitude_sum a n := by
  79  unfold amplitude_sum
  80  exact Finset.sum_nonneg (fun k _ => abs_nonneg _)
  81
  82/-! ## Derivative Amplitude Bound
  83
  84|f'(t)| ≤ Σ_k |a_k × ω_k| ≤ Ω × Σ_k |a_k| when |ω_k| ≤ Ω. -/
  85
  86def derivative_amplitude_sum (a ω : ℕ → ℝ) (n : ℕ) : ℝ :=
  87  (Finset.range n).sum (fun k => |a k * ω k|)
  88
  89theorem derivative_bounded_by_frequency (a ω : ℕ → ℝ) (n : ℕ) (Ω : ℝ)