exact Integrable.const_mul (DiracSeq.integrable (by simp)) _
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
no goals