Theorem: DiracSeq.tendsto_setIntegral_Ioi_zero (ForML/Dirac.lean)

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)
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)

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)
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)

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]
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)

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
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)

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)]
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))

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
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))

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]
State after:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in 0 ..a, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))

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
State after:
no goals

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']
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

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]
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

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]
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)

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]
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)

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]
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)

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
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)

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)
State after:
case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)

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)
State after:
no goals

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]
State after:
no goals

State before:
case this.hst
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Disjoint (Set.Ioc 0 a) (Set.Ioi a)
Tactic:
simp [disjoint_iff]
State after:
no goals

State before:
case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)
Tactic:
exact measurableSet_Ioi
State after:
no goals

State before:
case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)
Tactic:
apply Integrable.integrableOn
State after:
case this.hfs.h
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x

State before:
case this.hfs.h
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x
Tactic:
exact DiracSeq.integrable (by simp)
State after:
no goals

State before:
a : ℝ
ha : 0 < a
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
State after:
no goals

State before:
case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
Tactic:
apply Integrable.integrableOn
State after:
case this.hft.h
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x

State before:
case this.hft.h
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x
Tactic:
exact DiracSeq.integrable (by simp)
State after:
no goals

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]
State after:
no goals

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]
State after:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..a, ↑↑b * DiracSeq 1 (↑↑b * x)) atTop (nhds (1 / 2))

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
State after:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ↑↑b * ∫ (x : ℝ) in 0 ..a, DiracSeq 1 (↑↑b * x)) atTop (nhds 2⁻¹)

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]
State after:
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..↑↑b * a, DiracSeq 1 x) atTop (nhds 2⁻¹)

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]
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))

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
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

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
State after:
case hg.hb
a : ℝ
ha : 0 < a
⊢ Tendsto (fun i => ↑↑i * a) atTop atTop

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
State after:
no goals

State before:
case hg.hfi
a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => DiracSeq 1 x) (Set.Ioi 0)
Tactic:
apply Integrable.integrableOn
State after:
case hg.hfi.h
a : ℝ
ha : 0 < a
⊢ Integrable fun x => DiracSeq 1 x

State before:
case hg.hfi.h
a : ℝ
ha : 0 < a
⊢ Integrable fun x => DiracSeq 1 x
Tactic:
exact DiracSeq.integrable zero_lt_one
State after:
no goals

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
State after:
no goals