norm_mul_integral_Ici_le_integral_norm

lemma norm_mul_integral_Ici_le_integral_norm    (A : ℂ) (F : ℝ → ℂ) (a : ℝ)    (hF : IntegrableOn F (Set.Ici a))    (hnorm : Integrable (fun u : ℝ => ‖F u‖)) :    ‖A * (∫ u in Set.Ici a, F u)‖ ≤ ‖A‖ * (∫ u : ℝ, ‖F u‖) := by  have hmul : ‖A * (∫ u in Set.Ici a, F u)‖ = ‖A‖ * ‖∫ u in Set.Ici a, F u‖ := by    simp  have hnormI :      ‖∫ u in Set.Ici a, F u‖ ≤ ∫ u in Set.Ici a, ‖F u‖ := by    have _ : Integrable F (Measure.restrict volume (Set.Ici a)) := hF    have h :        ‖∫ u, F u ∂Measure.restrict volume (Set.Ici a)‖          ≤ ∫ u, ‖F u‖ ∂Measure.restrict volume (Set.Ici a) :=      norm_integral_le_integral_norm (μ := Measure.restrict volume (Set.Ici a)) (f := F)    simpa using h   have hdom :      (∫ u in Set.Ici a, ‖F u‖) ≤ ∫ u : ℝ, ‖F u‖ := by    have hEq :        (∫ u in Set.Ici a, ‖F u‖) =          ∫ u : ℝ, Set.indicator (Set.Ici a) (fun u => ‖F u‖) u := by      have h := (integral_indicator (μ := (volume : Measure ℝ))        (s := Set.Ici a) (f := fun u => ‖F u‖))      have h' := h measurableSet_Ici      simpa using h'.symm    have hind_int :        Integrable (Set.indicator (Set.Ici a) (fun u => ‖F u‖)) :=      hnorm.indicator measurableSet_Ici    have hpoint :        Set.indicator (Set.Ici a) (fun u => ‖F u‖)            ≤ᵐ[volume] (fun u : ℝ => ‖F u‖) := by      filter_upwards with u      by_cases hu : u ∈ Set.Ici a      · simp [Set.indicator_of_mem hu]      · simp [Set.indicator_of_notMem hu]    have hmono :=        integral_mono_ae (μ := (volume : Measure ℝ))          hind_int hnorm hpoint    simpa [hEq] using hmono   calc    ‖A * (∫ u in Set.Ici a, F u)‖        = ‖A‖ * ‖∫ u in Set.Ici a, F u‖ := hmul    _   ≤ ‖A‖ * (∫ u in Set.Ici a, ‖F u‖) :=      mul_le_mul_of_nonneg_left hnormI (by simp)    _   ≤ ‖A‖ * (∫ u : ℝ, ‖F u‖) :=      mul_le_mul_of_nonneg_left hdom (by simp)