internlm/Lean-Github huggingface dataset:
Theorem: integrable_bump_sub_const_mul_diracSeq
Proof state before:
case refine_1
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Integrable fun x => DiracSeq b x

case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume

case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Tactic:
. exact DiracSeq.integrable hb
Proof state after:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume

case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Theorem: integrable_bump_sub_const_mul_diracSeq
Proof state before:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume

case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Tactic:
. refine Continuous.aestronglyMeasurable ?_
  exact Continuous.sub hφ.continuous continuous_const
Proof state after:
case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Theorem: integrable_bump_sub_const_mul_diracSeq
Proof state before:
case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Tactic:
. exact bounded_bump_sub_const hφ y
Proof state after:
no goals
Theorem: integrable_bump_sub_const_mul_diracSeq
Proof state before:
case refine_1
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Integrable fun x => DiracSeq b x
Tactic:
exact DiracSeq.integrable hb
Proof state after:
no goals
Theorem: integrable_bump_sub_const_mul_diracSeq
Proof state before:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume
Tactic:
refine Continuous.aestronglyMeasurable ?_
Proof state after:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Continuous fun x => φ x - y
Theorem: integrable_bump_sub_const_mul_diracSeq
Proof state before:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Continuous fun x => φ x - y
Tactic:
exact Continuous.sub hφ.continuous continuous_const
Proof state after:
no goals
Theorem: integrable_bump_sub_const_mul_diracSeq
Proof state before:
case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Tactic:
exact bounded_bump_sub_const hφ y
Proof state after:
no goals
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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⟩
Proof 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)
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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)
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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]
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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]
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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 ?_ ?_
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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)) _
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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)
Proof state after:
no goals
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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
Proof 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)
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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]
Proof 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))
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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)
Proof state after:
no goals
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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)) _
Proof state after:
no goals
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof state before:
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
Proof state after:
no goals
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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 ?_
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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 _)]
Proof 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
Theorem: tendsto_integral_Ioi_bump_sub_const_mul
Proof 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)
Proof state after:
no goals
Theorem: tendsto_integral_Iic_bump_sub_const_mul
Proof 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]
Proof 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)
Theorem: tendsto_integral_Iic_bump_sub_const_mul
Proof 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]
Proof 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)
Theorem: tendsto_integral_Iic_bump_sub_const_mul
Proof 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
Proof state after:
no goals
Theorem: integral_eq_add_Iic_Ioc_Ioi
Proof state before:
f : ℝ → ℝ
hf : Integrable f
a b : ℝ
hab : a ≤ b
⊢ ∫ (x : ℝ), f x = ((∫ (x : ℝ) in Set.Iic a, f x) + ∫ (x : ℝ) in Set.Ioc a b, f x) + ∫ (x : ℝ) in Set.Ioi b, f x
Tactic:
simp [← integral_union, hab, Integrable.integrableOn, hf]
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) atTop (nhds (φ 0))
Tactic:
suffices h_tendsto : Tendsto (fun (n : ℕ+) => ∫ x, (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
Proof state after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) atTop (nhds (φ 0))

case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) atTop (nhds (φ 0))

case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. conv => arg 1; intro n; rw [← sub_add_cancel (∫ x, _) (φ 0)]
  conv => arg 3; rw [← sub_add_cancel (φ 0) (φ 0)]
  refine Tendsto.add_const _ ?_
  simp
  refine Filter.Tendsto.congr ?_ h_tendsto
  intro n
  simp [sub_mul]
  rw [integral_sub]
  rotate_left
  . exact IsBump.integrable_mul_continuous hφ DiracSeq.continuous
  . refine Integrable.const_mul ?_ _
    exact DiracSeq.integrable (by simp)
  simp [integral_mul_left, DiracSeq.integral]
Proof state after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
have h_integrable {n : ℕ+} := @integrable_bump_sub_const_mul_diracSeq _ hφ (φ 0) n (by simp)
Proof state after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
have hδ : Tendsto (fun (x : ℝ) => |φ x - φ 0|) (nhds 0) (nhds 0)
Proof state after:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)

case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)

case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. refine Continuous.tendsto' ?_ _ _ (by simp)
  refine Continuous.abs ?_
  exact Continuous.sub hφ.continuous continuous_const
Proof state after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
rw [Metric.tendsto_nhds_nhds] at hδ
Proof state after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, dist x 0 < δ → dist |φ x - φ 0| 0 < ε
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, dist x 0 < δ → dist |φ x - φ 0| 0 < ε
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
simp at hδ
Proof state after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
simp [Metric.tendsto_atTop]
Proof state after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
intro ε hε
Proof state after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
specialize hδ (ε/2) (half_pos hε)
Proof state after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
hδ : ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
hδ : ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
rcases hδ with ⟨δ, ⟨hδ, hδε⟩⟩
Proof state after:
case h_tendsto.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
suffices : (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ x in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε/2) ∧
    Tendsto (fun (n : ℕ+) => ∫ x in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
Proof state after:
case h_tendsto.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
this :
  (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2) ∧
    Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2) ∧
    Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)