internlm/Lean-Github huggingface dataset:
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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| < ε
Tactic:
exists max N_center N_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 : ℕ+), max N_center N_sides ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 : ℕ+), max N_center N_sides ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
intro n hn
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 : ℕ+
hn : max N_center N_sides ≤ n
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 : ℕ+
hn : max N_center N_sides ≤ n
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
specialize h_center n (le_of_max_le_left hn)
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 N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
specialize h_sides n (le_of_max_le_right hn)
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 N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
rw [← add_halves' ε]
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 N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2 + ε / 2
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2 + ε / 2
Tactic:
refine lt_of_le_of_lt ?_ (add_lt_add h_center 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 N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
clear h_center h_sides hn N_center N_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 : ℕ+
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 : ℕ+
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
have hδδ : -δ ≤ δ := by simp [hδ.le]
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
simp [integral_eq_add_Iic_Ioc_Ioi h_integrable hδδ]
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |((∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |((∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
conv =>
  lhs; arg 1
  conv => lhs; rw [add_comm]
  rw [add_assoc]
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ((∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ((∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
refine le_trans (abs_add _ _) ?_
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
simp
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
refine le_of_eq ?_
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| =
    |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
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 : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| =
    |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
congr
Proof state after:
case h_tendsto.intro.intro.intro.intro.intro.e_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 : ℕ+
hδδ : -δ ≤ δ
⊢ (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) + ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case h_tendsto.intro.intro.intro.intro.intro.e_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 : ℕ+
hδδ : -δ ≤ δ
⊢ (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) + ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x
Tactic:
simp [integral_union, Set.Iic_disjoint_Ioi hδδ, h_integrable.integrableOn]
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 : ℕ+
⊢ -δ ≤ δ
Tactic:
simp [hδ.le]
Proof state after:
no goals
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
Tactic:
exists 1
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 : ℕ+), 1 ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
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 : ℕ+), 1 ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
Tactic:
intro n
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 : ℕ+
⊢ 1 ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
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 : ℕ+
⊢ 1 ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
Tactic:
simp
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 : ℕ+
⊢ |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
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 : ℕ+
⊢ |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
Tactic:
rw [integral_Ioc_eq_integral_Ioo]
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 : ℕ+
⊢ |∫ (t : ℝ) in Set.Ioo (-δ) δ, (φ t - φ 0) * DiracSeq (↑↑n) t| < ε / 2
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 : ℕ+
⊢ |∫ (t : ℝ) in Set.Ioo (-δ) δ, (φ t - φ 0) * DiracSeq (↑↑n) t| < ε / 2
Tactic:
rw [← norm_eq_abs]
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 : ℕ+
⊢ ‖∫ (t : ℝ) in Set.Ioo (-δ) δ, (φ t - φ 0) * DiracSeq (↑↑n) t‖ < ε / 2
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 : ℕ+
⊢ ‖∫ (t : ℝ) in Set.Ioo (-δ) δ, (φ t - φ 0) * DiracSeq (↑↑n) t‖ < ε / 2
Tactic:
refine lt_of_le_of_lt (@norm_integral_le_of_norm_le _ _ _ _ _ _ _
  (fun x => ε / 2 * DiracSeq n x) ?_ ?_) ?_
Proof state after:
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

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

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:
. refine Integrable.integrableOn ?_
  exact Integrable.const_mul DiracSeq.integrable_pnat _
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 : ℝ) ∂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