1·
12 days agoYou 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⟩
Being able to call out a middle manager that if these tools are really so great he can just open the PR himself is pretty awesome though.