internlm/Lean-Github huggingface dataset:
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Ioo (-δ) δ),
    ‖(φ x - φ 0) * DiracSeq (↑↑n) x‖ ≤ (fun x => ε / 2 * DiracSeq (↑↑n) x) x

case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2
Tactic:
. 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
Proof state after:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2
Tactic:
. 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:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ Integrable fun x => ε / 2 * DiracSeq (↑↑n) x
Tactic:
exact Integrable.const_mul DiracSeq.integrable_pnat _
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Ioo (-δ) δ),
    ‖(φ x - φ 0) * DiracSeq (↑↑n) x‖ ≤ (fun x => ε / 2 * DiracSeq (↑↑n) x) x
Tactic:
simp
Proof state after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᶠ (x : ℝ) in Measure.ae volume ⊓ 𝓟 (Set.Ioo (-δ) δ), |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᶠ (x : ℝ) in Measure.ae volume ⊓ 𝓟 (Set.Ioo (-δ) δ), |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
Tactic:
rw [eventually_inf_principal]
Proof state after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ), x ∈ Set.Ioo (-δ) δ → |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ), x ∈ Set.Ioo (-δ) δ → |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
Tactic:
refine ae_of_all _ ?_
Proof state after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ a ∈ Set.Ioo (-δ) δ, |φ a - φ 0| * |DiracSeq (↑↑n) a| ≤ ε / 2 * DiracSeq (↑↑n) a
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ a ∈ Set.Ioo (-δ) δ, |φ a - φ 0| * |DiracSeq (↑↑n) a| ≤ ε / 2 * DiracSeq (↑↑n) a
Tactic:
intro x hx
Proof state after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
Tactic:
simp [abs_of_nonneg, DiracSeq.nonneg_nat]
Proof state after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| * DiracSeq (↑↑n) x ≤ ε / 2 * DiracSeq (↑↑n) x
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| * DiracSeq (↑↑n) x ≤ ε / 2 * DiracSeq (↑↑n) x
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (DiracSeq.nonneg_nat _)
Proof state after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| ≤ ε / 2
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| ≤ ε / 2
Tactic:
refine le_of_lt ?_
Proof state after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| < ε / 2
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| < ε / 2
Tactic:
apply hδε
Proof state after:
case this.left.refine_2.a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |x| < δ
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2.a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |x| < δ
Tactic:
simp [abs_lt]
Proof state after:
case this.left.refine_2.a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ -δ < x ∧ x < δ
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_2.a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ -δ < x ∧ x < δ
Tactic:
exact hx
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2
Tactic:
simp [integral_mul_left]
Proof state after:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ε / 2 * ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < ε / 2
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ε / 2 * ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < ε / 2
Tactic:
rw [mul_lt_iff_lt_one_right (half_pos hε)]
Proof state after:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < 1
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < 1
Tactic:
rw [← @DiracSeq.integral_pnat n]
Proof state after:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < ∫ (x : ℝ), DiracSeq (↑↑n) x
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
refine Ne.lt_of_le ?_ ?_
Proof state after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ ∫ (x : ℝ), DiracSeq (↑↑n) x

case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ ∫ (x : ℝ), DiracSeq (↑↑n) x

case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
. 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
Proof state after:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
. refine set_integral_le_integral (DiracSeq.integrable_pnat) ?_
  exact Filter.eventually_of_forall DiracSeq.nonneg_nat
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
symm
Proof state after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ), DiracSeq (↑↑n) x ≠ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ), DiracSeq (↑↑n) x ≠ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a
Tactic:
rw [← sub_ne_zero]
Proof state after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ (∫ (x : ℝ), DiracSeq (↑↑n) x) - ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ 0
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ (∫ (x : ℝ), DiracSeq (↑↑n) x) - ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ 0
Tactic:
rw [← integral_add_compl (by simp : MeasurableSet (Set.Ioo (-δ) δ)) DiracSeq.integrable_pnat]
Proof state after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) x ∂volume + ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume -
      ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠
    0
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) x ∂volume + ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume -
      ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠
    0
Tactic:
rw [@add_sub_cancel']
Proof state after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume ≠ 0
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume ≠ 0
Tactic:
simp
Proof state after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ¬∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume = 0
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ¬∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume = 0
Tactic:
rw [← ne_eq]
Proof state after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume ≠ 0
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume ≠ 0
Tactic:
refine DiracSeq.set_integral_ne_zero (by simp) ?_
Proof state after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ
Tactic:
suffices : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
Proof state after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
this : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ

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 : ℕ+
⊢ Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
this : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ

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 : ℕ+
⊢ Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
Tactic:
. exact lt_of_lt_of_le (by simp) (measure_mono this)
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 : ℕ+
⊢ Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
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 : ℕ+
⊢ Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
Tactic:
rw [Set.subset_def]
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 : ℕ+
⊢ ∀ x ∈ Set.Ici δ, x ∈ (Set.Ioo (-δ) δ)ᶜ
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 : ℕ+
⊢ ∀ x ∈ Set.Ici δ, x ∈ (Set.Ioo (-δ) δ)ᶜ
Tactic:
simp
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 : ℕ+
⊢ ∀ (x : ℝ), δ ≤ x → -δ < x → δ ≤ x
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 : ℕ+
⊢ ∀ (x : ℝ), δ ≤ x → -δ < x → δ ≤ x
Tactic:
intro x hx _
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 : ℕ+
x : ℝ
hx : δ ≤ x
a✝ : -δ < x
⊢ δ ≤ x
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 : ℕ+
x : ℝ
hx : δ ≤ x
a✝ : -δ < x
⊢ δ ≤ x
Tactic:
exact hx
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
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ MeasurableSet (Set.Ioo (-δ) δ)
Tactic:
simp
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
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
this : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ
Tactic:
exact lt_of_lt_of_le (by simp) (measure_mono this)
Proof state after:
no goals