internlm/Lean-Github huggingface dataset:
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ EquivLike.coe xs.repr (A.transpose j) i = xs.repr (fun i => A i j * 1) i
Tactic:
simp_rw [mul_one]
Proof state after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ EquivLike.coe xs.repr (A.transpose j) i = xs.repr (fun i => A i j) i
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ EquivLike.coe xs.repr (A.transpose j) i = xs.repr (fun i => A i j) i
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
simp only [diagonal_mul, Function.comp]
Proof state after:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ ↑(as i) * xs.toBasis.toMatrix (⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ ↑(as i) * xs.toBasis.toMatrix (⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
erw [Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply,
  OrthonormalBasis.repr_reindex, Pi.basisFun_apply, LinearMap.coe_stdBasis,
  EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2,
  Equiv.symm_apply_apply, Equiv.apply_symm_apply]
Proof state after:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ ↑(as i) * EquivLike.coe xs.repr (Pi.single j 1) i =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) *
      xs.repr (fun a => Decidable.rec (fun h => (fun h => 0 a) h) (fun h => (fun h => ⋯ ▸ 1) h) (inst✝ a j)) i
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ ↑(as i) * EquivLike.coe xs.repr (Pi.single j 1) i =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) *
      xs.repr (fun a => Decidable.rec (fun h => (fun h => 0 a) h) (fun h => (fun h => ⋯ ▸ 1) h) (inst✝ a j)) i
Tactic:
congr
Proof state after:
case h.e'_3.e_a.e_a.e_a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ i = (Fintype.equivOfCardEq ⋯) ((Fintype.equivOfCardEq ⋯).symm i)
Theorem: Matrix.spectral_theorem
Proof state before:
case h.e'_3.e_a.e_a.e_a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ i = (Fintype.equivOfCardEq ⋯) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.det_eq_prod_eigenvalues
Proof state before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ A.det = ↑(∏ i : n, as i)
Tactic:
apply mul_left_cancel₀ (det_ne_zero_of_left_inverse
  (Basis.toMatrix_mul_toMatrix_flip (Pi.basisFun 𝕜 n) xs.toBasis))
Proof state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * A.det = (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ↑(∏ i : n, as i)
Theorem: Matrix.det_eq_prod_eigenvalues
Proof state before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * A.det = (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ↑(∏ i : n, as i)
Tactic:
rw [← det_mul, spectral_theorem xs as hxs, det_mul, mul_comm, det_diagonal]
Proof state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ∏ i : n, (RCLike.ofReal ∘ as) i =
    (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ↑(∏ i : n, as i)
Theorem: Matrix.det_eq_prod_eigenvalues
Proof state before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ∏ i : n, (RCLike.ofReal ∘ as) i =
    (xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)).det * ↑(∏ i : n, as i)
Tactic:
simp
Proof state after:
no goals
Theorem: VehicleSpeedSched.simp_vec_fraction
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
⊢ d i / (d i / s i) = s i
Tactic:
have h_di_pos := h_d_pos i
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 i < d i
⊢ d i / (d i / s i) = s i
Theorem: VehicleSpeedSched.simp_vec_fraction
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 i < d i
⊢ d i / (d i / s i) = s i
Tactic:
simp at h_di_pos
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
⊢ d i / (d i / s i) = s i
Theorem: VehicleSpeedSched.simp_vec_fraction
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
⊢ d i / (d i / s i) = s i
Tactic:
have h_di_nonzero : d i ≠ 0 := by linarith
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
h_di_nonzero : d i ≠ 0
⊢ d i / (d i / s i) = s i
Theorem: VehicleSpeedSched.simp_vec_fraction
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
h_di_nonzero : d i ≠ 0
⊢ d i / (d i / s i) = s i
Tactic:
rw [← div_mul, div_self h_di_nonzero, one_mul]
Proof state after:
no goals
Theorem: VehicleSpeedSched.simp_vec_fraction
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
h_d_pos : StrongLT 0 d
s : Fin n → ℝ
i : Fin n
h_di_pos : 0 < d i
⊢ d i ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: VehicleSpeedSched.fold_partial_sum
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
⊢ ∑ j ∈ [[0, i]], t j = Vec.cumsum t i
Tactic:
simp [Vec.cumsum]
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
⊢ ∑ j ∈ [[0, i]], t j = if h : 0 < n then ∑ j ∈ [[⟨0, h⟩, i]], t j else 0
Theorem: VehicleSpeedSched.fold_partial_sum
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
⊢ ∑ j ∈ [[0, i]], t j = if h : 0 < n then ∑ j ∈ [[⟨0, h⟩, i]], t j else 0
Tactic:
split_ifs
Proof state after:
case pos
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
h✝ : 0 < n
⊢ ∑ j ∈ [[0, i]], t j = ∑ j ∈ [[⟨0, h✝⟩, i]], t j

case neg
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
h✝ : ¬0 < n
⊢ ∑ j ∈ [[0, i]], t j = 0
Theorem: VehicleSpeedSched.fold_partial_sum
Proof state before:
case pos
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
h✝ : 0 < n
⊢ ∑ j ∈ [[0, i]], t j = ∑ j ∈ [[⟨0, h✝⟩, i]], t j
Tactic:
rfl
Proof state after:
no goals
Theorem: VehicleSpeedSched.fold_partial_sum
Proof state before:
case neg
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
hn : Fact (0 < n)
t : Fin n → ℝ
i : Fin n
h✝ : ¬0 < n
⊢ ∑ j ∈ [[0, i]], t j = 0
Tactic:
linarith [hn.out]
Proof state after:
no goals
Theorem: VehicleSpeedSched.nₚ_pos
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 < nₚ
Tactic:
unfold nₚ
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 < 10
Theorem: VehicleSpeedSched.nₚ_pos
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 < 10
Tactic:
norm_num
Proof state after:
no goals
Theorem: VehicleSpeedSched.dₚ_pos
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ StrongLT 0 dₚ
Tactic:
intro i
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i < dₚ i
Theorem: VehicleSpeedSched.dₚ_pos
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i < dₚ i
Tactic:
fin_cases i <;> (dsimp [dₚ]; norm_num)
Proof state after:
no goals
Theorem: VehicleSpeedSched.dₚ_pos
Proof state before:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ⟨9, ⋯⟩ < dₚ ⟨9, ⋯⟩
Tactic:
dsimp [dₚ]
Proof state after:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 < ![1.9501, 1.2311, 1.6068, 1.4860, 1.8913, 1.7621, 1.4565, 1.0185, 1.8214, 1.4447] ⟨9, ⋯⟩
Theorem: VehicleSpeedSched.dₚ_pos
Proof state before:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 < ![1.9501, 1.2311, 1.6068, 1.4860, 1.8913, 1.7621, 1.4565, 1.0185, 1.8214, 1.4447] ⟨9, ⋯⟩
Tactic:
norm_num
Proof state after:
no goals
Theorem: VehicleSpeedSched.sminₚ_pos
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ StrongLT 0 sminₚ
Tactic:
intro i
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i < sminₚ i
Theorem: VehicleSpeedSched.sminₚ_pos
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i < sminₚ i
Tactic:
fin_cases i <;> norm_num
Proof state after:
no goals
Theorem: VehicleSpeedSched.sminₚ_le_smaxₚ
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ sminₚ ≤ smaxₚ
Tactic:
intro i
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ sminₚ i ≤ smaxₚ i
Theorem: VehicleSpeedSched.sminₚ_le_smaxₚ
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ sminₚ i ≤ smaxₚ i
Tactic:
fin_cases i <;> (dsimp [sminₚ, smaxₚ]; norm_num)
Proof state after:
no goals
Theorem: VehicleSpeedSched.sminₚ_le_smaxₚ
Proof state before:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ sminₚ ⟨9, ⋯⟩ ≤ smaxₚ ⟨9, ⋯⟩
Tactic:
dsimp [sminₚ, smaxₚ]
Proof state after:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ ![0.7828, 0.6235, 0.7155, 0.5340, 0.6329, 0.4259, 0.7798, 0.9604, 0.7298, 0.8405] ⟨9, ⋯⟩ ≤
    ![1.9624, 1.6036, 1.6439, 1.5641, 1.7194, 1.9090, 1.3193, 1.3366, 1.9470, 2.8803] ⟨9, ⋯⟩
Theorem: VehicleSpeedSched.sminₚ_le_smaxₚ
Proof state before:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ ![0.7828, 0.6235, 0.7155, 0.5340, 0.6329, 0.4259, 0.7798, 0.9604, 0.7298, 0.8405] ⟨9, ⋯⟩ ≤
    ![1.9624, 1.6036, 1.6439, 1.5641, 1.7194, 1.9090, 1.3193, 1.3366, 1.9470, 2.8803] ⟨9, ⋯⟩
Tactic:
norm_num
Proof state after:
no goals
Theorem: VehicleSpeedSched.aₚ_nonneg
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ aₚ
Tactic:
unfold aₚ
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ 1
Theorem: VehicleSpeedSched.aₚ_nonneg
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: VehicleSpeedSched.aₚdₚ2_nonneg
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ aₚ • dₚ ^ 2
Tactic:
intros i
Proof state after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i ≤ (aₚ • dₚ ^ 2) i
Theorem: VehicleSpeedSched.aₚdₚ2_nonneg
Proof state before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i ≤ (aₚ • dₚ ^ 2) i
Tactic:
fin_cases i <;> (dsimp [aₚ, dₚ]; norm_num)
Proof state after:
no goals
Theorem: VehicleSpeedSched.aₚdₚ2_nonneg
Proof state before:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ⟨9, ⋯⟩ ≤ (aₚ • dₚ ^ 2) ⟨9, ⋯⟩
Tactic:
dsimp [aₚ, dₚ]
Proof state after:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ 1 * ![1.9501, 1.2311, 1.6068, 1.4860, 1.8913, 1.7621, 1.4565, 1.0185, 1.8214, 1.4447] ⟨9, ⋯⟩ ^ 2
Theorem: VehicleSpeedSched.aₚdₚ2_nonneg
Proof state before:
case tail.tail.tail.tail.tail.tail.tail.tail.tail.head
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ 1 * ![1.9501, 1.2311, 1.6068, 1.4860, 1.8913, 1.7621, 1.4565, 1.0185, 1.8214, 1.4447] ⟨9, ⋯⟩ ^ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: sum_primesBelow_eq_sum_range_indicator
Proof state before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n : ℕ
⊢ ∑ p ∈ n.primesBelow, f p = ∑ m ∈ Finset.range n, {p | p.Prime}.indicator f m
Tactic:
convert (Finset.sum_indicator_subset f Finset.mem_of_mem_filter).symm using 2 with _ _ m hm
Proof state after:
case h.e'_3.a
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
⊢ {p | p.Prime}.indicator f m = (↑(Finset.filter (fun p => p.Prime) (Finset.range n))).indicator f m
Theorem: sum_primesBelow_eq_sum_range_indicator
Proof state before:
case h.e'_3.a
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
⊢ {p | p.Prime}.indicator f m = (↑(Finset.filter (fun p => p.Prime) (Finset.range n))).indicator f m
Tactic:
simp only [Set.mem_setOf_eq, Finset.mem_range, Finset.coe_filter, not_and, Set.indicator_apply]
Proof state after:
case h.e'_3.a
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
⊢ (if m.Prime then f m else 0) = if m < n ∧ m.Prime then f m else 0
Theorem: sum_primesBelow_eq_sum_range_indicator
Proof state before:
case h.e'_3.a
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
⊢ (if m.Prime then f m else 0) = if m < n ∧ m.Prime then f m else 0
Tactic:
split_ifs with h₁ h₂ h₃
Proof state after:
case pos
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : m.Prime
h₂ : m < n ∧ m.Prime
⊢ f m = f m

case neg
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : m.Prime
h₂ : ¬(m < n ∧ m.Prime)
⊢ f m = 0

case pos
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : ¬m.Prime
h₃ : m < n ∧ m.Prime
⊢ 0 = f m

case neg
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : ¬m.Prime
h₃ : ¬(m < n ∧ m.Prime)
⊢ 0 = 0
Theorem: sum_primesBelow_eq_sum_range_indicator
Proof state before:
case pos
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : m.Prime
h₂ : m < n ∧ m.Prime
⊢ f m = f m
Tactic:
rfl
Proof state after:
no goals
Theorem: sum_primesBelow_eq_sum_range_indicator
Proof state before:
case neg
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : m.Prime
h₂ : ¬(m < n ∧ m.Prime)
⊢ f m = 0
Tactic:
exact (h₂ ⟨Finset.mem_range.mp hm, h₁⟩).elim
Proof state after:
no goals
Theorem: sum_primesBelow_eq_sum_range_indicator
Proof state before:
case pos
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : ¬m.Prime
h₃ : m < n ∧ m.Prime
⊢ 0 = f m
Tactic:
exact (h₁ h₃.2).elim
Proof state after:
no goals
Theorem: sum_primesBelow_eq_sum_range_indicator
Proof state before:
case neg
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
n m : ℕ
hm : m ∈ Finset.range n
h₁ : ¬m.Prime
h₃ : ¬(m < n ∧ m.Prime)
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: tendsto_sum_primesBelow_tsum
Proof state before:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ p ∈ n.primesBelow, f p) atTop (𝓝 (∑' (p : Nat.Primes), f ↑p))
Tactic:
rw [(show ∑' p : Nat.Primes, f p = ∑' p : {p : ℕ | p.Prime}, f p from rfl)]
Proof state after:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ p ∈ n.primesBelow, f p) atTop (𝓝 (∑' (p : ↑{p | p.Prime}), f ↑p))
Theorem: tendsto_sum_primesBelow_tsum
Proof state before:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ p ∈ n.primesBelow, f p) atTop (𝓝 (∑' (p : ↑{p | p.Prime}), f ↑p))
Tactic:
simp_rw [tsum_subtype, sum_primesBelow_eq_sum_range_indicator]
Proof state after:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ m ∈ Finset.range n, {p | p.Prime}.indicator (fun p => f p) m) atTop
    (𝓝 (∑' (x : ℕ), {p | p.Prime}.indicator f x))
Theorem: tendsto_sum_primesBelow_tsum
Proof state before:
R : Type u_1
inst✝⁴ : AddCommGroup R
inst✝³ : UniformSpace R
inst✝² : UniformAddGroup R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
f : ℕ → R
hsum : Summable f
⊢ Tendsto (fun n => ∑ m ∈ Finset.range n, {p | p.Prime}.indicator (fun p => f p) m) atTop
    (𝓝 (∑' (x : ℕ), {p | p.Prime}.indicator f x))
Tactic:
exact (Summable.hasSum_iff_tendsto_nat <| hsum.indicator _).mp <| (hsum.indicator _).hasSum
Proof state after:
no goals
Theorem: Complex.exp_tsum_primes
Proof state before:
f : ℕ → ℂ
hsum : Summable f
⊢ Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (f p)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), f ↑p)))
Tactic:
simpa only [← exp_sum] using Tendsto.cexp <| tendsto_sum_primesBelow_tsum hsum
Proof state after:
no goals
Theorem: Summable.neg_clog_one_sub
Proof state before:
α : Type u_1
f : α → ℂ
hsum : Summable f
⊢ Summable fun n => -(1 - f n).log
Tactic:
let g (z : ℂ) : ℂ := -log (1 - z)
Proof state after:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
⊢ Summable fun n => -(1 - f n).log
Theorem: Summable.neg_clog_one_sub
Proof state before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
⊢ Summable fun n => -(1 - f n).log
Tactic:
have hg : DifferentiableAt ℂ g 0 :=
  DifferentiableAt.neg <| ((differentiableAt_const 1).sub differentiableAt_id').clog <|
    by simp only [sub_zero, one_mem_slitPlane]
Proof state after:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
⊢ Summable fun n => -(1 - f n).log