W21 approximation

theorem W21_approximation (f : W21) (g : trunc) :    Tendsto (fun R => ‖f - (g.scale R * f : W21)‖) atTop (𝓝 0) := by   -- Definitions  let f' := f.deriv  let f'' := f'.deriv  let g' := (g : CS 2 ℝ).deriv  let g'' := g'.deriv  let h R v := 1 - g.scale R v  let h' R := - (g.scale R).deriv  let h'' R := - (g.scale R).deriv.deriv   -- Properties of h  have ch {R} : Continuous (fun v => (h R v : ℂ)) :=    continuous_ofReal.comp <| continuous_const.sub (CS.continuous _)  have ch' {R} : Continuous (fun v => (h' R v : ℂ)) := continuous_ofReal.comp (CS.continuous _)  have ch'' {R} : Continuous (fun v => (h'' R v : ℂ)) := continuous_ofReal.comp (CS.continuous _)  have dh R v : HasDerivAt (h R) (h' R v) v := by    convert! CS.hasDerivAt_scale (g : CS 2 ℝ) R v |>.const_sub 1 using 1    simp [h', CS.deriv_scale', show g.deriv.toFun = deriv g.toFun from rfl]  have dh' R v : HasDerivAt (h' R) (h'' R v) v := ((g.scale R).deriv.hasDerivAt v).neg  have hh1 R v : |h R v| ≤ 1 := by    by_cases hR : R = 0 <;>      simp only [CS.scale, funscale, smul_eq_mul, hR, ↓reduceDIte, Pi.zero_apply, sub_zero,        abs_one, le_refl, h]    rw [abs_le] ; constructor <;>    linarith [g.le_one (R⁻¹ * v), g.nonneg (R⁻¹ * v)]  have vR v : Tendsto (fun R : ℝ => v * R⁻¹) atTop (𝓝 0) := by    simpa using tendsto_inv_atTop_zero.const_mul v   -- Proof  convert_to Tendsto (fun R => W21.norm (fun v => h R v * f v)) atTop (𝓝 0)  · ext R ; change W21.norm _ = _ ; congr ; ext v ; simp [h, sub_mul] ; rfl  rw [show (0 : ℝ) = 0 + ((4 * π ^ 2)⁻¹ : ℝ) * 0 by simp]  refine Tendsto.add ?_ (Tendsto.const_mul _ ?_)   · let F R v := ‖h R v * f v‖    have eh v : ∀ᶠ R in atTop, h R v = 0 := by      filter_upwards [(vR v).eventually g.zero, eventually_ne_atTop 0] with R hR hR'      simp [h, hR, CS.scale, hR', funscale, mul_comm R⁻¹]    have e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume := by      apply Eventually.of_forall ; intro R      exact (ch.mul f.continuous).norm.aestronglyMeasurable    have e2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : ℝ), ‖F n a‖ ≤ ‖f a‖ := by      apply Eventually.of_forall ; intro R      apply Eventually.of_forall ; intro v      simpa [F] using mul_le_mul (hh1 R v) le_rfl (by simp) zero_le_one    have e4 : ∀ᵐ (a : ℝ), Tendsto (fun n ↦ F n a) atTop (𝓝 0) := by      apply Eventually.of_forall ; intro v      apply tendsto_nhds_of_eventually_eq ; filter_upwards [eh v] with R hR ; simp [F, hR]    simpa [F] using tendsto_integral_filter_of_dominated_convergence _ e1 e2 f.hf.norm e4   · let F R v := ‖h'' R v * f v + 2 * h' R v * f' v + h R v * f'' v‖    convert_to Tendsto (fun R ↦ ∫ (v : ℝ), F R v) atTop (𝓝 0)    · have this R v :        deriv (deriv (fun v => h R v * f v)) v =          h'' R v * f v + 2 * h' R v * f' v + h R v * f'' v := by        have df v : HasDerivAt f (f' v) v := f.hasDerivAt v        have df' v : HasDerivAt f' (f'' v) v := f'.hasDerivAt v        have l3 v : HasDerivAt (fun v => h R v * f v) (h' R v * f v + h R v * f' v) v :=          (dh R v).ofReal_comp.mul (df v)        have l5 : HasDerivAt (fun v => h' R v * f v) (h'' R v * f v + h' R v * f' v) v :=          (dh' R v).ofReal_comp.mul (df v)        have l7 : HasDerivAt (fun v => h R v * f' v) (h' R v * f' v + h R v * f'' v) v :=          (dh R v).ofReal_comp.mul (df' v)        have d1 : deriv (fun v => h R v * f v) = fun v => h' R v * f v + h R v * f' v :=          funext (fun v => (l3 v).deriv)        rw [d1] ; convert! (l5.add l7).deriv using 1 ; ring      simp_rw [this, F]     obtain ⟨c1, mg'⟩ := g'.bounded    obtain ⟨c2, mg''⟩ := g''.bounded    let bound v := c2 * ‖f v‖ + 2 * c1 * ‖f' v‖ + ‖f'' v‖    have e1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (F n) volume := by      apply Eventually.of_forall ; intro R ; apply (Continuous.norm ?_).aestronglyMeasurable      exact ((ch''.mul f.continuous).add ((continuous_const.mul ch').mul f.deriv.continuous)).add        (ch.mul f.deriv.deriv.continuous)    have e2 : ∀ᶠ R in atTop, ∀ᵐ (a : ℝ), ‖F R a‖ ≤ bound a := by      have hc1 : ∀ᶠ R in atTop, ∀ v, |h' R v| ≤ c1 := by        filter_upwards [eventually_ge_atTop 1] with R hR v        have hR' : R ≠ 0 := by linarith        have : 0 ≤ R := by linarith        simp only [CS.deriv_scale, CS.neg_apply, CS.smul_apply, smul_eq_mul, abs_neg, abs_mul,          abs_inv, abs_eq_self.mpr this, ge_iff_le, h']        simp only [CS.scale, hR', ↓reduceDIte, funscale, smul_eq_mul]        convert_to _ ≤ c1 * 1        · simp        · rw [mul_comm]          apply mul_le_mul (mg' _)            (inv_le_of_inv_le₀ (by linarith) (by simpa using hR)) (by positivity)          exact (abs_nonneg _).trans (mg' 0)      have hc2 : ∀ᶠ R in atTop, ∀ v, |h'' R v| ≤ c2 := by        filter_upwards [eventually_ge_atTop 1] with R hR v        have e1 : 0 ≤ R := by linarith        have e2 : R⁻¹ ≤ 1 := inv_le_of_inv_le₀ (by linarith) (by simpa using hR)        have e3 : R ≠ 0 := by linarith        simp only [CS.deriv_scale, CS.deriv_smul, CS.neg_apply, CS.smul_apply, smul_eq_mul, abs_neg,          abs_mul, abs_inv, abs_eq_self.mpr e1, ge_iff_le, h'']        convert_to _ ≤ 1 * (1 * c2)        · simp        apply mul_le_mul e2 ?_ (by positivity) zero_le_one        apply mul_le_mul e2 ?_ (by positivity) zero_le_one        simp only [CS.scale, e3, ↓reduceDIte, funscale, smul_eq_mul] ; apply mg''      filter_upwards [hc1, hc2] with R hc1 hc2      apply Eventually.of_forall ; intro v ; specialize hc1 v ; specialize hc2 v      simp only [F, bound, norm_norm]      refine (norm_add_le _ _).trans ?_ ; apply add_le_add      · refine (norm_add_le _ _).trans ?_ ; apply add_le_add <;> simp only [Complex.norm_mul,        Complex.norm_ofNat, norm_real, norm_eq_abs] <;> gcongr      · simpa using mul_le_mul (hh1 R v) le_rfl (by simp) zero_le_one    have e3 : Integrable bound volume :=      (((f.hf.norm).const_mul _).add ((f.hf'.norm).const_mul _)).add f.hf''.norm    have e4 : ∀ᵐ (a : ℝ), Tendsto (fun n ↦ F n a) atTop (𝓝 0) := by      apply Eventually.of_forall ; intro v      have evg' : g' =ᶠ[𝓝 0] 0 := by convert! ← g.zero.deriv ; exact deriv_const' _      have evg'' : g'' =ᶠ[𝓝 0] 0 := by convert! ← evg'.deriv ; exact deriv_const' _      refine tendsto_norm_zero.comp <| (ZeroAtFilter.add ?_ ?_).add ?_      · have eh'' v : ∀ᶠ R in atTop, h'' R v = 0 := by          filter_upwards [(vR v).eventually evg'', eventually_ne_atTop 0] with R hR hR'          simp only [CS.deriv_scale, CS.deriv_smul, CS.neg_apply, CS.smul_apply, smul_eq_mul,            neg_eq_zero, mul_eq_zero, inv_eq_zero, hR', false_or, h'']          simp only [CS.scale, hR', ↓reduceDIte, funscale, smul_eq_mul, mul_comm R⁻¹]          exact hR        apply tendsto_nhds_of_eventually_eq        filter_upwards [eh'' v] with R hR ; simp [hR]      · have eh' v : ∀ᶠ R in atTop, h' R v = 0 := by          filter_upwards [(vR v).eventually evg'] with R hR          simp [g'] at hR          simp [h', CS.deriv_scale', mul_comm R⁻¹, hR]        apply tendsto_nhds_of_eventually_eq        filter_upwards [eh' v] with R hR ; simp [hR]      · simpa [h] using! ((g.tendsto_scale v).const_sub 1).ofReal.mul tendsto_const_nhds    simpa [F] using tendsto_integral_filter_of_dominated_convergence bound e1 e2 e3 e4