integrable_bump_convolution

lemma integrable_bump_convolution {f g : ℝ → ℝ}    (hf : MemLp f ∞ volume) (hg : MemLp g ∞ volume) (periodic_g : g.Periodic (2 * π))    {r : ℝ} (hr : r ∈ Ioo 0 π) (hle : ∀ x, |g x| ≤ niceKernel r x) :    eLpNorm (fun x ↦ ∫ y in (0)..2 * π, f y * g (x - y)) 2 (volume.restrict (Ioc 0 (2 * π))) ≤    17 * eLpNorm f 2 (volume.restrict (Ioc 0 (2 * π))) := by  obtain ⟨hr0, hrπ⟩ := hr  have h_integrable {a b} := niceKernel_intervalIntegrable a b hr0  have hg_integrable : Integrable g (volume.restrict (Ioc 0 (2 * π))) := by    apply IntegrableOn.integrable    rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith)]    apply h_integrable.mono_fun hg.1.restrict (Filter.Eventually.of_forall ?_)    simpa [abs_of_pos (niceKernel_pos hr0)] using hle  have hbound_integrable : IntervalIntegrable (fun x ↦ 4 * r / x ^ 2) volume r π := by    apply ContinuousOn.intervalIntegrable_of_Icc hrπ.le    have (x) (hx : x ∈ Icc r π) : x ^ 2 ≠ 0 := pow_ne_zero 2 (by linarith [mem_Icc.mp hx])    fun_prop (disch := assumption)  grw [young_convolution hf.1.aemeasurable hg.1.aemeasurable periodic_g, mul_comm]  gcongr  have: eLpNorm g 1 (volume.restrict (Ioc 0 (2 * π))) ≠ ⊤ := by    grw [← lt_top_iff_ne_top,      eLpNorm_le_eLpNorm_mul_rpow_measure_univ (OrderTop.le_top 1) (hg.restrict _).1]    exact ENNReal.mul_lt_top (hg.restrict _).eLpNorm_lt_top      (by norm_num; simp [← ENNReal.ofReal_ofNat, ← ENNReal.ofReal_mul])  rw [← ENNReal.toReal_le_toReal this (by norm_num)]  calc    _ ≤ ∫ x in (0)..2 * π, niceKernel r x := by      simp_rw [eLpNorm_one_eq_lintegral_enorm]      rw [← ofReal_integral_norm_eq_lintegral_enorm hg_integrable,        ENNReal.toReal_ofReal (by positivity), intervalIntegral.integral_of_le (by positivity)]      apply setIntegral_mono_on hg_integrable.norm ?_ measurableSet_Ioc (fun x _ ↦ hle x)      exact intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith) |>.mp h_integrable    _ = 2 * ∫ x in (0)..π, niceKernel r x := by      have := (zero_add (2 * π)) ▸ (niceKernel_periodic r).intervalIntegral_add_eq 0 (-π)      rw [this, show -π + 2 * π = π by group, ← intervalIntegral.integral_add_adjacent_intervals        (b := 0) h_integrable h_integrable, two_mul]      have := intervalIntegral.integral_comp_neg (a := -π) (b := 0) (niceKernel r)      simpa [neg_zero, neg_neg, niceKernel_neg]    _ = 2 * (∫ x in (0)..r, niceKernel r x) + 2 * ∫ x in r..π, niceKernel r x := by      rw [← mul_add, intervalIntegral.integral_add_adjacent_intervals h_integrable h_integrable]    _ ≤ 2 * (∫ _ in (0)..r, r⁻¹) + 2 * ∫ x in r..π, 1 + (4 * r) / x ^ 2 := by      gcongr      · refine le_of_eq <| intervalIntegral.integral_congr (g := fun _ ↦ r⁻¹) fun x hx ↦ ?_        rw [uIcc_of_le (by positivity)] at hx        exact niceKernel_eq_inv ⟨hr0, hrπ⟩ hx      · apply intervalIntegral.integral_mono_on hrπ.le h_integrable        · exact IntervalIntegrable.add intervalIntegrable_const hbound_integrable        · exact fun x hx ↦ niceKernel_upperBound hr0 hx    _ ≤ 2 + (2 * π + 8 * r * (r⁻¹ - π⁻¹)) := by      gcongr      · simp [mul_inv_le_one]      have (x : ℝ) : 4 * r / x ^ 2 = (4 * r) * (x ^ (-2 : ℤ)) := rfl      rw [intervalIntegral.integral_add intervalIntegrable_const hbound_integrable]      simp_rw [        intervalIntegral.integral_const, this, intervalIntegral.integral_const_mul, ge_iff_le,        smul_eq_mul, mul_one, mul_add, ← mul_assoc, show 2 * 4 * r = 8 * r by group]      gcongr      · linarith      rw [integral_zpow]      · apply le_of_eq; group      · exact .inr ⟨by trivial, by simp [mem_uIcc, hr0, Real.pi_pos]⟩    _ ≤ (17 : ℝ≥0∞).toReal := by      rw [mul_sub, mul_inv_cancel_right₀ hr0.ne.symm]      grw [sub_le_self 8 (by positivity), Real.pi_lt_d2]      norm_num