integrable_norm_fourier_scaled_of_CS2

lemma integrable_norm_fourier_scaled_of_CS2    (ψ : CS 2 ℂ) :    Integrable (fun u : ℝ => ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖) := by  obtain ⟨C, hdecay⟩ := fourier_decay_of_CS2 (ψ := ψ)  have hC_nonneg : 0 ≤ C := by    have h0 := hdecay 0    have hnorm : 0 ≤ ‖𝓕 (ψ : ℝ → ℂ) 0‖ := norm_nonneg _    have hC' : ‖𝓕 (ψ : ℝ → ℂ) 0‖ ≤ C := by simpa using h0    exact hnorm.trans hC'  have hmaj_int : Integrable (fun u : ℝ => (C : ℝ) / (1 + (u / (2 * Real.pi))^2)) := by    have hbase : Integrable (fun u : ℝ => (1 + u ^ 2)⁻¹) := integrable_inv_one_add_sq    have hscale :        Integrable (fun u : ℝ => (1 + (u / (2 * Real.pi)) ^ 2)⁻¹) :=      hbase.comp_div (by nlinarith [Real.pi_pos])    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc, pow_two] using      hscale.const_mul C  have hle :      (fun u : ℝ => ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖)        ≤ᵐ[volume]      (fun u : ℝ => (C : ℝ) / (1 + (u / (2 * Real.pi))^2)) := by    refine Filter.Eventually.of_forall ?_    intro u    simpa using (hdecay (u / (2 * Real.pi)))  have hle_norm :      (fun u : ℝ => ‖‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖‖)        ≤ᵐ[volume]      (fun u : ℝ => ‖(C : ℝ) / (1 + (u / (2 * Real.pi))^2)‖) := by    refine hle.mono ?_    intro u hu    have hden_pos : 0 < 1 + (u / (2 * Real.pi)) ^ 2 := by nlinarith    have hnonneg : 0 ≤ (C : ℝ) / (1 + (u / (2 * Real.pi))^2) :=      div_nonneg hC_nonneg hden_pos.le    have hleft_nonneg : 0 ≤ ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖ := norm_nonneg _    have hbound : ‖‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖‖ ≤        (C : ℝ) / (1 + (u / (2 * Real.pi))^2) := by      simpa [Real.norm_eq_abs, abs_of_nonneg hleft_nonneg] using hu    have hC_abs : |C| = C := abs_of_nonneg hC_nonneg    have hden_abs : |1 + (u / (2 * Real.pi))^2| = 1 + (u / (2 * Real.pi))^2 := by      have : 0 ≤ 1 + (u / (2 * Real.pi))^2 := by nlinarith      simpa using abs_of_nonneg this    have hnorm :        ‖(C : ℝ) / (1 + (u / (2 * Real.pi))^2)‖ =          (C : ℝ) / (1 + (u / (2 * Real.pi))^2) := by      have hrec :          ‖(C : ℝ) / (1 + (u / (2 * Real.pi))^2)‖ =            |C| / |1 + (u / (2 * Real.pi))^2| := by        simp [Real.norm_eq_abs]      simp [hC_abs, hden_abs, hrec]    simpa [hnorm] using hbound  have hmaj_int_norm :      Integrable (fun u : ℝ => ‖(C : ℝ) / (1 + (u / (2 * Real.pi))^2)‖) :=    hmaj_int.norm  have hmeas :      AEStronglyMeasurable (fun u : ℝ => ‖𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi))‖) := by    have hcont : Continuous fun u : ℝ => 𝓕 (ψ : ℝ → ℂ) u := by      simpa using! continuous_FourierIntegral (ψ : W21)    have hcont_scaled : Continuous fun u : ℝ => 𝓕 (ψ : ℝ → ℂ) (u / (2 * Real.pi)) :=      hcont.comp (by continuity)    exact hcont_scaled.aestronglyMeasurable.norm  exact hmaj_int_norm.mono' hmeas hle_norm