refine norm_integral_le_of_norm_le ?_ ?_
case this
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
⊢ ‖∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x‖ ≤ ∫ (a : ℝ) in Set.Ioi a, M * DiracSeq (↑↑n) a
case this.refine_1
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
⊢ Integrable fun a => M * DiracSeq (↑↑n) a

case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Ioi a), ‖(φ x - y) * DiracSeq (↑↑n) x‖ ≤ M * DiracSeq (↑↑n) x