Theorem: tendsto_integral_Iic_bump_sub_const_mul (ForML/Dirac.lean)

State before:
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y : ℝ
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - y) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
simp only [← integral_comp_neg_Ioi]
State after:
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y : ℝ
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ (-x) - y) * DiracSeq (↑↑n) (-x)) atTop (nhds 0)

State before:
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y : ℝ
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ (-x) - y) * DiracSeq (↑↑n) (-x)) atTop (nhds 0)
Tactic:
simp only [DiracSeq.symm]
State after:
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y : ℝ
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ (-x) - y) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y : ℝ
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ (-x) - y) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
exact tendsto_integral_Ioi_bump_sub_const_mul ha (IsBump.comp_neg hφ) y
State after:
no goals