internlm/Lean-Github huggingface dataset:
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
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)
Tactic:
. rcases this with ⟨h_center, h_sides⟩
  simp [Metric.tendsto_atTop] at h_sides
  specialize h_sides (ε/2) (half_pos hε)
  rcases h_center with ⟨N_center, h_center⟩
  rcases h_sides with ⟨N_sides, h_sides⟩
  exists max N_center N_sides
  intro n hn
  specialize h_center n (le_of_max_le_left hn)
  specialize h_sides n (le_of_max_le_right hn)
  rw [← add_halves' ε]
  refine lt_of_le_of_lt ?_ (add_lt_add h_center h_sides)
  clear h_center h_sides hn N_center N_sides  have hδδ : -δ ≤ δ := by simp [hδ.le]
  simp [integral_eq_add_Iic_Ioc_Ioi h_integrable hδδ]
  conv =>
    lhs; arg 1
    conv => lhs; rw [add_comm]
    rw [add_assoc]
  refine le_trans (abs_add _ _) ?_
  simp
  refine le_of_eq ?_
  congr
  simp [integral_union, Set.Iic_disjoint_Ioi hδδ, h_integrable.integrableOn]
Proof state after:
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)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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)
Tactic:
apply And.intro
Proof state after:
case this.left
φ : ℝ → ℝ
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

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left
φ : ℝ → ℝ
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

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. exists 1  intro n
  simp
  rw [integral_Ioc_eq_integral_Ioo]
  rw [← norm_eq_abs]
  refine lt_of_le_of_lt (@norm_integral_le_of_norm_le _ _ _ _ _ _ _
    (fun x => ε / 2 * DiracSeq n x) ?_ ?_) ?_
  . refine Integrable.integrableOn ?_
    exact Integrable.const_mul DiracSeq.integrable_pnat _
  . simp
    rw [eventually_inf_principal]
    refine ae_of_all _ ?_
    intro x hx
    simp [abs_of_nonneg, DiracSeq.nonneg_nat]
    refine mul_le_mul_of_nonneg_right ?_ (DiracSeq.nonneg_nat _)
    refine le_of_lt ?_
    apply hδε
    simp [abs_lt]
    exact hx
  . simp [integral_mul_left]
    rw [mul_lt_iff_lt_one_right (half_pos hε)]
    rw [← @DiracSeq.integral_pnat n]
    refine Ne.lt_of_le ?_ ?_
    . symm
      rw [← sub_ne_zero]
      rw [← integral_add_compl (by simp : MeasurableSet (Set.Ioo (-δ) δ)) DiracSeq.integrable_pnat]
      rw [@add_sub_cancel']
      simp
      rw [← ne_eq]
      refine DiracSeq.set_integral_ne_zero (by simp) ?_
      suffices : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
      . exact lt_of_lt_of_le (by simp) (measure_mono this)
      rw [Set.subset_def]
      simp
      intro x hx _
      exact hx
    . refine set_integral_le_integral (DiracSeq.integrable_pnat) ?_
      exact Filter.eventually_of_forall DiracSeq.nonneg_nat
Proof state after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. have hI₂ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Ioi a, (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
  . exact tendsto_integral_Ioi_bump_sub_const_mul ha hφ (φ 0)
  have hI₁ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Iic (-a), (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
  . exact tendsto_integral_Iic_bump_sub_const_mul ha hφ (φ 0)
  clear hδε hε ε  simp [integral_union, hδ.le, h_integrable.integrableOn]
  conv => rhs; rw [← add_zero 0]
  exact Tendsto.add (hI₁ hδ) (hI₂ hδ)
Proof state after:
no goals
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))
Tactic:
conv => arg 1; intro n; rw [← sub_add_cancel (∫ x, _) (φ 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) - φ 0 + φ 0) 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) - φ 0 + φ 0) atTop (nhds (φ 0))
Tactic:
conv => arg 3; rw [← sub_add_cancel (φ 0) (φ 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) - φ 0 + φ 0) atTop (nhds (φ 0 - φ 0 + φ 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) - φ 0 + φ 0) atTop (nhds (φ 0 - φ 0 + φ 0))
Tactic:
refine Tendsto.add_const _ ?_
Proof state after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun k => (∫ (x : ℝ), φ x * DiracSeq (↑↑k) x) - φ 0) atTop (nhds (φ 0 - φ 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 k => (∫ (x : ℝ), φ x * DiracSeq (↑↑k) x) - φ 0) atTop (nhds (φ 0 - φ 0))
Tactic:
simp
Proof state after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun k => (∫ (x : ℝ), φ x * DiracSeq (↑↑k) x) - φ 0) 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 k => (∫ (x : ℝ), φ x * DiracSeq (↑↑k) x) - φ 0) atTop (nhds 0)
Tactic:
refine Filter.Tendsto.congr ?_ h_tendsto
Proof state after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ ∀ (x : ℕ+), ∫ (x_1 : ℝ), (φ x_1 - φ 0) * DiracSeq (↑↑x) x_1 = (∫ (x_1 : ℝ), φ x_1 * DiracSeq (↑↑x) x_1) - φ 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)
⊢ ∀ (x : ℕ+), ∫ (x_1 : ℝ), (φ x_1 - φ 0) * DiracSeq (↑↑x) x_1 = (∫ (x_1 : ℝ), φ x_1 * DiracSeq (↑↑x) x_1) - φ 0
Tactic:
intro n
Proof state after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 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)
n : ℕ+
⊢ ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
Tactic:
simp [sub_mul]
Proof state after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x - φ 0 * DiracSeq (↑↑n) x = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 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)
n : ℕ+
⊢ ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x - φ 0 * DiracSeq (↑↑n) x = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
Tactic:
rw [integral_sub]
Proof state after:
φ : ℝ → ℝ
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

case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x

case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x
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)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0

case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x

case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x
Tactic:
rotate_left
Proof state after:
case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x

case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x

φ : ℝ → ℝ
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
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x

case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x

φ : ℝ → ℝ
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
Tactic:
. exact IsBump.integrable_mul_continuous hφ DiracSeq.continuous
Proof state after:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x

φ : ℝ → ℝ
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
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x

φ : ℝ → ℝ
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
Tactic:
. refine Integrable.const_mul ?_ _
  exact DiracSeq.integrable (by simp)
Proof state after:
φ : ℝ → ℝ
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
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)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
Tactic:
simp [integral_mul_left, DiracSeq.integral]
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x
Tactic:
exact IsBump.integrable_mul_continuous hφ DiracSeq.continuous
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x
Tactic:
refine Integrable.const_mul ?_ _
Proof state after:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x
Tactic:
exact DiracSeq.integrable (by simp)
Proof state after:
no goals
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)
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
φ : ℝ → ℝ
hφ : IsBump φ
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
Proof state after:
no goals
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)
Tactic:
refine Continuous.tendsto' ?_ _ _ (by simp)
Proof state after:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Continuous fun x => |φ x - φ 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
⊢ Continuous fun x => |φ x - φ 0|
Tactic:
refine Continuous.abs ?_
Proof state after:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Continuous fun x => φ x - φ 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
⊢ Continuous fun x => φ x - φ 0
Tactic:
exact Continuous.sub hφ.continuous continuous_const
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ |φ 0 - φ 0| = 0
Tactic:
simp
Proof state after:
no goals
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
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| < ε
Tactic:
rcases this with ⟨h_center, h_sides⟩
Proof state after:
case h_tendsto.intro.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
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : 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| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto.intro.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
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : 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| < ε
Tactic:
simp [Metric.tendsto_atTop] at h_sides
Proof state after:
case h_tendsto.intro.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
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides :
  ∀ (ε : ℝ),
    0 < ε → ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto.intro.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
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides :
  ∀ (ε : ℝ),
    0 < ε → ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
specialize h_sides (ε/2) (half_pos hε)
Proof state after:
case h_tendsto.intro.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
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 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.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
rcases h_center with ⟨N_center, h_center⟩
Proof state after:
case h_tendsto.intro.intro.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
h_sides : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 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.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
h_sides : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
rcases h_sides with ⟨N_sides, h_sides⟩
Proof state after:
case h_tendsto.intro.intro.intro.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_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε