Complex.CartanBound.ae_restrict_norm_phi_le_of_forall_mem

lemma ae_restrict_norm_phi_le_of_forall_mem {A B : ℝ} (hAB : A ≤ B) {g : ℝ → ℝ}    (hg : ∀ t, 0 ≤ g t) (h : ∀ t ∈ Set.Icc A B, φ t ≤ g t) :    (fun t : ℝ => ‖φ t‖) ≤ᶠ[ae (volume.restrict (Set.uIoc A B))] fun t => ‖g t‖ := by  refine    MeasureTheory.ae_restrict_of_forall_mem (μ := (volume : MeasureTheory.Measure ℝ))    (s := Set.uIoc A B)      (by simpa using (measurableSet_uIoc : MeasurableSet (Set.uIoc A B))) ?_  intro t ht  have htIoc : t ∈ Set.Ioc A B := by    simpa [Set.uIoc_of_le hAB] using ht  have htIcc : t ∈ Set.Icc A B := ⟨le_of_lt htIoc.1, htIoc.2⟩  have hle : φ t ≤ g t := h t htIcc  have hφ0 : 0 ≤ φ t := φ_nonneg t  have hg0 : 0 ≤ g t := hg t  simpa [Real.norm_eq_abs, abs_of_nonneg hφ0, abs_of_nonneg hg0] using hle