decay_alt

@[blueprint "decay-alt"  (title := "Decay bound, alternate form")  (statement := /--If $\psi:\R \to \C$ is absolutelyintegrable, absolutely continuous, and $\psi'$ is of bounded variation, then$$ |\hat \psi(u)| \leq ( \|\psi\|_1 + \| \psi' \|_{TV} / (2\pi)^2) / (1+|u|^2)$$for all $u \in \R$.  -/)  (proof := /-- Should follow from previous lemmas. -/)  (proofUses := ["prelim-decay", "prelim-decay-3", "decay"])  (latexEnv := "lemma")  (discussion := 564)]theorem decay_alt (ψ : ℝ → ℂ) (hψ : Integrable ψ) (habscont : AbsolutelyContinuous ψ)    (hvar : BoundedVariationOn (deriv ψ) Set.univ) (u : ℝ) :    ‖𝓕 (ψ : ℝ → ℂ) u‖ ≤      ((∫ t, ‖ψ t‖) + (eVariationOn (deriv ψ) Set.univ).toReal / (2 * π) ^ 2) /        (1 + ‖u‖ ^ 2) := by  rw [le_div_iff₀' <| one_add_sq_pos ‖u‖]  by_cases hu : u = 0  · subst hu    simp only [norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero,      one_mul]    calc ‖𝓕 ψ 0‖ ≤ ∫ t, ‖ψ t‖ := prelim_decay ψ 0      _ ≤ (∫ t, ‖ψ t‖) + (eVariationOn (deriv ψ) Set.univ).toReal / (2 * π) ^ 2 := by          have : 0 ≤ (eVariationOn (deriv ψ) Set.univ).toReal / (2 * π) ^ 2 := by positivity          linarith  · have bound1 : ‖𝓕 ψ u‖ ≤ ∫ t, ‖ψ t‖ := prelim_decay ψ u    have bound2 : ‖𝓕 ψ u‖ ≤ (eVariationOn (deriv ψ) Set.univ).toReal / (2 * π * ‖u‖) ^ 2 :=      prelim_decay_3 ψ hψ habscont hvar u hu    have : (2 * π * ‖u‖) ^ 2 = (2 * π) ^ 2 * ‖u‖ ^ 2 := by ring    calc (1 + ‖u‖ ^ 2) * ‖𝓕 ψ u‖        = ‖𝓕 ψ u‖ * 1 + ‖𝓕 ψ u‖ * ‖u‖ ^ 2 := by ring      _ ≤ (∫ t, ‖ψ t‖) * 1 +            (eVariationOn (deriv ψ) Set.univ).toReal / (2 * π * ‖u‖) ^ 2 * ‖u‖ ^ 2 := by          gcongr      _ = (∫ t, ‖ψ t‖) + (eVariationOn (deriv ψ) Set.univ).toReal / (2 * π) ^ 2 := by          rw [mul_one, this, div_mul_eq_div_div]          congr 1          rw [div_mul_eq_mul_div, div_eq_iff (pow_ne_zero 2 <| norm_ne_zero_iff.mpr hu)]