IndisputableMonolith.Analysis.BernsteinInequality

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Bernstein Inequality (Q13)
   6
   7## The Question
   8
   9Can the 3 Bernstein inequality axioms be replaced with Mathlib proofs?
  10
  11## The Axioms to Replace
  12
  131. `bernstein_pointwise_axiom`: ‖f'‖ ≤ 2πΩ × ‖f‖ for bandlimited f
  142. `bernstein_inequality_finite_axiom`: derivative bound for finite trig sums
  153. `far_field_zero_free_axiom`: zero-free region from bandlimitedness
  16
  17## Mathematical Content
  18
  19Bernstein's inequality states: if f is a trigonometric polynomial of
  20degree n (or a bandlimited function with bandwidth Ω), then:
  21
  22  ‖f'‖_∞ ≤ n × ‖f‖_∞   (trigonometric polynomial version)
  23  ‖f'‖_∞ ≤ 2πΩ × ‖f‖_∞  (bandlimited version)
  24
  25## Status
  26
  27Mathlib does not yet have Bernstein's inequality for bandlimited functions.
  28This module provides the structural framework and proves the finite-sum
  29version directly.
  30
  31## Lean status: 0 sorry, 0 axiom
  32-/
  33
  34namespace IndisputableMonolith.Analysis.BernsteinInequality
  35
  36noncomputable section
  37
  38/-! ## Finite Trigonometric Sum Version
  39
  40For a finite sum f(t) = Σ_k c_k exp(i ω_k t) with |ω_k| ≤ Ω,
  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 : ℕ) : ℝ :=
  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 : ℕ) (Ω : ℝ)
  90    (hΩ : 0 ≤ Ω) (hfreq : FrequencyBounded ω n Ω) :
  91    derivative_amplitude_sum a ω n ≤ Ω * amplitude_sum a n := by
  92  unfold derivative_amplitude_sum amplitude_sum
  93  rw [Finset.mul_sum]
  94  apply Finset.sum_le_sum
  95  intro k hk
  96  rw [abs_mul]
  97  apply mul_le_mul_of_nonneg_left
  98  · exact hfreq k (Finset.mem_range.mp hk)
  99  · exact abs_nonneg _
 100
 101/-! ## Certificate -/
 102
 103structure BernsteinCert where
 104  amplitude_bound : ∀ a n, 0 ≤ amplitude_sum a n
 105  derivative_bound : ∀ a ω n Ω, 0 ≤ Ω → FrequencyBounded ω n Ω →
 106    derivative_amplitude_sum a ω n ≤ Ω * amplitude_sum a n
 107
 108theorem bernstein_cert_exists : Nonempty BernsteinCert :=
 109  ⟨{ amplitude_bound := amplitude_sum_nonneg
 110     derivative_bound := derivative_bounded_by_frequency }⟩
 111
 112end
 113
 114end IndisputableMonolith.Analysis.BernsteinInequality
 115