Theorem: tendsto_integral_Ioi_bump_sub_const_mul (ForML/Dirac.lean)

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:
rcases bounded_bump_sub_const hφ y with ⟨M, hM⟩
State after:
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
suffices (n : ℕ+) : |∫ x in Set.Ioi a, (φ x - y) * DiracSeq n x| ≤ M * ∫ x in Set.Ioi a, DiracSeq n x
State after:
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
this : ∀ (n : ℕ+), |∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x) atTop (nhds 0)

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| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x

State before:
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
this : ∀ (n : ℕ+), |∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x) atTop (nhds 0)

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| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
Tactic:
. apply tendsto_zero_of_forall_abs_le this
  conv => arg 3; rw [← mul_zero M]
  exact Tendsto.const_mul _ (DiracSeq.tendsto_setIntegral_Ioi_zero ha)
State after:
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| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x

State before:
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| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
Tactic:
rw [← norm_eq_abs]
State after:
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‖ ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x

State before:
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‖ ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
Tactic:
rw [← integral_mul_left]
State after:
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

State before:
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
Tactic:
refine norm_integral_le_of_norm_le ?_ ?_
State after:
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

State before:
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
Tactic:
. refine Integrable.integrableOn ?_
  exact Integrable.const_mul (DiracSeq.integrable (by simp)) _
State after:
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

State before:
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
Tactic:
. refine Filter.eventually_of_forall ?_
  intro x
  simp
  rw [abs_of_nonneg (DiracSeq.nonneg_nat _)]
  refine mul_le_mul_of_nonneg_right (hM x) (DiracSeq.nonneg_nat x)
State after:
no goals

State before:
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
this : ∀ (n : ℕ+), |∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
apply tendsto_zero_of_forall_abs_le this
State after:
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
this : ∀ (n : ℕ+), |∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
⊢ Tendsto (fun x => M * ∫ (x_1 : ℝ) in Set.Ioi a, DiracSeq (↑↑x) x_1) atTop (nhds 0)

State before:
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
this : ∀ (n : ℕ+), |∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
⊢ Tendsto (fun x => M * ∫ (x_1 : ℝ) in Set.Ioi a, DiracSeq (↑↑x) x_1) atTop (nhds 0)
Tactic:
conv => arg 3; rw [← mul_zero M]
State after:
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
this : ∀ (n : ℕ+), |∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
⊢ Tendsto (fun x => M * ∫ (x_1 : ℝ) in Set.Ioi a, DiracSeq (↑↑x) x_1) atTop (nhds (M * 0))

State before:
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
this : ∀ (n : ℕ+), |∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
⊢ Tendsto (fun x => M * ∫ (x_1 : ℝ) in Set.Ioi a, DiracSeq (↑↑x) x_1) atTop (nhds (M * 0))
Tactic:
exact Tendsto.const_mul _ (DiracSeq.tendsto_setIntegral_Ioi_zero ha)
State after:
no goals

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

State before:
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
State after:
no goals

State before:
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
Tactic:
refine Filter.eventually_of_forall ?_
State after:
case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
⊢ ∀ (x : ℝ), ‖(φ x - y) * DiracSeq (↑↑n) x‖ ≤ M * DiracSeq (↑↑n) x

State before:
case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
⊢ ∀ (x : ℝ), ‖(φ x - y) * DiracSeq (↑↑n) x‖ ≤ M * DiracSeq (↑↑n) x
Tactic:
intro x
State after:
case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
x : ℝ
⊢ ‖(φ x - y) * DiracSeq (↑↑n) x‖ ≤ M * DiracSeq (↑↑n) x

State before:
case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
x : ℝ
⊢ ‖(φ x - y) * DiracSeq (↑↑n) x‖ ≤ M * DiracSeq (↑↑n) x
Tactic:
simp
State after:
case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
x : ℝ
⊢ |φ x - y| * |DiracSeq (↑↑n) x| ≤ M * DiracSeq (↑↑n) x

State before:
case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
x : ℝ
⊢ |φ x - y| * |DiracSeq (↑↑n) x| ≤ M * DiracSeq (↑↑n) x
Tactic:
rw [abs_of_nonneg (DiracSeq.nonneg_nat _)]
State after:
case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
x : ℝ
⊢ |φ x - y| * DiracSeq (↑↑n) x ≤ M * DiracSeq (↑↑n) x

State before:
case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
x : ℝ
⊢ |φ x - y| * DiracSeq (↑↑n) x ≤ M * DiracSeq (↑↑n) x
Tactic:
refine mul_le_mul_of_nonneg_right (hM x) (DiracSeq.nonneg_nat x)
State after:
no goals