Norm interval Integral exp neg mul sinc tail le

theorem norm_intervalIntegral_exp_neg_mul_sinc_tail_le    {a R B : ℝ} (ha : 0 < a) (hR : 1 ≤ R) (hRB : R ≤ B) :    ‖∫ x in R..B, Real.exp (-a * x) * Real.sinc x‖ ≤ 4 * R⁻¹ := by  have hR_pos : 0 < R := zero_lt_one.trans_le hR  have hB_pos : 0 < B := hR_pos.trans_le hRB  have hpos_uIcc : ∀ x ∈ Set.uIcc R B, 0 < x := by    intro x hx    rw [Set.uIcc_of_le hRB] at hx    exact hR_pos.trans_le hx.1  have hpos_Icc : ∀ x ∈ Set.Icc R B, 0 < x := by    intro x hx    exact hR_pos.trans_le hx.1  have hsinc :      (∫ x in R..B, Real.exp (-a * x) * Real.sinc x) =        ∫ x in R..B, (Real.exp (-a * x) * x⁻¹) * Real.sin x := by    refine intervalIntegral.integral_congr ?_    intro x hx    have hx0 : x ≠ 0 := (hpos_uIcc x hx).ne'    simp only [Real.sinc_of_ne_zero hx0]    ring  have hu : ∀ x ∈ Set.uIcc R B,      HasDerivAt (fun y : ℝ => Real.exp (-a * y) * y⁻¹)        (-(a * Real.exp (-a * x) * x⁻¹) - Real.exp (-a * x) * (x ^ 2)⁻¹) x := by    intro x hx    have hx0 : x ≠ 0 := (hpos_uIcc x hx).ne'    have hlin : HasDerivAt (fun y : ℝ => -a * y) (-a) x := by      simpa using (hasDerivAt_id x).const_mul (-a)    have hexp := (Real.hasDerivAt_exp (-a * x)).comp x hlin    have hinv := hasDerivAt_inv hx0    have hmul := hexp.mul hinv    rw [show -(a * Real.exp (-a * x) * x⁻¹) - Real.exp (-a * x) * (x ^ 2)⁻¹        = Real.exp (-a * x) * -a * x⁻¹ + Real.exp (-a * x) * -(x ^ 2)⁻¹ from by ring]    exact hmul  have hv : ∀ x ∈ Set.uIcc R B,      HasDerivAt (fun y : ℝ => -Real.cos y) (Real.sin x) x := by    intro x _hx    have h : HasDerivAt (fun y : ℝ => -Real.cos y) (-(-Real.sin x)) x :=      (Real.hasDerivAt_cos x).neg    rwa [neg_neg] at h  have hu' : IntervalIntegrable      (fun x : ℝ => -(a * Real.exp (-a * x) * x⁻¹) -        Real.exp (-a * x) * (x ^ 2)⁻¹) volume R B := by    apply ContinuousOn.intervalIntegrable_of_Icc hRB    have hcont_exp : ContinuousOn (fun x : ℝ => Real.exp (-a * x)) (Set.Icc R B) := by      fun_prop    have hcont_inv : ContinuousOn (fun x : ℝ => x⁻¹) (Set.Icc R B) :=      continuousOn_id.inv₀ fun x hx => (hpos_Icc x hx).ne'    have hcont_inv_sq : ContinuousOn (fun x : ℝ => (x ^ 2)⁻¹) (Set.Icc R B) :=      (continuousOn_pow 2).inv₀ fun x hx => pow_ne_zero 2 (hpos_Icc x hx).ne'    exact (((continuousOn_const.mul hcont_exp).mul hcont_inv).neg.sub      (hcont_exp.mul hcont_inv_sq))  have hv' : IntervalIntegrable (fun x : ℝ => Real.sin x) volume R B :=    Real.continuous_sin.intervalIntegrable R B  have hIBP := intervalIntegral.integral_mul_deriv_eq_deriv_mul    (u := fun x : ℝ => Real.exp (-a * x) * x⁻¹) (v := fun x : ℝ => -Real.cos x)    (u' := fun x : ℝ => -(a * Real.exp (-a * x) * x⁻¹) -      Real.exp (-a * x) * (x ^ 2)⁻¹)    (v' := fun x : ℝ => Real.sin x) hu hv hu' hv'  have hint :      (∫ x in R..B,        (-(a * Real.exp (-a * x) * x⁻¹) - Real.exp (-a * x) * (x ^ 2)⁻¹) *          -Real.cos x) =        ∫ x in R..B,          (a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹) *            Real.cos x := by    apply intervalIntegral.integral_congr    intro x _hx    ring  have hrepr :      ∫ x in R..B, Real.exp (-a * x) * Real.sinc x =        (-Real.exp (-a * B) * B⁻¹ * Real.cos B +            Real.exp (-a * R) * R⁻¹ * Real.cos R) -          ∫ x in R..B,            (a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹) *              Real.cos x := by    rw [hsinc, hIBP, hint]    ring  have hboundary :      ‖-Real.exp (-a * B) * B⁻¹ * Real.cos B +          Real.exp (-a * R) * R⁻¹ * Real.cos R‖ ≤ 2 * R⁻¹ := by    calc      ‖-Real.exp (-a * B) * B⁻¹ * Real.cos B +          Real.exp (-a * R) * R⁻¹ * Real.cos R‖          = |(-Real.exp (-a * B) * B⁻¹ * Real.cos B) +              (Real.exp (-a * R) * R⁻¹ * Real.cos R)| := by rw [Real.norm_eq_abs]      _ ≤ |-Real.exp (-a * B) * B⁻¹ * Real.cos B| +            |Real.exp (-a * R) * R⁻¹ * Real.cos R| := abs_add_le _ _      _ ≤ B⁻¹ + R⁻¹ := by            refine add_le_add ?_ ?_            · calc                |-Real.exp (-a * B) * B⁻¹ * Real.cos B|                    = Real.exp (-a * B) * B⁻¹ * |Real.cos B| := by                      rw [abs_mul, abs_mul, abs_neg, abs_of_pos (Real.exp_pos _),                        abs_of_pos (inv_pos.mpr hB_pos)]                  _ ≤ 1 * B⁻¹ * 1 := by                      gcongr                      · exact Real.exp_le_one_iff.mpr (by                          have hmul : 0 ≤ a * B := mul_nonneg ha.le hB_pos.le                          nlinarith)                      · exact Real.abs_cos_le_one B                  _ = B⁻¹ := by ring            · calc                |Real.exp (-a * R) * R⁻¹ * Real.cos R|                    = Real.exp (-a * R) * R⁻¹ * |Real.cos R| := by                      rw [abs_mul, abs_mul, abs_of_pos (Real.exp_pos _),                        abs_of_pos (inv_pos.mpr hR_pos)]                  _ ≤ 1 * R⁻¹ * 1 := by                      gcongr                      · exact Real.exp_le_one_iff.mpr (by                          have hmul : 0 ≤ a * R := mul_nonneg ha.le hR_pos.le                          nlinarith)                      · exact Real.abs_cos_le_one R                  _ = R⁻¹ := by ring      _ ≤ R⁻¹ + R⁻¹ := by            exact add_le_add (by              simpa [one_div] using one_div_le_one_div_of_le hR_pos hRB) le_rfl      _ = 2 * R⁻¹ := by ring  have hnormInt : IntervalIntegrable      (fun x : ℝ =>        ‖(a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹) *          Real.cos x‖) volume R B := by    apply ContinuousOn.intervalIntegrable_of_Icc hRB    have hcont_exp : ContinuousOn (fun x : ℝ => Real.exp (-a * x)) (Set.Icc R B) := by      fun_prop    have hcont_inv : ContinuousOn (fun x : ℝ => x⁻¹) (Set.Icc R B) :=      continuousOn_id.inv₀ fun x hx => (hpos_Icc x hx).ne'    have hcont_inv_sq : ContinuousOn (fun x : ℝ => (x ^ 2)⁻¹) (Set.Icc R B) :=      (continuousOn_pow 2).inv₀ fun x hx => pow_ne_zero 2 (hpos_Icc x hx).ne'    exact ((((continuousOn_const.mul hcont_exp).mul hcont_inv).add      (hcont_exp.mul hcont_inv_sq)).mul Real.continuous_cos.continuousOn).norm  have hboundInt : IntervalIntegrable      (fun x : ℝ => R⁻¹ * (a * Real.exp (-a * x)) + (x ^ 2)⁻¹) volume R B := by    apply ContinuousOn.intervalIntegrable_of_Icc hRB    have hcont_exp : ContinuousOn (fun x : ℝ => Real.exp (-a * x)) (Set.Icc R B) := by      fun_prop    have hcont_inv_sq : ContinuousOn (fun x : ℝ => (x ^ 2)⁻¹) (Set.Icc R B) :=      (continuousOn_pow 2).inv₀ fun x hx => pow_ne_zero 2 (hpos_Icc x hx).ne'    exact ((continuousOn_const.mul (continuousOn_const.mul hcont_exp)).add hcont_inv_sq)  have hJ :      ‖∫ x in R..B,        (a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹) *          Real.cos x‖ ≤ 2 * R⁻¹ := by    calc      ‖∫ x in R..B,        (a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹) *          Real.cos x‖          ≤ ∫ x in R..B,              ‖(a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹) *                Real.cos x‖ :=            intervalIntegral.norm_integral_le_integral_norm hRB      _ ≤ ∫ x in R..B, R⁻¹ * (a * Real.exp (-a * x)) + (x ^ 2)⁻¹ := by            refine intervalIntegral.integral_mono_on hRB hnormInt hboundInt ?_            intro x hx            have hx_pos : 0 < x := hpos_Icc x hx            have hR_inv : x⁻¹ ≤ R⁻¹ := by              simpa [one_div] using one_div_le_one_div_of_le hR_pos hx.1            calc              ‖(a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹) *                Real.cos x‖                  ≤ |a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹| := by                    rw [Real.norm_eq_abs, abs_mul]                    exact mul_le_of_le_one_right (abs_nonneg _) (Real.abs_cos_le_one x)              _ = a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹ := by                    rw [abs_of_nonneg]                    positivity              _ ≤ R⁻¹ * (a * Real.exp (-a * x)) + (x ^ 2)⁻¹ := by                    refine add_le_add ?_ ?_                    · calc                        a * Real.exp (-a * x) * x⁻¹                            = (a * Real.exp (-a * x)) * x⁻¹ := by ring                        _ ≤ (a * Real.exp (-a * x)) * R⁻¹ :=                            mul_le_mul_of_nonneg_left hR_inv                              (mul_nonneg ha.le (Real.exp_pos _).le)                        _ = R⁻¹ * (a * Real.exp (-a * x)) := by ring                    · calc                        Real.exp (-a * x) * (x ^ 2)⁻¹                            ≤ 1 * (x ^ 2)⁻¹ := by                              exact mul_le_mul_of_nonneg_right                                (Real.exp_le_one_iff.mpr (by                                  have hmul : 0 ≤ a * x := mul_nonneg ha.le hx_pos.le                                  nlinarith))                                (inv_nonneg.mpr (sq_nonneg x))                        _ = (x ^ 2)⁻¹ := by ring      _ = R⁻¹ * (∫ x in R..B, a * Real.exp (-a * x)) +            ∫ x in R..B, (x ^ 2)⁻¹ := by            rw [intervalIntegral.integral_add]            · rw [intervalIntegral.integral_const_mul]            · exact (Continuous.intervalIntegrable (by fun_prop) R B).const_mul _            · apply ContinuousOn.intervalIntegrable_of_Icc hRB              exact (continuousOn_pow 2).inv₀ fun x hx =>                pow_ne_zero 2 (hpos_Icc x hx).ne'      _ = R⁻¹ * (Real.exp (-a * R) - Real.exp (-a * B)) + (R⁻¹ - B⁻¹) := by            rw [intervalIntegral_exp_neg_mul_const_mul_self a R B,              intervalIntegral_inv_sq_of_pos hR_pos hRB]      _ ≤ R⁻¹ * 1 + R⁻¹ := by            gcongr            · exact (sub_le_self _ (Real.exp_pos _).le).trans                (Real.exp_le_one_iff.mpr (by                  have hmul : 0 ≤ a * R := mul_nonneg ha.le hR_pos.le                  nlinarith))            · exact sub_le_self _ (inv_nonneg.mpr hB_pos.le)      _ = 2 * R⁻¹ := by ring  rw [hrepr]  calc    ‖(-Real.exp (-a * B) * B⁻¹ * Real.cos B +        Real.exp (-a * R) * R⁻¹ * Real.cos R) -        ∫ x in R..B,          (a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹) *            Real.cos x‖        ≤ ‖-Real.exp (-a * B) * B⁻¹ * Real.cos B +            Real.exp (-a * R) * R⁻¹ * Real.cos R‖ +            ‖∫ x in R..B,              (a * Real.exp (-a * x) * x⁻¹ + Real.exp (-a * x) * (x ^ 2)⁻¹) *                Real.cos x‖ := norm_sub_le _ _    _ ≤ 2 * R⁻¹ + 2 * R⁻¹ := add_le_add hboundary hJ    _ = 4 * R⁻¹ := by ring