Technology

You know what all those methods have in common? FUCKING evaluation of smooth continuous functions based on a limited number of samples.

REAL MEN WRITE REAL PROOFS. They don't use God damned computational methods which completely IGNORE non-converging regions.

I used opus to generate this lean-verifiable proof that you in particular are full of shit!

import Mathlib
open Real

noncomputable def f (x : ℝ) : ℝ := sin (π * x) * exp (-x^2)

lemma f_smooth : ContDiff ℝ ⊤ f :=
  (contDiff_sin.comp (contDiff_const.mul contDiff_id)).mul
    (contDiff_exp.comp (contDiff_id.pow 2).neg)

lemma f_zero_on_ints : ∀ n : ℤ, f n = 0 := by
  intro n
  show sin (π * (n : ℝ)) * exp (-((n : ℝ))^2) = 0
  rw [mul_comm π (n : ℝ), sin_int_mul_pi, zero_mul]

lemma f_ne_zero : f ≠ 0 := fun h => by
  have h₁ : f (1/2) = 0 := congrFun h (1/2)
  have h₂ : f (1/2) = exp (-(1/2)^2) := by
    show sin (π * (1/2)) * exp (-(1/2)^2) = exp (-(1/2)^2)
    rw [show π * (1/2) = π/2 from by ring, sin_pi_div_two, one_mul]
  exact (exp_pos _).ne' (h₂ ▸ h₁)

theorem sampling_is_a_lie :
    ∃ f : ℝ → ℝ,
      ContDiff ℝ ⊤ f ∧
      (∀ n : ℤ, f n = 0) ∧
      f ≠ 0 :=
  ⟨f, f_smooth, f_zero_on_ints, f_ne_zero⟩