internlm/Lean-Github huggingface dataset:
Theorem: tendsto_zero_of_forall_abs_le
Proof state before:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
h : Tendsto g atTop (nhds 0)
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
simp [Metric.tendsto_atTop] at h
Proof state after:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
h : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Theorem: tendsto_zero_of_forall_abs_le
Proof state before:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
h : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
specialize h ε hε
Proof state after:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
h : ∃ N, ∀ (n : α), N ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Theorem: tendsto_zero_of_forall_abs_le
Proof state before:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
h : ∃ N, ∀ (n : α), N ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
rcases h with ⟨a, ha⟩
Proof state after:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Theorem: tendsto_zero_of_forall_abs_le
Proof state before:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
exists a
Proof state after:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
⊢ ∀ (n : α), a ≤ n → |f n| < ε
Theorem: tendsto_zero_of_forall_abs_le
Proof state before:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
⊢ ∀ (n : α), a ≤ n → |f n| < ε
Tactic:
intro x hx
Proof state after:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
x : α
hx : a ≤ x
⊢ |f x| < ε
Theorem: tendsto_zero_of_forall_abs_le
Proof state before:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
x : α
hx : a ≤ x
⊢ |f x| < ε
Tactic:
exact lt_of_le_of_lt (hfg x) (lt_of_abs_lt (ha x hx))
Proof state after:
no goals
Theorem: tendsto_coe_pnat_atTop
Proof state before:
⊢ Tendsto (fun n => ↑n) atTop atTop
Tactic:
rw [tendsto_atTop_atTop]
Proof state after:
⊢ ∀ (b : ℕ), ∃ i, ∀ (a : ℕ+), i ≤ a → b ≤ ↑a
Theorem: tendsto_coe_pnat_atTop
Proof state before:
⊢ ∀ (b : ℕ), ∃ i, ∀ (a : ℕ+), i ≤ a → b ≤ ↑a
Tactic:
intro a
Proof state after:
a : ℕ
⊢ ∃ i, ∀ (a_1 : ℕ+), i ≤ a_1 → a ≤ ↑a_1
Theorem: tendsto_coe_pnat_atTop
Proof state before:
a : ℕ
⊢ ∃ i, ∀ (a_1 : ℕ+), i ≤ a_1 → a ≤ ↑a_1
Tactic:
exists Nat.toPNat' a
Proof state after:
a : ℕ
⊢ ∀ (a_1 : ℕ+), Nat.toPNat' a ≤ a_1 → a ≤ ↑a_1
Theorem: tendsto_coe_pnat_atTop
Proof state before:
a : ℕ
⊢ ∀ (a_1 : ℕ+), Nat.toPNat' a ≤ a_1 → a ≤ ↑a_1
Tactic:
intro x hx
Proof state after:
a : ℕ
x : ℕ+
hx : Nat.toPNat' a ≤ x
⊢ a ≤ ↑x
Theorem: tendsto_coe_pnat_atTop
Proof state before:
a : ℕ
x : ℕ+
hx : Nat.toPNat' a ≤ x
⊢ a ≤ ↑x
Tactic:
exact Nat.le_of_pred_lt hx
Proof state after:
no goals
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∫ (x : ℝ) in s, DiracSeq b x ≠ 0
Tactic:
refine ne_of_gt ?_
Proof state after:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ∫ (x : ℝ) in s, DiracSeq b x
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ∫ (x : ℝ) in s, DiracSeq b x
Tactic:
rw [set_integral_pos_iff_support_of_nonneg_ae]
Proof state after:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume ((Function.support fun x => DiracSeq b x) ∩ s)

case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x

case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume ((Function.support fun x => DiracSeq b x) ∩ s)

case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x

case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Tactic:
. simp [DiracSeq.support hb.ne']
  exact hs
Proof state after:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x

case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x

case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Tactic:
. refine Filter.eventually_of_forall ?_
  simp
  exact DiracSeq.nonneg hb.le
Proof state after:
case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Tactic:
. exact Integrable.integrableOn (DiracSeq.integrable hb)
Proof state after:
no goals
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume ((Function.support fun x => DiracSeq b x) ∩ s)
Tactic:
simp [DiracSeq.support hb.ne']
Proof state after:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume s
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 < ↑↑volume s
Tactic:
exact hs
Proof state after:
no goals
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ 0 ≤ᵐ[Measure.restrict volume s] fun x => DiracSeq b x
Tactic:
refine Filter.eventually_of_forall ?_
Proof state after:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∀ (x : ℝ), 0 x ≤ (fun x => DiracSeq b x) x
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∀ (x : ℝ), 0 x ≤ (fun x => DiracSeq b x) x
Tactic:
simp
Proof state after:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∀ (x : ℝ), 0 ≤ DiracSeq b x
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
case hf
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ ∀ (x : ℝ), 0 ≤ DiracSeq b x
Tactic:
exact DiracSeq.nonneg hb.le
Proof state after:
no goals
Theorem: DiracSeq.set_integral_ne_zero
Proof state before:
case hfi
b : ℝ
hb : 0 < b
s : Set ℝ
hs : 0 < ↑↑volume s
⊢ IntegrableOn (fun x => DiracSeq b x) s
Tactic:
exact Integrable.integrableOn (DiracSeq.integrable hb)
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
have {n : ℕ+} : ∫ (x : ℝ) in Set.Ioi a, DiracSeq n x
  = (∫ (x : ℝ) in Set.Ioi 0, DiracSeq n x) - (∫ x in (0:ℝ)..a, DiracSeq n x)
Proof state after:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x

a : ℝ
ha : 0 < a
this :
  ∀ {n : ℕ+},
    ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
      (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x

a : ℝ
ha : 0 < a
this :
  ∀ {n : ℕ+},
    ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
      (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. rw [eq_sub_iff_add_eq']
  simp [intervalIntegral.integral_of_le ha.le]
  rw [← integral_union]
  . simp [Set.Ioc_union_Ioi_eq_Ioi ha.le]
  . simp [disjoint_iff]
  . exact measurableSet_Ioi
  . apply Integrable.integrableOn
    exact DiracSeq.integrable (by simp)
  . apply Integrable.integrableOn
    exact DiracSeq.integrable (by simp)
Proof state after:
a : ℝ
ha : 0 < a
this :
  ∀ {n : ℕ+},
    ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
      (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
a : ℝ
ha : 0 < a
this :
  ∀ {n : ℕ+},
    ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
      (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
simp [this]
Proof state after:
a : ℝ
ha : 0 < a
this :
  ∀ {n : ℕ+},
    ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
      (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
a : ℝ
ha : 0 < a
this :
  ∀ {n : ℕ+},
    ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
      (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
clear this
Proof state after:
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
conv => rhs; rw [← sub_self (1/2)]
Proof state after:
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) atTop
    (nhds (1 / 2 - 1 / 2))
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) atTop
    (nhds (1 / 2 - 1 / 2))
Tactic:
apply Tendsto.sub
Proof state after:
case hf
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in Set.Ioi 0, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))

case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in 0 ..a, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hf
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in Set.Ioi 0, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))

case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in 0 ..a, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))
Tactic:
. simp [DiracSeq.integral_Ioi]
Proof state after:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in 0 ..a, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in 0 ..a, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))
Tactic:
. conv => arg 1; intro b; arg 1; intro x; rw [DiracSeq.eq_comp_mul]
  simp
  simp [intervalIntegral.integral_comp_mul_left]
  rw [inv_eq_one_div, ← DiracSeq.integral_Ioi zero_lt_one]
  apply intervalIntegral_tendsto_integral_Ioi
  . apply Integrable.integrableOn
    exact DiracSeq.integrable zero_lt_one
  . exact Tendsto.atTop_mul_const ha tendsto_coe_coe_pnat_atTop
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x
Tactic:
rw [eq_sub_iff_add_eq']
Proof state after:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ (∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) + ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ (∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) + ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x
Tactic:
simp [intervalIntegral.integral_of_le ha.le]
Proof state after:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioc 0 a, DiracSeq (↑↑n) x ∂volume + ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioc 0 a, DiracSeq (↑↑n) x ∂volume + ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x
Tactic:
rw [← integral_union]
Proof state after:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioc 0 a ∪ Set.Ioi a, DiracSeq (↑↑n) x ∂volume = ∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x

case this.hst
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Disjoint (Set.Ioc 0 a) (Set.Ioi a)

case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)

case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioc 0 a ∪ Set.Ioi a, DiracSeq (↑↑n) x ∂volume = ∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x

case this.hst
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Disjoint (Set.Ioc 0 a) (Set.Ioi a)

case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)

case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Tactic:
. simp [Set.Ioc_union_Ioi_eq_Ioi ha.le]
Proof state after:
case this.hst
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Disjoint (Set.Ioc 0 a) (Set.Ioi a)

case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)

case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.hst
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Disjoint (Set.Ioc 0 a) (Set.Ioi a)

case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)

case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Tactic:
. simp [disjoint_iff]
Proof state after:
case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)

case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)

case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Tactic:
. exact measurableSet_Ioi
Proof state after:
case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Tactic:
. apply Integrable.integrableOn
  exact DiracSeq.integrable (by simp)
Proof state after:
case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Tactic:
. apply Integrable.integrableOn
  exact DiracSeq.integrable (by simp)
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioc 0 a ∪ Set.Ioi a, DiracSeq (↑↑n) x ∂volume = ∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x
Tactic:
simp [Set.Ioc_union_Ioi_eq_Ioi ha.le]
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.hst
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Disjoint (Set.Ioc 0 a) (Set.Ioi a)
Tactic:
simp [disjoint_iff]
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)
Tactic:
exact measurableSet_Ioi
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)
Tactic:
apply Integrable.integrableOn
Proof state after:
case this.hfs.h
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.hfs.h
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x
Tactic:
exact DiracSeq.integrable (by simp)
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
a : ℝ
ha : 0 < a
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Tactic:
apply Integrable.integrableOn
Proof state after:
case this.hft.h
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case this.hft.h
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x
Tactic:
exact DiracSeq.integrable (by simp)
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hf
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in Set.Ioi 0, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))
Tactic:
simp [DiracSeq.integral_Ioi]
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in 0 ..a, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))
Tactic:
conv => arg 1; intro b; arg 1; intro x; rw [DiracSeq.eq_comp_mul]
Proof state after:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..a, ↑↑b * DiracSeq 1 (↑↑b * x)) atTop (nhds (1 / 2))
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..a, ↑↑b * DiracSeq 1 (↑↑b * x)) atTop (nhds (1 / 2))
Tactic:
simp
Proof state after:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ↑↑b * ∫ (x : ℝ) in 0 ..a, DiracSeq 1 (↑↑b * x)) atTop (nhds 2⁻¹)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ↑↑b * ∫ (x : ℝ) in 0 ..a, DiracSeq 1 (↑↑b * x)) atTop (nhds 2⁻¹)
Tactic:
simp [intervalIntegral.integral_comp_mul_left]
Proof state after:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..↑↑b * a, DiracSeq 1 x) atTop (nhds 2⁻¹)
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..↑↑b * a, DiracSeq 1 x) atTop (nhds 2⁻¹)
Tactic:
rw [inv_eq_one_div, ← DiracSeq.integral_Ioi zero_lt_one]
Proof state after:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..↑↑b * a, DiracSeq 1 x) atTop (nhds (∫ (x : ℝ) in Set.Ioi 0, DiracSeq 1 x))
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..↑↑b * a, DiracSeq 1 x) atTop (nhds (∫ (x : ℝ) in Set.Ioi 0, DiracSeq 1 x))
Tactic:
apply intervalIntegral_tendsto_integral_Ioi
Proof state after:
case hg.hfi
a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => DiracSeq 1 x) (Set.Ioi 0)

case hg.hb
a : ℝ
ha : 0 < a
⊢ Tendsto (fun i => ↑↑i * a) atTop atTop
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg.hfi
a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => DiracSeq 1 x) (Set.Ioi 0)

case hg.hb
a : ℝ
ha : 0 < a
⊢ Tendsto (fun i => ↑↑i * a) atTop atTop
Tactic:
. apply Integrable.integrableOn
  exact DiracSeq.integrable zero_lt_one
Proof state after:
case hg.hb
a : ℝ
ha : 0 < a
⊢ Tendsto (fun i => ↑↑i * a) atTop atTop
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg.hb
a : ℝ
ha : 0 < a
⊢ Tendsto (fun i => ↑↑i * a) atTop atTop
Tactic:
. exact Tendsto.atTop_mul_const ha tendsto_coe_coe_pnat_atTop
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg.hfi
a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => DiracSeq 1 x) (Set.Ioi 0)
Tactic:
apply Integrable.integrableOn
Proof state after:
case hg.hfi.h
a : ℝ
ha : 0 < a
⊢ Integrable fun x => DiracSeq 1 x
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg.hfi.h
a : ℝ
ha : 0 < a
⊢ Integrable fun x => DiracSeq 1 x
Tactic:
exact DiracSeq.integrable zero_lt_one
Proof state after:
no goals
Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero
Proof state before:
case hg.hb
a : ℝ
ha : 0 < a
⊢ Tendsto (fun i => ↑↑i * a) atTop atTop
Tactic:
exact Tendsto.atTop_mul_const ha tendsto_coe_coe_pnat_atTop
Proof state after:
no goals
Theorem: bounded_bump_sub_const
Proof state before:
φ : ℝ → ℝ
hφ : IsBump φ
y : ℝ
⊢ ∃ M, ∀ (x : ℝ), ‖φ x - y‖ ≤ M
Tactic:
rcases hφ.bounded with ⟨C, hC⟩
Proof state after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∃ M, ∀ (x : ℝ), ‖φ x - y‖ ≤ M
Theorem: bounded_bump_sub_const
Proof state before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∃ M, ∀ (x : ℝ), ‖φ x - y‖ ≤ M
Tactic:
exists C + ‖y‖
Proof state after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∀ (x : ℝ), ‖φ x - y‖ ≤ C + ‖y‖
Theorem: bounded_bump_sub_const
Proof state before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∀ (x : ℝ), ‖φ x - y‖ ≤ C + ‖y‖
Tactic:
intro x
Proof state after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ ‖φ x - y‖ ≤ C + ‖y‖
Theorem: bounded_bump_sub_const
Proof state before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ ‖φ x - y‖ ≤ C + ‖y‖
Tactic:
refine le_trans (norm_sub_le _ _) ?_
Proof state after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ ‖φ x‖ + ‖y‖ ≤ C + ‖y‖
Theorem: bounded_bump_sub_const
Proof state before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ ‖φ x‖ + ‖y‖ ≤ C + ‖y‖
Tactic:
simp
Proof state after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ |φ x| ≤ C
Theorem: bounded_bump_sub_const
Proof state before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ |φ x| ≤ C
Tactic:
exact hC x
Proof state after:
no goals
Theorem: integrable_bump_sub_const_mul_diracSeq
Proof state before:
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Integrable fun x => (φ x - y) * DiracSeq b x
Tactic:
refine Integrable.bdd_mul ?_ ?_ ?_
Proof state after:
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