chore(linear_algebra/*): rename copair, pair to coprod, prod (#2213)

* chore(linear_algebra/*): rename copair, pair to coprod, prod * add back mistakenly deleted lemma * fix sensitivity, change comments to module docs * docstrings, linting * Update archive/sensitivity.lean Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
leanprover-community · Mar 22, 2020 · 7d02c23 · 7d02c23
1 parent 3a71499
commit 7d02c23
Show file tree

Hide file tree

Showing 4 changed files with 225 additions and 186 deletions.
diff --git a/archive/sensitivity.lean b/archive/sensitivity.lean
@@ -1,5 +1,6 @@
 /-
-Copyright (c) 2019 Reid Barton, Johan Commelin, Jesse Han, Chris Hughes, Robert Y. Lewis, and Patrick Massot. All rights reserved.
+Copyright (c) 2019 Reid Barton, Johan Commelin, Jesse Han, Chris Hughes, Robert Y. Lewis, and
+Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Johan Commelin, Jesse Han, Chris Hughes, Robert Y. Lewis, and Patrick Massot
 -/
@@ -11,6 +12,8 @@ import linear_algebra.dual
 import analysis.normed_space.basic
 
 /-!
+# Huang's sensitivity theorem
+
 A formalization of Hao Huang's sensitivity theorem: in the hypercube of
 dimension n ≥ 1, if one colors more than half the vertices then at least one
 vertex has at least √n colored neighbors.
@@ -19,7 +22,7 @@ A fun summer collaboration by
 Reid Barton, Johan Commelin, Jesse Han, Chris Hughes, Robert Y. Lewis, and Patrick Massot,
 based on Don Knuth's account of the story
 (https://www.cs.stanford.edu/~knuth/papers/huang.pdf),
-using the Lean theorem prover (http://leanprover.github.io/),
+using the Lean theorem prover (https://leanprover.github.io/),
 by Leonardo de Moura at Microsoft Research, and his collaborators
 (https://leanprover.github.io/people/),
 and using Lean's user maintained mathematics library
@@ -29,8 +32,8 @@ The project was developed at https://github.com/leanprover-community/lean-sensit
 and is now archived at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean
 -/
 
--- The next two lines assert we do not want to give a constructive proof,
--- but rather use classical logic.
+/-! The next two lines assert we do not want to give a constructive proof,
+but rather use classical logic. -/
 noncomputable theory
 open_locale classical
 
@@ -39,38 +42,35 @@ notation `√` := real.sqrt
 
 open function bool linear_map fintype finite_dimensional dual_pair
 
-/- -------------------------------------------------------------------------\
-|  The hypercube.                                                           |
-\---------------------------------------------------------------------------/
+/-! ### The hypercube
 
-/-
 Notations:
-ℕ denotes natural numbers (including zero).
-fin n = {0, ⋯ , n - 1}.
-bool = {tt, ff}.
+- `ℕ` denotes natural numbers (including zero).
+- `fin n` = {0, ⋯ , n - 1}.
+- `bool` = {`tt`, `ff`}.
 -/
 
-/-- The hypercube in dimension n. -/
+/-- The hypercube in dimension `n`. -/
 @[derive [inhabited, fintype]] def Q (n : ℕ) := fin n → bool
 
-/-- The projection from Q (n + 1) to Q n forgetting the first value
+/-- The projection from `Q (n + 1)` to `Q n` forgetting the first value
 (ie. the image of zero). -/
 def π {n : ℕ} : Q (n + 1) → Q n := λ p, p ∘ fin.succ
 
 namespace Q
--- n will always denote a natural number.
+/-! `n` will always denote a natural number. -/
 variable (n : ℕ)
 
-/-- Q 0 has a unique element. -/
+/-- `Q 0` has a unique element. -/
 instance : unique (Q 0) :=
 ⟨⟨λ _, tt⟩, by { intro, ext x, fin_cases x }⟩
 
-/-- Q n has 2^n elements. -/
+/-- `Q n` has 2^n elements. -/
 lemma card : card (Q n) = 2^n :=
 by simp [Q]
 
--- Until the end of this namespace, n will be an implicit argument (still
--- a natural number).
+/-! Until the end of this namespace, `n` will be an implicit argument (still
+a natural number). -/
 variable {n}
 
 lemma succ_n_eq (p q : Q (n+1)) : p = q ↔ (p 0 = q 0 ∧ π p = π q) :=
@@ -85,16 +85,16 @@ begin
       convert congr_fun h (fin.pred x hx) } }
 end
 
-/-- The adjacency relation defining the graph structure on Q n:
-p.adjacent q if there is an edge from p to q in Q n -/
+/-- The adjacency relation defining the graph structure on `Q n`:
+`p.adjacent q` if there is an edge from `p` to `q` in `Q n`. -/
 def adjacent {n : ℕ} (p : Q n) : set (Q n) := λ q, ∃! i, p i ≠ q i
 
-/-- In Q 0, no two vertices are adjacent. -/
+/-- In `Q 0`, no two vertices are adjacent. -/
 lemma not_adjacent_zero (p q : Q 0) : ¬ p.adjacent q :=
 by rintros ⟨v, _⟩; apply fin_zero_elim v
 
-/-- If p and q in Q (n+1) have different values at zero then they are adjacent
-iff their projections to Q n are equal. -/
+/-- If `p` and `q` in `Q (n+1)` have different values at zero then they are adjacent
+iff their projections to `Q n` are equal. -/
 lemma adj_iff_proj_eq {p q : Q (n+1)} (h₀ : p 0 ≠ q 0) :
   p.adjacent q ↔ π p = π q :=
 begin
@@ -111,8 +111,8 @@ begin
     apply congr_fun heq }
 end
 
-/-- If p and q in Q (n+1) have the same value at zero then they are adjacent
-iff their projections to Q n are adjacent. -/
+/-- If `p` and `q` in `Q (n+1)` have the same value at zero then they are adjacent
+iff their projections to `Q n` are adjacent. -/
 lemma adj_iff_proj_adj {p q : Q (n+1)} (h₀ : p 0 = q 0) :
   p.adjacent q ↔ (π p).adjacent (π q) :=
 begin
@@ -141,9 +141,7 @@ by simp only [adjacent, ne_comm]
 
 end Q
 
-/- -------------------------------------------------------------------------\
-|  The vector space.                                                        |
-\---------------------------------------------------------------------------/
+/-! ### The vector space -/
 
 /-- The free vector space on vertices of a hypercube, defined inductively. -/
 def V : ℕ → Type
@@ -153,7 +151,7 @@ def V : ℕ → Type
 namespace V
 variables (n : ℕ)
 
--- V n is a real vector space whose equality relation is computable.
+/-! `V n` is a real vector space whose equality relation is computable. -/
 
 instance : decidable_eq (V n) :=
 by { induction n ; { dunfold V, resetI, apply_instance } }
@@ -164,8 +162,8 @@ by { induction n ; { dunfold V, resetI, apply_instance } }
 instance : vector_space ℝ (V n) :=
 by { induction n ; { dunfold V, resetI, apply_instance } }
 
--- The next five definitions are short circuits helping Lean to quickly find
--- relevant structures on V n
+/-! The next five definitions are short circuits helping Lean to quickly find
+relevant structures on `V n`. -/
 def module : module ℝ (V n) := by apply_instance
 def add_comm_semigroup : add_comm_semigroup (V n) := by apply_instance
 def add_comm_monoid : add_comm_monoid (V n) := by apply_instance
@@ -177,14 +175,14 @@ end V
 local attribute [instance, priority 100000]
   V.module V.add_comm_semigroup V.add_comm_monoid V.has_scalar V.has_add
 
-/-- The basis of V indexed by the hypercube, defined inductively. -/
+/-- The basis of `V` indexed by the hypercube, defined inductively. -/
 noncomputable def e : Π {n}, Q n → V n
 | 0     := λ _, (1:ℝ)
 | (n+1) := λ x, cond (x 0) (e (π x), 0) (0, e (π x))
 
 @[simp] lemma e_zero_apply (x : Q 0) : e x = (1 : ℝ) := rfl
 
-/-- The dual basis to e, defined inductively. -/
+/-- The dual basis to `e`, defined inductively. -/
 noncomputable def ε : Π {n : ℕ} (p : Q n), V n →ₗ[ℝ] ℝ
 | 0 _ := linear_map.id
 | (n+1) p := cond (p 0) ((ε $ π p).comp $ linear_map.fst _ _ _) ((ε $ π p).comp $ linear_map.snd _ _ _)
@@ -210,7 +208,7 @@ begin
         simp [this] } } }
 end
 
-/-- Any vector in V n annihilated by all ε p's is zero. -/
+/-- Any vector in `V n` annihilated by all `ε p`'s is zero. -/
 lemma epsilon_total {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 :=
 begin
   induction n with n ih,
@@ -225,14 +223,14 @@ begin
       rwa show p = π q, by { ext, simp [q, fin.succ_ne_zero, π] } } }
 end
 
-/-- e and ε are dual families of vectors. It implies that e is indeed a basis
-and ε computes coefficients of decompositions of vectors on that basis. -/
+/-- `e` and `ε` are dual families of vectors. It implies that `e` is indeed a basis
+and `ε` computes coefficients of decompositions of vectors on that basis. -/
 def dual_pair_e_ε (n : ℕ) : dual_pair (@e n) (@ε n) :=
 { eval := duality,
   total := @epsilon_total _ }
 
--- We will now derive the dimension of V, first as a cardinal in dim_V and,
--- since this cardinal is finite, as a natural number in findim_V
+/-! We will now derive the dimension of `V`, first as a cardinal in `dim_V` and,
+since this cardinal is finite, as a natural number in `findim_V` -/
 
 lemma dim_V : vector_space.dim ℝ (V n) = 2^n :=
 have vector_space.dim ℝ (V n) = ↑(2^n : ℕ),
@@ -246,21 +244,19 @@ lemma findim_V : findim ℝ (V n) = 2^n :=
 have _ := @dim_V n,
 by rw ←findim_eq_dim at this; assumption_mod_cast
 
-/- -------------------------------------------------------------------------\
-|  The linear map.                                                          |
-\---------------------------------------------------------------------------/
+/-! ### The linear map -/
 
-/-- The linear operator f_n corresponding to Huang's matrix A_n,
-defined inductively as a ℝ-linear map from V n to V n. -/
+/-- The linear operator $f_n$ corresponding to Huang's matrix $A_n$,
+defined inductively as a ℝ-linear map from `V n` to `V n`. -/
 noncomputable def f : Π n, V n →ₗ[ℝ] V n
 | 0 := 0
-| (n+1) := linear_map.pair
-             (linear_map.copair (f n) linear_map.id)
-             (linear_map.copair linear_map.id (-f n))
+| (n+1) := linear_map.prod
+             (linear_map.coprod (f n) linear_map.id)
+             (linear_map.coprod linear_map.id (-f n))
 
--- The preceding definition use linear map constructions to automatically
--- get that f is linear, but its values are somewhat buried as a side-effect.
--- The next two lemmas unbury them.
+/-! The preceding definition uses linear map constructions to automatically
+get that `f` is linear, but its values are somewhat buried as a side-effect.
+The next two lemmas unbury them. -/
 
 @[simp] lemma f_zero : f 0 = 0 := rfl
 
@@ -269,14 +265,14 @@ lemma f_succ_apply (v : V (n+1)) :
 begin
   cases v,
   rw f,
-  simp only [linear_map.id_apply, linear_map.pair_apply, prod.mk.inj_iff,
-    linear_map.neg_apply, sub_eq_add_neg, linear_map.copair_apply],
+  simp only [linear_map.id_apply, linear_map.prod_apply, prod.mk.inj_iff,
+    linear_map.neg_apply, sub_eq_add_neg, linear_map.coprod_apply],
   exact ⟨rfl, rfl⟩
 end
 
--- In the next statement, the explicit conversion (n : ℝ) of n to a real number
--- is necessary since otherwise `n • v` refers to the multiplication defined
--- using only the addition of V.
+/-! In the next statement, the explicit conversion `(n : ℝ)` of `n` to a real number
+is necessary since otherwise `n • v` refers to the multiplication defined
+using only the addition of `V`. -/
 
 lemma f_squared : ∀ v : V n, (f n) (f n v) = (n : ℝ) • v :=
 begin
@@ -285,8 +281,8 @@ begin
   { cases v, simp [f_succ_apply, IH, add_smul], abel }
 end
 
--- We now compute the matrix of f in the e basis (p is the line index,
--- q the column index.)
+/-! We now compute the matrix of `f` in the `e` basis (`p` is the line index,
+`q` the column index). -/
 
 lemma f_matrix :
   ∀ p q : Q n, |ε q (f n (e p))| = if q.adjacent p then 1 else 0 :=
@@ -307,22 +303,22 @@ begin
       congr' 1 } }
 end
 
-/-- The linear operator g_m corresponding to Knuth's matrix B_m. -/
+/-- The linear operator $g_m$ corresponding to Knuth's matrix $B_m$. -/
 noncomputable def g (m : ℕ) : V m →ₗ[ℝ] V (m+1) :=
-linear_map.pair (f m + √(m+1) • linear_map.id) linear_map.id
+linear_map.prod (f m + √(m+1) • linear_map.id) linear_map.id
 
--- in the following lemmas, m will denote a natural number
+/-! In the following lemmas, `m` will denote a natural number. -/
 variables {m : ℕ}
 
--- again we unpack what are the values of g
+/-! Again we unpack what are the values of `g`. -/
 lemma g_apply : ∀ v, g m v = (f m v + √(m+1) • v, v) :=
 by delta g; simp
 
 lemma g_injective : injective (g m) :=
 begin
   rw g,
   intros x₁ x₂ h,
-  simp only [linear_map.pair_apply, linear_map.id_apply, prod.mk.inj_iff] at h,
+  simp only [linear_map.prod_apply, linear_map.id_apply, prod.mk.inj_iff] at h,
   exact h.right
 end
 
@@ -336,32 +332,31 @@ begin
   abel
 end
 
-/- -------------------------------------------------------------------------\
-|  The main proof.                                                          |
-\---------------------------------------------------------------------------/
+/-!
+### The main proof
 
--- In this section, in order to enforce that n is positive, we write it as
--- m + 1 for some natural number m.
+In this section, in order to enforce that `n` is positive, we write it as
+`m + 1` for some natural number `m`. -/
 
--- dim X will denote the dimension of a subspace X as a cardinal
+/-! `dim X` will denote the dimension of a subspace `X` as a cardinal. -/
 notation `dim` X:70 := vector_space.dim ℝ ↥X
--- fdim X will denote the (finite) dimension of a subspace X as a natural number
+/-! `fdim X` will denote the (finite) dimension of a subspace `X` as a natural number. -/
 notation `fdim` := findim ℝ
 
--- Span S will denote the ℝ-subspace spanned by S
+/-! `Span S` will denote the ℝ-subspace spanned by `S`. -/
 notation `Span` := submodule.span ℝ
 
--- Card X will denote the cardinal of a subset of a finite type, as a
--- natural number.
+/-! `Card X` will denote the cardinal of a subset of a finite type, as a
+natural number. -/
 notation `Card` X:70 := X.to_finset.card
 
--- In the following, ⊓ and ⊔ will denote intersection and sums of ℝ-subspaces,
--- equipped with their subspace structures. The notations come from the general
--- theory of lattices, with inf and sup (also known as meet and join).
+/-! In the following, `⊓` and `⊔` will denote intersection and sums of ℝ-subspaces,
+equipped with their subspace structures. The notations come from the general
+theory of lattices, with inf and sup (also known as meet and join). -/
 
-/-- If a subset H of Q (m+1) has cardinal at least 2^m + 1 then the
-subspace of V (m+1) spanned by the corresponding basis vectors non-trivially
-intersects the range of g m. -/
+/-- If a subset `H` of `Q (m+1)` has cardinal at least `2^m + 1` then the
+subspace of `V (m+1)` spanned by the corresponding basis vectors non-trivially
+intersects the range of `g m`. -/
 lemma exists_eigenvalue (H : set (Q (m + 1))) (hH : Card H ≥ 2^m + 1) :
   ∃ y ∈ Span (e '' H) ⊓ (g m).range, y ≠ (0 : _) :=
 begin