internlm/Lean-Github huggingface dataset:
Theorem: DiracSeq.expNegSq
Proof state before:
x : ℝ
⊢ sqrt π * ((sqrt π)⁻¹ * rexp (-x ^ 2)) = rexp (-x ^ 2)
Tactic:
rw [← mul_assoc]
Proof state after:
x : ℝ
⊢ sqrt π * (sqrt π)⁻¹ * rexp (-x ^ 2) = rexp (-x ^ 2)
Theorem: DiracSeq.expNegSq
Proof state before:
x : ℝ
⊢ sqrt π * (sqrt π)⁻¹ * rexp (-x ^ 2) = rexp (-x ^ 2)
Tactic:
rw [mul_inv_cancel sqrt_pi_pos.ne']
Proof state after:
x : ℝ
⊢ 1 * rexp (-x ^ 2) = rexp (-x ^ 2)
Theorem: DiracSeq.expNegSq
Proof state before:
x : ℝ
⊢ 1 * rexp (-x ^ 2) = rexp (-x ^ 2)
Tactic:
simp
Proof state after:
no goals
Theorem: DiracSeq.rpow_def
Proof state before:
b x : ℝ
⊢ DiracSeq b x = b / sqrt π * rexp (-rpow (b * x) 2)
Tactic:
simp [DiracSeq]
Proof state after:
no goals
Theorem: DiracSeq.npow_one
Proof state before:
x : ℝ
⊢ DiracSeq 1 x = (sqrt π)⁻¹ * rexp (-x ^ 2)
Tactic:
simp [DiracSeq]
Proof state after:
no goals
Theorem: DiracSeq.continuous
Proof state before:
b : ℝ
⊢ Continuous (DiracSeq b)
Tactic:
refine Continuous.mul continuous_const ?_
Proof state after:
b : ℝ
⊢ Continuous fun x => rexp (-(b * x) ^ 2)
Theorem: DiracSeq.continuous
Proof state before:
b : ℝ
⊢ Continuous fun x => rexp (-(b * x) ^ 2)
Tactic:
refine Continuous.exp ?_
Proof state after:
b : ℝ
⊢ Continuous fun x => -(b * x) ^ 2
Theorem: DiracSeq.continuous
Proof state before:
b : ℝ
⊢ Continuous fun x => -(b * x) ^ 2
Tactic:
refine Continuous.neg ?_
Proof state after:
b : ℝ
⊢ Continuous fun x => (b * x) ^ 2
Theorem: DiracSeq.continuous
Proof state before:
b : ℝ
⊢ Continuous fun x => (b * x) ^ 2
Tactic:
refine Continuous.pow ?_ 2
Proof state after:
b : ℝ
⊢ Continuous fun x => b * x
Theorem: DiracSeq.continuous
Proof state before:
b : ℝ
⊢ Continuous fun x => b * x
Tactic:
refine Continuous.mul continuous_const continuous_id
Proof state after:
no goals
Theorem: DiracSeq.nonneg
Proof state before:
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ DiracSeq b x
Tactic:
simp [DiracSeq]
Proof state after:
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π * rexp (-(b * x) ^ 2)
Theorem: DiracSeq.nonneg
Proof state before:
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π * rexp (-(b * x) ^ 2)
Tactic:
refine mul_nonneg ?_ ?_
Proof state after:
case refine_1
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π

case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)
Theorem: DiracSeq.nonneg
Proof state before:
case refine_1
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π

case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)
Tactic:
. exact div_nonneg hb (sqrt_nonneg π)
Proof state after:
case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)
Theorem: DiracSeq.nonneg
Proof state before:
case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)
Tactic:
. exact le_of_lt (exp_pos _)
Proof state after:
no goals
Theorem: DiracSeq.nonneg
Proof state before:
case refine_1
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ b / sqrt π
Tactic:
exact div_nonneg hb (sqrt_nonneg π)
Proof state after:
no goals
Theorem: DiracSeq.nonneg
Proof state before:
case refine_2
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ rexp (-(b * x) ^ 2)
Tactic:
exact le_of_lt (exp_pos _)
Proof state after:
no goals
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), DiracSeq b x = 1
Tactic:
simp [DiracSeq]
Proof state after:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), b / sqrt π * rexp (-(b * x) ^ 2) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), b / sqrt π * rexp (-(b * x) ^ 2) = 1
Tactic:
simp [integral_mul_left]
Proof state after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b * a) ^ 2) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b * a) ^ 2) = 1
Tactic:
simp [mul_pow]
Proof state after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
Tactic:
have h := integral_gaussian
Proof state after:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-b * x ^ 2) = sqrt (π / b)
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-b * x ^ 2) = sqrt (π / b)
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
Tactic:
simp at h
Proof state after:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-(b * x ^ 2)) = sqrt (π / b)
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-(b * x ^ 2)) = sqrt (π / b)
⊢ b / sqrt π * ∫ (a : ℝ), rexp (-(b ^ 2 * a ^ 2)) = 1
Tactic:
simp [h]
Proof state after:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-(b * x ^ 2)) = sqrt (π / b)
⊢ b / sqrt π * sqrt (π / b ^ 2) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
h : ∀ (b : ℝ), ∫ (x : ℝ), rexp (-(b * x ^ 2)) = sqrt (π / b)
⊢ b / sqrt π * sqrt (π / b ^ 2) = 1
Tactic:
clear h
Proof state after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * sqrt (π / b ^ 2) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * sqrt (π / b ^ 2) = 1
Tactic:
rw [sqrt_div pi_pos.le]
Proof state after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * (sqrt π / sqrt (b ^ 2)) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * (sqrt π / sqrt (b ^ 2)) = 1
Tactic:
rw [sqrt_sq hb.le]
Proof state after:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * (sqrt π / b) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ b / sqrt π * (sqrt π / b) = 1
Tactic:
rw [div_mul_div_comm]
Proof state after:
b : ℝ
hb : 0 < b
⊢ b * sqrt π / (sqrt π * b) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ b * sqrt π / (sqrt π * b) = 1
Tactic:
rw [mul_comm]
Proof state after:
b : ℝ
hb : 0 < b
⊢ sqrt π * b / (sqrt π * b) = 1
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ sqrt π * b / (sqrt π * b) = 1
Tactic:
rw [div_self]
Proof state after:
b : ℝ
hb : 0 < b
⊢ sqrt π * b ≠ 0
Theorem: DiracSeq.integral
Proof state before:
b : ℝ
hb : 0 < b
⊢ sqrt π * b ≠ 0
Tactic:
apply ne_of_gt
Proof state after:
case h
b : ℝ
hb : 0 < b
⊢ 0 < sqrt π * b
Theorem: DiracSeq.integral
Proof state before:
case h
b : ℝ
hb : 0 < b
⊢ 0 < sqrt π * b
Tactic:
exact mul_pos sqrt_pi_pos hb
Proof state after:
no goals
Theorem: DiracSeq.integral_pnat
Proof state before:
b : ℕ+
⊢ 0 < ↑↑b
Tactic:
simp
Proof state after:
no goals
Theorem: DiracSeq.integrable_pnat
Proof state before:
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
Proof state after:
no goals
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ), f x
Tactic:
have hs : MeasurableSet (Set.Ioi 0 : Set ℝ) := measurableSet_Ioi
Proof state after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ), f x
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ), f x
Tactic:
rw [← integral_add_compl hs hf]
Proof state after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in (Set.Ioi 0)ᶜ, f x ∂volume
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in (Set.Ioi 0)ᶜ, f x ∂volume
Tactic:
simp
Proof state after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Tactic:
simp only [@two_mul ℝ]
Proof state after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ (∫ (x : ℝ) in Set.Ioi 0, f x) + ∫ (x : ℝ) in Set.Ioi 0, f x =
    ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ (∫ (x : ℝ) in Set.Ioi 0, f x) + ∫ (x : ℝ) in Set.Ioi 0, f x =
    ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Tactic:
simp
Proof state after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Tactic:
have h0 : (0 : ℝ) = -0 := by norm_num
Proof state after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Tactic:
rw [h0]
Proof state after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi (-0), f x = ∫ (x : ℝ) in Set.Iic (-0), f x ∂volume
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi (-0), f x = ∫ (x : ℝ) in Set.Iic (-0), f x ∂volume
Tactic:
rw [← integral_comp_neg_Ioi]
Proof state after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi (-0), f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi (-0), f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)
Tactic:
simp
Proof state after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)
Tactic:
congr
Proof state after:
case e_f
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ (fun x => f x) = fun x => f (-x)
Theorem: integral_symm
Proof state before:
case e_f
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ (fun x => f x) = fun x => f (-x)
Tactic:
ext x
Proof state after:
case e_f.h
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
x : ℝ
⊢ f x = f (-x)
Theorem: integral_symm
Proof state before:
case e_f.h
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
x : ℝ
⊢ f x = f (-x)
Tactic:
rw [h_symm]
Proof state after:
no goals
Theorem: integral_symm
Proof state before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 0 = -0
Tactic:
norm_num
Proof state after:
no goals
Theorem: DiracSeq.symm
Proof state before:
b x : ℝ
⊢ DiracSeq b (-x) = DiracSeq b x
Tactic:
simp [DiracSeq]
Proof state after:
no goals
Theorem: DiracSeq.eq_comp_mul
Proof state before:
b x : ℝ
⊢ DiracSeq b x = b * DiracSeq 1 (b * x)
Tactic:
simp [DiracSeq]
Proof state after:
b x : ℝ
⊢ b / sqrt π * rexp (-(b * x) ^ 2) = b * ((sqrt π)⁻¹ * rexp (-(b * x) ^ 2))
Theorem: DiracSeq.eq_comp_mul
Proof state before:
b x : ℝ
⊢ b / sqrt π * rexp (-(b * x) ^ 2) = b * ((sqrt π)⁻¹ * rexp (-(b * x) ^ 2))
Tactic:
rw [← mul_assoc]
Proof state after:
b x : ℝ
⊢ b / sqrt π * rexp (-(b * x) ^ 2) = b * (sqrt π)⁻¹ * rexp (-(b * x) ^ 2)
Theorem: DiracSeq.eq_comp_mul
Proof state before:
b x : ℝ
⊢ b / sqrt π * rexp (-(b * x) ^ 2) = b * (sqrt π)⁻¹ * rexp (-(b * x) ^ 2)
Tactic:
rfl
Proof state after:
no goals
Theorem: DiracSeq.integral_Ioi
Proof state before:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x = 1 / 2
Tactic:
rw [eq_div_iff (by norm_num)]
Proof state after:
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x) * 2 = 1
Theorem: DiracSeq.integral_Ioi
Proof state before:
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x) * 2 = 1
Tactic:
rw [mul_comm]
Proof state after:
b : ℝ
hb : 0 < b
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x = 1
Theorem: DiracSeq.integral_Ioi
Proof state before:
b : ℝ
hb : 0 < b
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, DiracSeq b x = 1
Tactic:
rw [integral_symm (DiracSeq.integrable hb) (DiracSeq.symm b)]
Proof state after:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), DiracSeq b x = 1
Theorem: DiracSeq.integral_Ioi
Proof state before:
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), DiracSeq b x = 1
Tactic:
exact DiracSeq.integral hb
Proof state after:
no goals
Theorem: DiracSeq.integral_Ioi
Proof state before:
b : ℝ
hb : 0 < b
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: DiracSeq.intervalIntegral_comp_mul
Proof state before:
s a b : ℝ
⊢ ∫ (x : ℝ) in a..b, DiracSeq s x = ∫ (x : ℝ) in s * a..s * b, DiracSeq 1 x
Tactic:
simp [DiracSeq]
Proof state after:
s a b : ℝ
⊢ s / sqrt π * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)
Theorem: DiracSeq.intervalIntegral_comp_mul
Proof state before:
s a b : ℝ
⊢ s / sqrt π * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)
Tactic:
rw [div_eq_inv_mul]
Proof state after:
s a b : ℝ
⊢ (sqrt π)⁻¹ * s * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)
Theorem: DiracSeq.intervalIntegral_comp_mul
Proof state before:
s a b : ℝ
⊢ (sqrt π)⁻¹ * s * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)
Tactic:
rw [mul_assoc]
Proof state after:
s a b : ℝ
⊢ (sqrt π)⁻¹ * (s * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2)) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)
Theorem: DiracSeq.intervalIntegral_comp_mul
Proof state before:
s a b : ℝ
⊢ (sqrt π)⁻¹ * (s * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2)) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)
Tactic:
rw [← intervalIntegral.mul_integral_comp_mul_left]
Proof state after:
no goals
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in (fun u => k * u) '' s, DiracSeq 1 x
Tactic:
rw [@integral_image_eq_integral_abs_deriv_smul _ _ _ _ _ (fun _ => k : ℝ → ℝ) hs]
Proof state after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)

case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x

case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)

case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x

case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s
Tactic:
rotate_left
Proof state after:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x

case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x

case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
Tactic:
. intro x _
  simp [mul_comm k]
  exact HasDerivAt.hasDerivWithinAt (hasDerivAt_mul_const k)
Proof state after:
case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
Tactic:
. apply Function.Injective.injOn
  simp [Function.Injective]
  intro u v
  intro h
  cases h with
  | inl h => exact h
  | inr h => exfalso; exact hk.ne' h
Proof state after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
Tactic:
simp
Proof state after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| * DiracSeq 1 (k * x)
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| * DiracSeq 1 (k * x)
Tactic:
rw [abs_of_pos hk]
Proof state after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, k * DiracSeq 1 (k * x)
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, k * DiracSeq 1 (k * x)
Tactic:
simp [DiracSeq]
Proof state after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, k / sqrt π * rexp (-(k * x) ^ 2) = ∫ (x : ℝ) in s, k * ((sqrt π)⁻¹ * rexp (-(k * x) ^ 2))
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, k / sqrt π * rexp (-(k * x) ^ 2) = ∫ (x : ℝ) in s, k * ((sqrt π)⁻¹ * rexp (-(k * x) ^ 2))
Tactic:
simp [← mul_assoc]
Proof state after:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, k / sqrt π * rexp (-(k * x) ^ 2) = ∫ (x : ℝ) in s, k * (sqrt π)⁻¹ * rexp (-(k * x) ^ 2)
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, k / sqrt π * rexp (-(k * x) ^ 2) = ∫ (x : ℝ) in s, k * (sqrt π)⁻¹ * rexp (-(k * x) ^ 2)
Tactic:
rfl
Proof state after:
no goals
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x
Tactic:
intro x _
Proof state after:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : x ∈ s
⊢ HasDerivWithinAt (fun u => k * u) k s x
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : x ∈ s
⊢ HasDerivWithinAt (fun u => k * u) k s x
Tactic:
simp [mul_comm k]
Proof state after:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : x ∈ s
⊢ HasDerivWithinAt (fun u => u * k) k s x
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : x ∈ s
⊢ HasDerivWithinAt (fun u => u * k) k s x
Tactic:
exact HasDerivAt.hasDerivWithinAt (hasDerivAt_mul_const k)
Proof state after:
no goals
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s
Tactic:
apply Function.Injective.injOn
Proof state after:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Function.Injective fun u => k * u
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Function.Injective fun u => k * u
Tactic:
simp [Function.Injective]
Proof state after:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ ⦃a₁ a₂ : ℝ⦄, a₁ = a₂ ∨ k = 0 → a₁ = a₂
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ ⦃a₁ a₂ : ℝ⦄, a₁ = a₂ ∨ k = 0 → a₁ = a₂
Tactic:
intro u v
Proof state after:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
⊢ u = v ∨ k = 0 → u = v
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
⊢ u = v ∨ k = 0 → u = v
Tactic:
intro h
Proof state after:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : u = v ∨ k = 0
⊢ u = v
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : u = v ∨ k = 0
⊢ u = v
Tactic:
cases h with
| inl h => exact h
| inr h => exfalso; exact hk.ne' h
Proof state after:
no goals
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf.h.inl
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : u = v
⊢ u = v
Tactic:
exact h
Proof state after:
no goals
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf.h.inr
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : k = 0
⊢ u = v
Tactic:
exfalso
Proof state after:
case hf.h.inr
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : k = 0
⊢ False
Theorem: DiracSeq.setIntegral_comp_mul
Proof state before:
case hf.h.inr
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
u v : ℝ
h : k = 0
⊢ False
Tactic:
exact hk.ne' h
Proof state after:
no goals
Theorem: DiracSeq.support
Proof state before:
b : ℝ
hb : b ≠ 0
⊢ Function.support (DiracSeq b) = Set.univ
Tactic:
simp [DiracSeq.def]
Proof state after:
b : ℝ
hb : b ≠ 0
⊢ (((Function.support fun a => b) ∩ Function.support fun a => sqrt π) ∩ Function.support fun x => rexp (-(b * x) ^ 2)) =
    Set.univ
Theorem: DiracSeq.support
Proof state before:
b : ℝ
hb : b ≠ 0
⊢ (((Function.support fun a => b) ∩ Function.support fun a => sqrt π) ∩ Function.support fun x => rexp (-(b * x) ^ 2)) =
    Set.univ
Tactic:
ext x
Proof state after:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ (x ∈
      ((Function.support fun a => b) ∩ Function.support fun a => sqrt π) ∩
        Function.support fun x => rexp (-(b * x) ^ 2)) ↔
    x ∈ Set.univ
Theorem: DiracSeq.support
Proof state before:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ (x ∈
      ((Function.support fun a => b) ∩ Function.support fun a => sqrt π) ∩
        Function.support fun x => rexp (-(b * x) ^ 2)) ↔
    x ∈ Set.univ
Tactic:
simp [hb, sqrt_pi_pos.ne']
Proof state after:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ ¬rexp (-(b * x) ^ 2) = 0
Theorem: DiracSeq.support
Proof state before:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ ¬rexp (-(b * x) ^ 2) = 0
Tactic:
rw [← ne_eq]
Proof state after:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ rexp (-(b * x) ^ 2) ≠ 0
Theorem: DiracSeq.support
Proof state before:
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ rexp (-(b * x) ^ 2) ≠ 0
Tactic:
exact ne_of_gt (exp_pos _)
Proof state after:
no goals
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)
⊢ Tendsto f atTop (nhds 0)
Tactic:
simp [Metric.tendsto_atTop]
Proof state after:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
h : Tendsto g atTop (nhds 0)
⊢ ∀ (ε : ℝ), 0 < ε → ∃ 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 : Tendsto g atTop (nhds 0)
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
intro ε hε
Proof state after:
α : 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| < ε