--- > [! info] Note these LEAN proofs were for LADR Exercises, 2ed 1997, so the numbering does not match LADR, 4th edition of 2024. Fixed, below ### 24 LADR Exercises written in Lean 3 by ProofNet researchers - Here is the most up-to-date Lean version: - note that Exercise numbers changed in Edition 4 [ProofNet at HuggingFace](https://huggingface.co/datasets/hoskinson-center/proofnet?row=59): Here are the complete texts of each exercise, with Natural language statement; NL proof; Lean proof; Lean header information [ProofNet at Github](https://github.com/zhangir-azerbayev/ProofNet) - [Here's the original LEAN work for LADR](https://github.com/zhangir-azerbayev/ProofNet/blob/main/benchmark/benchmark_to_publish/formal/Axler.lean) by [[Zhangir Axerbayev]] about ProofNet - Header statements for Lean: - import .common - open set fintype complex polynomial submodule linear_map finite_dimensional open module module.End inner_product_space - open_locale big_operators ### Exercise numbers: from V2 to V4 | Old V2 Exercise | New V4 Exercise | In Proofnet? | | --------------- | --------------- | ------------ | | 1_2 | 1A-8 | no | | 1_3 | 1B-1 | yes | | 1_4 | 1B-2 | no | | 1_6 | 1C-7 | yes | | 1_7 | 1C-8 | no | | 1_8 | 1C-11 | yes | | 1_9 | 1C-12 | no | | 3_1 | 3A-7 | yes | | 3_8 | 3B-11 | no | | 4_4 | 4.8 | yes | | 5_1 | 5A-2 | no | | 5_4 | 5E-3? | yes | | 5_11 | 5A-23 | no | | 5_12 | 5A-26 | yes | | 5_13 | 5A-27 | no | | 5_20 | ? | yes | | 5_24 | 5B-2 | | | 6_2 | 6A-6 | yes | | 6_3 | 6A-17 | no | | 6_7 | 6A-27 | yes | | 6_13 | 6B-3 | no | | 6_16 | Th-6-54 | yes | | 7_5 | ? | no | | 7_6 | ? | yes | | 7_9 | 7B-1 | no | | 7_10 | 7B-6 | yes | | 7_11 | 7B-10 | no | | 7_14 | 7B-23 | yes | > [! info] > Original problem set numbers refer to LADR edition 2: 1997; here, they are matched to LADR edition 4: 2024 > We abbreviate ProofNet to PN; Natural Language to NL; ## 1A-8 - Lean 1_2: - theorem exercise_1_2 : (⟨-1/2, real.sqrt 3 / 2⟩ : ℂ) ^ 3 = -1 := sorry [ProofNet Natural Language]() ## 1B-1 - NL: Prove that $-(-v) = v$ for every $v \in V$. - NL-proof: - \begin{proof} By definition, we have $ (-v)+(-(-v))=0 \quad \text { and } \quad v+(-v)=0 . $ This implies both $v$ and $-(-v)$ are additive inverses of $-v$, by the uniqueness of additive inverse, it follows that $-(-v)=v$. \end{proof} - Formal statement: - theorem exercise_1_3 {F V : Type*} [add_comm_group V] [field F] [module F V] {v : V} : -(-v) = v := - src_header - import .common open set fintype complex polynomial submodule linear_map finite_dimensional open module module.End inner_product_space open_locale big_operators - Lean 1_3: - theorem exercise_1_3 {F V : Type*} [add_comm_group V] [field F] [module F V] {v : V} : -(-v) = v := sorry - [NL](https://huggingface.co/datasets/hoskinson-center/proofnet?row=59) ## 1B-2 - Lean: - theorem exercise_1_4 {F V : Type*} [add_comm_group V] [field F] [module F V] (v : V) (a : F): a • v = 0 ↔ a = 0 ∨ v = 0 := sorry ## 1C-7 - NL: additive inverses (meaning $-u \in U$ whenever $u \in U$), but $U$ is not a subspace of $\mathbf{R}^2$. - nl_proof: - \begin{proof} \[U=\mathbb{Z}^2=\left\{(x, y) \in \mathbf{R}^2: x, y \text { are integers }\right\}\] $U=\mathbb{Z}^2$ satisfies the desired properties. To come up with this, note by assumption, $U$ must be closed under addition and subtraction, so in particular, it must contain 0 . We need to find a set which fails scalar multiplication. A discrete set like $\mathbb{Z}^2$ does this. \end{proof} - Lean - theorem exercise_1_6 : ∃ U : set (ℝ × ℝ), (U ≠ ∅) ∧ (∀ (u v : ℝ × ℝ), u ∈ U ∧ v ∈ U → u + v ∈ U) ∧ (∀ (u : ℝ × ℝ), u ∈ U → -u ∈ U) ∧ (∀ U' : submodule ℝ (ℝ × ℝ), U ≠ ↑U') := sorry ## 1C-8 theorem exercise_1_7 : ∃ U : set (ℝ × ℝ), (U ≠ ∅) ∧ (∀ (c : ℝ) (u : ℝ × ℝ), u ∈ U → c • u ∈ U) ∧ (∀ U' : submodule ℝ (ℝ × ℝ), U ≠ ↑U') := sorry ## 1C-11 - NL: Prove that the intersection of any collection of subspaces of $V$ is a subspace of $V$. - nl_proof: - \begin{proof} Let $V_1, V_2, \ldots, V_n$ be subspaces of the vector space $V$ over the field $F$. We must show that their intersection $V_1 \cap V_2 \cap \ldots \cap V_n$ is also a subspace of $V$. To begin, we observe that the additive identity $0$ of $V$ is in $V_1 \cap V_2 \cap \ldots \cap V_n$. This is because $0$ is in each subspace $V_i$, as they are subspaces and hence contain the additive identity. Next, we show that the intersection of subspaces is closed under addition. Let $u$ and $v$ be vectors in $V_1 \cap V_2 \cap \ldots \cap V_n$. By definition, $u$ and $v$ belong to each of the subspaces $V_i$. Since each $V_i$ is a subspace and therefore closed under addition, it follows that $u+v$ belongs to each $V_i$. Thus, $u+v$ belongs to the intersection $V_1 \cap V_2 \cap \ldots \cap V_n$. Finally, we show that the intersection of subspaces is closed under scalar multiplication. Let $a$ be a scalar in $F$ and let $v$ be a vector in $V_1 \cap V_2 \cap \ldots \cap V_n$. Since $v$ belongs to each $V_i$, we have $av$ belongs to each $V_i$ as well, as $V_i$ are subspaces and hence closed under scalar multiplication. Therefore, $av$ belongs to the intersection $V_1 \cap V_2 \cap \ldots \cap V_n$. Thus, we have shown that $V_1 \cap V_2 \cap \ldots \cap V_n$ is a subspace of $V$. \end{proof} - Lean 1_8: - theorem exercise_1_8 {F V : Type*} [add_comm_group V] [field F] [module F V] {ι : Type*} (u : ι → submodule F V) : ∃ U : submodule F V, (⋂ (i : ι), (u i).carrier) = ↑U := sorry ## 1C-12 - Lean 1_9 - theorem exercise_1_9 {F V : Type*} [add_comm_group V] [field F] [module F V] (U W : submodule F V): ∃ U' : submodule F V, (U'.carrier = ↑U ∩ ↑W ↔ (U ≤ W ∨ W ≤ U)) := sorry ## 3A-7 - NL: - Show that every linear map from a one-dimensional vector space to itself is multiplication by some scalar. More precisely, prove that if $\operatorname{dim} V=1$ and $T \in \mathcal{L}(V, V)$, then there exists $a \in \mathbf{F}$ such that $T v=a v$ for all $v \in V$. - nl_proof: - \begin{proof} If $\operatorname{dim} V=1$, then in fact, $V=\mathbf{F}$ and it is spanned by $1 \in \mathbf{F}$. Let $T$ be a linear map from $V$ to itself. Let $T(1)=\lambda \in V(=\mathbf{F})$. Step 2 2 of 3 Every $v \in V$ is a scalar. Therefore, $ \begin{aligned} T(v) & =T(v \cdot 1) \\ & =v T(1) \ldots .(\text { By the linearity of } T) \\ & =v \lambda \end{aligned} $ Hence, $T v=\lambda v$ for every $v \in V$. \end{proof} - Formal Statement: - theorem exercise_3_1 {F V : Type*} [add_comm_group V] [field F] [module F V] [finite_dimensional F V] (T : V →ₗ[F] V) (hT : finrank F V = 1) : ∃ c : F, ∀ v : V, T v = c • v:= - Lean 3_1: theorem exercise_3_1 {F V : Type*} [add_comm_group V] [field F] [module F V] [finite_dimensional F V] (T : V →ₗ[F] V) (hT : finrank F V = 1) : ∃ c : F, ∀ v : V, T v = c • v:= sorry ## 3B-11 theorem exercise_3_8 {F V W : Type*} [add_comm_group V] [add_comm_group W] [field F] [module F V] [module F W] (L : V →ₗ[F] W) : ∃ U : submodule F V, U ⊓ L.ker = ⊥ ∧ linear_map.range L = range (dom_restrict L U):= sorry ## 4.8 theorem exercise_4_4 (p : polynomial ℂ) : p.degree = @card (root_set p ℂ) (polynomial.root_set_fintype p ℂ) ↔ disjoint (@card (root_set p.derivative ℂ) (polynomial.root_set_fintype p.derivative ℂ)) (@card (root_set p ℂ) (polynomial.root_set_fintype p ℂ)) := sorry ## 5A-2 theorem exercise_5_1 {F V : Type*} [add_comm_group V] [field F] [module F V] {L : V →ₗ[F] V} {n : ℕ} (U : fin n → submodule F V) (hU : ∀ i : fin n, map L (U i) = U i) : map L (∑ i : fin n, U i : submodule F V) = (∑ i : fin n, U i : submodule F V) := sorry ## 5E-3 ? - NL: - Suppose that $S, T \in \mathcal{L}(V)$ are such that $S T=T S$. Prove that $\operatorname{null} (T-\lambda I)$ is invariant under $S$ for every $\lambda \in \mathbf{F}$. - - - Lean 5_4: - theorem exercise_5_4 {F V : Type*} [add_comm_group V] [field F] [module F V] (S T : V →ₗ[F] V) (hST : S ∘ T = T ∘ S) (c : F): map S (T - c • id).ker = (T - c • id).ker := sorry ## 5A-23 - - - - Lean 5_11 - theorem exercise_5_11 {F V : Type*} [add_comm_group V] [field F] [module F V] (S T : End F V) : (S * T).eigenvalues = (T * S).eigenvalues := sorry ## 5A-26 - NL: - Suppose $T \in \mathcal{L}(V)$ is such that every vector in $V$ is an eigenvector of $T$. Prove that $T$ is a scalar multiple of the identity operator. - nl_proof: - \begin{proof} For every single $v \in V$, there does exist $a_v \in F$ such that $T v=a_v v$. Since $T 0=0$, then we have to make $a_0$ be the any number in F. However, for every single $v \in V\{0\}$, then the value of $a_V$ is uniquely determined by the previous equation of $T v=a_v v$. Now, to show that $T$ is a scalar multiple of the identity, then me must show that $a_v$ is independent of $v$ for $v \in V\{0\}$. We would now want to show that $a_v=a_w$. First, just make the case of where $(v, w)$ is linearly dependent. Then, there does exist $b \in F$ such that $w=b v$. Now, you would have the following: $a_W w=T w=T(b v)=b T v=b\left(a_v v\right)=a_v w$. This is showing that $a_v=a_w$. Finally, make the consideration to make $(v, w)$ be linearly independent. Now, we would have the following: $\left.a_{(} v+w\right)(v+w)=T(v+w)=T v+T w=a_v v+a_w w$. That previous equation implies the following: $\left.\left.\left(a_{(} v+w\right)-a_v\right) v+\left(a_{(} v+w\right)-a_w\right) w=0$. Since $(v, w)$ is linearly independent, this would imply that both $\left.a_{(} v+w\right)=a_v$ and $\left.a_{(} v+w\right)=a_w$. Therefore, $a_v=a_w$. \end{proof} - - Lean 5_12 - theorem exercise_5_12 {F V : Type*} [add_comm_group V] [field F] [module F V] {S : End F V} (hS : ∀ v : V, ∃ c : F, v ∈ eigenspace S c) : ∃ c : F, S = c • id := sorry ## 5A-27 theorem exercise_5_13 {F V : Type*} [add_comm_group V] [field F] [module F V] [finite_dimensional F V] {T : End F V} (hS : ∀ U : submodule F V, finrank F U = finrank F V - 1 → map T U = U) : ∃ c : F, T = c • id := sorry ## ? see 5-3 - NL: - Suppose that $T \in \mathcal{L}(V)$ has $\operatorname{dim} V$ distinct eigenvalues and that $S \in \mathcal{L}(V)$ has the same eigenvectors as $T$ (not necessarily with the same eigenvalues). Prove that $S T=T S$. - nl_proof: - \begin{proof} First off, let $n=\operatorname{dim} V$. so, there is a basis of $\left(v_1, \ldots, v_j\right)$ of $V$ that consist of eigenvectors of $T$. Now, let $\lambda_1, \ldots, \lambda_n$ be the corresponding eigenvalues, then we would have $T v_j=\lambda_1 v_j$ for every single $j$. Now, for every $v_j$ is also an eigenvector of S, so $S v_j=a_j v_j$ for some $a_j \in F$. For each $j$, we would then have $(S T) v_j=S\left(T v_j\right)=\lambda_j S v_j=a_j \lambda_j v_j$ and $(T S) v_j=T\left(S v_j\right)=a_j T v_j=a_j \lambda_j v_j$. Since both operators, which are $S T$ and $T S$, agree on a basis, then both are equal. \end{proof} - Formal statement: - theorem exercise_5_20 {F V : Type*} [add_comm_group V] [field F] [module F V] [finite_dimensional F V] {S T : End F V} (h1 : @card T.eigenvalues (eigenvalues.fintype T) = finrank F V) (h2 : ∀ v : V, ∃ c : F, v ∈ eigenspace S c ↔ ∃ c : F, v ∈ eigenspace T c) : S * T = T * S := - Lean 5-20 - theorem exercise_5_20 {F V : Type*} [add_comm_group V] [field F] [module F V] [finite_dimensional F V] {S T : End F V} (h1 : @card T.eigenvalues (eigenvalues.fintype T) = finrank F V) (h2 : ∀ v : V, ∃ c : F, v ∈ eigenspace S c ↔ ∃ c : F, v ∈ eigenspace T c) : S * T = T * S := sorry ## 5B-2 - - - - Lean 5_24: - theorem exercise_5_24 {V : Type*} [add_comm_group V] [module ℝ V] [finite_dimensional ℝ V] {T : End ℝ V} (hT : ∀ c : ℝ, eigenspace T c = ⊥) {U : submodule ℝ V} (hU : map T U = U) : even (finrank U) := sorry ## 6A-6 theorem exercise_6_2 {V : Type*} [add_comm_group V] [module ℂ V] [inner_product_space ℂ V] (u v : V) : ⟪u, v⟫_ℂ = 0 ↔ ∀ (a : ℂ), ‖u‖ ≤ ‖u + a • v‖ := sorry ## 6A-17 theorem exercise_6_3 {n : ℕ} (a b : fin n → ℝ) : (∑ i, a i * b i) ^ 2 ≤ (∑ i : fin n, i * a i ^ 2) * (∑ i, b i ^ 2 / i) := sorry ## 6A-27 theorem exercise_6_7 {V : Type*} [inner_product_space ℂ V] (u v : V) : ⟪u, v⟫_ℂ = (‖u + v‖^2 - ‖u - v‖^2 + I*‖u + I•v‖^2 - I*‖u-I•v‖^2) / 4 := sorry ## 6B-3 theorem exercise_6_13 {V : Type*} [inner_product_space ℂ V] {n : ℕ} {e : fin n → V} (he : orthonormal ℂ e) (v : V) : ‖v‖^2 = ∑ i : fin n, ‖⟪v, e i⟫_ℂ‖^2 ↔ v ∈ span ℂ (e '' univ) := sorry ## ? - NL: - Suppose $U$ is a subspace of $V$. Prove that $U^{\perp}=\{0\}$ if and only if $U=V$ - nl_proof - \begin{proof} $V=U \bigoplus U^{\perp}$, therefore $U^\perp = \{0\}$ iff $U=V$. \end{proof} - - Lean 6_16 - theorem exercise_6_16 {K V : Type*} [is_R_or_C K] [inner_product_space K V] {U : submodule K V} : U.orthogonal = ⊥ ↔ U = ⊤ := sorry ## ? - - - - Lean.7_5 - theorem exercise_7_5 {V : Type*} [inner_product_space ℂ V] [finite_dimensional ℂ V] (hV : finrank V ≥ 2) : ∀ U : submodule ℂ (End ℂ V), U.carrier ≠ {T | T * T.adjoint = T.adjoint * T} := sorry ## Th-7-21 - NL: - Prove that if $T \in \mathcal{L}(V)$ is normal, then $\operatorname{range} T=\operatorname{range} T^{*}.$ - - - Lean 7_6: - theorem exercise_7_6 {V : Type*} [inner_product_space ℂ V] [finite_dimensional ℂ V] (T : End ℂ V) (hT : T * T.adjoint = T.adjoint * T) : T.range = T.adjoint.range := sorry ## 7B-1 - NL: - - - - Lean 7_9: - theorem exercise_7_9 {V : Type*} [inner_product_space ℂ V] [finite_dimensional ℂ V] (T : End ℂ V) (hT : T * T.adjoint = T.adjoint * T) : is_self_adjoint T ↔ ∀ e : T.eigenvalues, (e : ℂ).im = 0 := sorry ## 7B-6 - NL: - Suppose $V$ is a complex inner-product space and $T \in \mathcal{L}(V)$ is a normal operator such that $T^{9}=T^{8}$. Prove that $T$ is self-adjoint and $T^{2}=T$. - - Lean 7_10: - theorem exercise_7_10 {V : Type*} [inner_product_space ℂ V] [finite_dimensional ℂ V] (T : End ℂ V) (hT : T * T.adjoint = T.adjoint * T) (hT1 : T^9 = T^8) : is_self_adjoint T ∧ T^2 = T := sorry ## 7B-10 theorem exercise_7_11 {V : Type*} [inner_product_space ℂ V] [finite_dimensional ℂ V] {T : End ℂ V} (hT : T*T.adjoint = T.adjoint*T) : ∃ (S : End ℂ V), S ^ 2 = T := sorry ## 7B-23 - NL: - Suppose $T \in \mathcal{L}(V)$ is self-adjoint, $\lambda \in \mathbf{F}$, and $\epsilon>0$. Prove that if there exists $v \in V$ such that $\|v\|=1$ and $\|T v-\lambda v\|<\epsilon,$ then $T$ has an eigenvalue $\lambda^{\prime}$ such that $\left|\lambda-\lambda^{\prime}\right|<\epsilon$. - - - - Lean 7_14: - theorem exercise_7_14 {𝕜 V : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 V] [finite_dimensional 𝕜 V] {T : End 𝕜 V} (hT : is_self_adjoint T) {l : 𝕜} {ε : ℝ} (he : ε > 0) : ∃ v : V, ‖v‖= 1 ∧ (‖T v - l • v‖ < ε → (∃ l' : T.eigenvalues, ‖l - l'‖ < ε)) := sorry