norm_error_integral_le

lemma norm_error_integral_le    (ψ : ℝ → ℂ) (x K : ℝ)    (hGline_meas : Measurable (fun t : ℝ => G (1 + t * I)))    (hψ_meas : AEStronglyMeasurable ψ)    (hx : 0 < x)    (hK : ∀ t : ℝ, t ∈ Function.support ψ → ‖G (1 + t * Complex.I)‖ ≤ K)    (hψ : Integrable (fun t : ℝ => ‖ψ t‖) ) :    ‖∫ t : ℝ, (G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖      ≤ K * (∫ t : ℝ, ‖ψ t‖) := by  have h1 : ‖∫ t : ℝ, (G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖        ≤ ∫ t : ℝ, ‖(G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖ := by    simpa using (norm_integral_le_integral_norm        (f := fun t : ℝ => (G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))))  have hmeas_main : AEStronglyMeasurable        (fun t : ℝ => (G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))) := by    have hG' : AEMeasurable fun t : ℝ => G (1 + t * Complex.I) := hGline_meas.aemeasurable    have hψ_meas' : AEMeasurable ψ := hψ_meas.aemeasurable    have hx_ne : (x : ℂ) ≠ 0 := by exact_mod_cast (ne_of_gt hx)    haveI hx_ne' : NeZero (x : ℂ) := ⟨hx_ne⟩    have hxpow_meas : AEMeasurable fun t : ℝ => ((x : ℂ) ^ (t * Complex.I)) := by      have hcontℂ : Continuous fun z : ℂ => ((x : ℂ) ^ z) :=        continuous_const_cpow (z := (x : ℂ))      have hcont : Continuous fun t : ℝ => ((x : ℂ) ^ ((t : ℂ) * Complex.I)) :=        hcontℂ.comp (by          have h : Continuous fun t : ℝ => (t : ℂ) * Complex.I := by            simpa using! (continuous_ofReal.mul continuous_const)          simpa [mul_comm] using h)      exact hcont.measurable.aemeasurable    have hGψ_meas : AEMeasurable fun t : ℝ => (G (1 + t * Complex.I)) * (ψ t) := hG'.mul hψ_meas'    have htotal : AEMeasurable (fun t : ℝ =>            (G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))) :=      hGψ_meas.mul hxpow_meas    exact htotal.aestronglyMeasurable  have hpt : (fun t : ℝ =>          ‖(G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖)        ≤ᵐ[volume] (fun t : ℝ => K * ‖ψ t‖) := by    refine Eventually.of_forall ?_    intro t    exact norm_integrand_le_K_mul_norm_psi (hx := hx) (hK := hK) t  have hR : Integrable (fun t : ℝ => K * ‖ψ t‖) := hψ.const_mul K  have hL : Integrable (fun t : ℝ =>        ‖(G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖) := by      have hpt_norm :          (fun t : ℝ => ‖‖(G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖‖)            ≤ᵐ[volume] (fun t : ℝ => K * ‖ψ t‖) := hpt.mono (by          intro t ht          simpa [norm_mul, mul_comm, mul_left_comm, mul_assoc] using ht)      exact hR.mono' hmeas_main.norm hpt_norm  have h2 : (∫ t : ℝ, ‖(G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖)        ≤ ∫ t : ℝ, K * ‖ψ t‖ := integral_mono_ae (μ := (volume : Measure ℝ)) hL hR hpt  have h3 : (∫ t : ℝ, K * ‖ψ t‖) = K * (∫ t : ℝ, ‖ψ t‖) := by    simp [integral_const_mul]  calc    ‖∫ t : ℝ, (G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖        ≤ ∫ t : ℝ, ‖(G (1 + t * Complex.I)) * (ψ t) * ((x : ℂ) ^ (t * Complex.I))‖ := h1    _   ≤ ∫ t : ℝ, K * ‖ψ t‖ := h2    _   = K * (∫ t : ℝ, ‖ψ t‖) := h3