simp [integral_mul_left, DiracSeq.integral]
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
no goals