chore(archive + counterexamples): namespaces imo, theorems_100, count…

…erexample, plus three more (#19129)

This PR is a revision of #19122: it addresses namespacing in `archive` and `counterexamples`.

The main difference with #19122 is that it adds namespaces less aggressively: I added a namespace only if there was not an explicit namespace after the initial "fluff".  In `counterexamples`, I added namespaces to all files.

I introduced three "main" namespaces: `imo, theorems_100, counterexample` (the last one singular).  Besides these, I also introduced the namespaces `prop_encodable, oxford_invariants, sensitivity`, to cover the left-over files in `archive`.

Note that if a file has `namespace` early on, then it does not get a new namespace, even though it might be desirable for it to have one.

Comments are very welcome!

Note: besides adding namespaces, the only files that I had to manually edit are the ones in
* commit d337b99 -- I do not like these changes, but currently do not see how to avoid them;
* commit 48471f3 -- I *removed* an pre-existing namespace, replacing it by `open <itself>`.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mk_all.2Esh): this PR is motivated by the desire to port to mathlib4 the files in `archive, counterexamples`, taking advantage of `mathport`.  The namespacing helps with avoiding clashes among names of declarations, as well as one-lettered declarations in the root namespace.

archive/100-theorems-list/37_solution_of_cubic.lean

@@ -35,6 +35,8 @@ Originally ported from Isabelle/HOL. The
 polynomial, cubic, root
 -/
 
+namespace theorems_100
+
 section field
 
 open polynomial
@@ -184,3 +186,5 @@ begin
 end
 
 end field
+
+end theorems_100

archive/100-theorems-list/42_inverse_triangle_sum.lean

@@ -23,7 +23,7 @@ open_locale big_operators
 open finset
 
 /-- **Sum of the Reciprocals of the Triangular Numbers** -/
-lemma inverse_triangle_sum :
+lemma theorem_100.inverse_triangle_sum :
   ∀ n, ∑ k in range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n :=
 begin
   refine sum_range_induction _ _ (if_pos rfl) _,

archive/100-theorems-list/45_partition.lean

@@ -53,6 +53,8 @@ https://en.wikipedia.org/wiki/Partition_(number_theory)#Odd_parts_and_distinct_p
 -/
 
 open power_series
+namespace theorems_100
+
 noncomputable theory
 
 variables {α : Type*}
@@ -521,3 +523,5 @@ begin
   rw odd_gf_prop n (n+1) (by linarith),
   apply same_coeffs (n+1) n n.le_succ,
 end
+
+end theorems_100

archive/100-theorems-list/57_herons_formula.lean

@@ -21,6 +21,8 @@ lengths.
 open real euclidean_geometry
 open_locale real euclidean_geometry
 
+namespace theorems_100
+
 local notation `√` := real.sqrt
 
 variables {V : Type*} {P : Type*}
@@ -61,3 +63,5 @@ begin
                                                           one_mul, mul_div_cancel];
                                                       norm_num,
 end
+
+end theorems_100

archive/100-theorems-list/70_perfect_numbers.lean

@@ -26,21 +26,23 @@ Euler proved the converse, that if `n` is even and perfect, then there exists `k
 https://en.wikipedia.org/wiki/Euclid%E2%80%93Euler_theorem
 -/
 
+namespace theorems_100
+
 lemma odd_mersenne_succ (k : ℕ) : ¬ 2 ∣ mersenne (k + 1) :=
 by simp [← even_iff_two_dvd, ← nat.even_add_one] with parity_simps
 
 namespace nat
-open arithmetic_function finset
+open nat.arithmetic_function finset
 open_locale arithmetic_function
 
 lemma sigma_two_pow_eq_mersenne_succ (k : ℕ) : σ 1 (2 ^ k) = mersenne (k + 1) :=
-by simp [sigma_one_apply, mersenne, prime_two, ← geom_sum_mul_add 1 (k+1)]
+by simp [sigma_one_apply, mersenne, nat.prime_two, ← geom_sum_mul_add 1 (k+1)]
 
 /-- Euclid's theorem that Mersenne primes induce perfect numbers -/
 theorem perfect_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).prime) :
-  perfect ((2 ^ k) * mersenne (k + 1)) :=
+  nat.perfect ((2 ^ k) * mersenne (k + 1)) :=
 begin
-  rw [perfect_iff_sum_divisors_eq_two_mul, ← mul_assoc, ← pow_succ, ← sigma_one_apply, mul_comm,
+  rw [nat.perfect_iff_sum_divisors_eq_two_mul, ← mul_assoc, ← pow_succ, ← sigma_one_apply, mul_comm,
     is_multiplicative_sigma.map_mul_of_coprime
         (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)),
     sigma_two_pow_eq_mersenne_succ],
@@ -53,7 +55,7 @@ lemma ne_zero_of_prime_mersenne (k : ℕ) (pr : (mersenne (k + 1)).prime) :
   k ≠ 0 :=
 begin
   intro H,
-  simpa [H, mersenne, not_prime_one] using pr,
+  simpa [H, mersenne, nat.not_prime_one] using pr,
 end
 
 theorem even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).prime) :
@@ -77,26 +79,26 @@ end
 
 /-- **Perfect Number Theorem**: Euler's theorem that even perfect numbers can be factored as a
   power of two times a Mersenne prime. -/
-theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : even n) (perf : perfect n) :
-  ∃ (k : ℕ), prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) :=
+theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : even n) (perf : nat.perfect n) :
+  ∃ (k : ℕ), nat.prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) :=
 begin
   have hpos := perf.2,
   rcases eq_two_pow_mul_odd hpos with ⟨k, m, rfl, hm⟩,
   use k,
   rw even_iff_two_dvd at hm,
-  rw [perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply,
+  rw [nat.perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply,
     is_multiplicative_sigma.map_mul_of_coprime (nat.prime_two.coprime_pow_of_not_dvd hm).symm,
     sigma_two_pow_eq_mersenne_succ, ← mul_assoc, ← pow_succ] at perf,
   rcases nat.coprime.dvd_of_dvd_mul_left
     (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)) (dvd.intro _ perf) with ⟨j, rfl⟩,
   rw [← mul_assoc, mul_comm _ (mersenne _), mul_assoc] at perf,
   have h := mul_left_cancel₀ (ne_of_gt (mersenne_pos (nat.succ_pos _))) perf,
-  rw [sigma_one_apply, sum_divisors_eq_sum_proper_divisors_add_self, ← succ_mersenne, add_mul,
+  rw [sigma_one_apply, nat.sum_divisors_eq_sum_proper_divisors_add_self, ← succ_mersenne, add_mul,
     one_mul, add_comm] at h,
   have hj := add_left_cancel h,
-  cases sum_proper_divisors_dvd (by { rw hj, apply dvd.intro_left (mersenne (k + 1)) rfl }),
+  cases nat.sum_proper_divisors_dvd (by { rw hj, apply dvd.intro_left (mersenne (k + 1)) rfl }),
   { have j1 : j = 1 := eq.trans hj.symm h_1,
-    rw [j1, mul_one, sum_proper_divisors_eq_one_iff_prime] at h_1,
+    rw [j1, mul_one, nat.sum_proper_divisors_eq_one_iff_prime] at h_1,
     simp [h_1, j1] },
   { have jcon := eq.trans hj.symm h_1,
     rw [← one_mul j, ← mul_assoc, mul_one] at jcon,
@@ -108,21 +110,24 @@ begin
         rw [← jcon2, one_mul],
         exact even_iff_two_dvd.mp ev },
       apply ne_of_lt _ jcon2,
-      rw [mersenne, ← nat.pred_eq_sub_one, lt_pred_iff, ← pow_one (nat.succ 1)],
+      rw [mersenne, ← nat.pred_eq_sub_one, nat.lt_pred_iff, ← pow_one (nat.succ 1)],
       apply pow_lt_pow (nat.lt_succ_self 1) (nat.succ_lt_succ (nat.succ_pos k)) },
     contrapose! hm,
     simp [hm] }
 end
 
 /-- The Euclid-Euler theorem characterizing even perfect numbers -/
 theorem even_and_perfect_iff {n : ℕ} :
-  (even n ∧ perfect n) ↔ ∃ (k : ℕ), prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) :=
+  (even n ∧ nat.perfect n) ↔
+    ∃ (k : ℕ), nat.prime (mersenne (k + 1)) ∧ n = 2 ^ k * mersenne (k + 1) :=
 begin
   split,
   { rintro ⟨ev, perf⟩,
-    exact eq_two_pow_mul_prime_mersenne_of_even_perfect ev perf },
+    exact nat.eq_two_pow_mul_prime_mersenne_of_even_perfect ev perf },
   { rintro ⟨k, pr, rfl⟩,
     exact ⟨even_two_pow_mul_mersenne_of_prime k pr, perfect_two_pow_mul_mersenne_of_prime k pr⟩ }
 end
 
 end nat
+
+end theorems_100

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -26,6 +26,8 @@ variables {α : Type*} [linear_order α] {β : Type*}
 open function finset
 open_locale classical
 
+namespace theorems_100
+
 /--
 **Erdős–Szekeres Theorem**: Given a sequence of more than `r * s` distinct values, there is an
 increasing sequence of length longer than `r` or a decreasing sequence of length longer than `s`.
@@ -158,3 +160,5 @@ begin
   -- Which follows from considering the cardinalities of the subset above, since `ab` is injective.
   simpa [nat.succ_injective, card_image_of_injective, ‹injective ab›] using card_le_of_subset this,
 end
+
+end theorems_100

archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean

@@ -42,6 +42,8 @@ open_locale big_operators
 open_locale classical
 open filter finset
 
+namespace theorems_100
+
 /--
 The primes in `(k, x]`.
 -/
@@ -246,3 +248,5 @@ begin
   ...          < x / 2 + x / 2               : add_lt_add_of_lt_of_le h3 h4
   ...          = x                           : add_halves ↑x,
 end
+
+end theorems_100

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -18,6 +18,8 @@ http://www.alaricstephen.com/main-featured/2017/9/28/cubing-a-cube-proof
 
 open real set function fin
 
+namespace theorems_100
+
 noncomputable theory
 
 namespace «82»
@@ -520,3 +522,5 @@ begin
 end
 
 end «82»
+
+end theorems_100

archive/100-theorems-list/83_friendship_graphs.lean

@@ -39,6 +39,8 @@ be phrased in terms of counting walks.
 -/
 
 open_locale classical big_operators
+namespace theorems_100
+
 noncomputable theory
 
 open finset simple_graph matrix
@@ -144,7 +146,7 @@ begin
   use G.degree v,
   intro x,
   by_cases hvx : G.adj v x, swap, { exact (degree_eq_of_not_adj hG hvx).symm, },
-  dunfold exists_politician at hG',
+  dunfold theorems_100.exists_politician at hG',
   push_neg at hG',
   rcases hG' v with ⟨w, hvw', hvw⟩,
   rcases hG' x with ⟨y, hxy', hxy⟩,
@@ -336,3 +338,5 @@ begin
   { exact npG (hG.exists_politician_of_degree_le_two dreg (nat.lt_succ_iff.mp dle2)) },
   { exact hG.false_of_three_le_degree dreg dge3 },
 end
+
+end theorems_100

archive/100-theorems-list/93_birthday_problem.lean

@@ -17,6 +17,8 @@ in terms of injective functions. The general result about `fintype.card (α ↪
 uses is `fintype.card_embedding_eq`.
 -/
 
+namespace theorems_100
+
 local notation (name := finset.card)  `|` x `|` := finset.card x
 local notation (name := fintype.card) `‖` x `‖` := fintype.card x
 
@@ -75,3 +77,5 @@ begin
 end
 
 end measure_theory
+
+end theorems_100

archive/100-theorems-list/9_area_of_a_circle.lean

@@ -43,6 +43,8 @@ to the n-ball.
 open set real measure_theory interval_integral
 open_locale real nnreal
 
+namespace theorems_100
+
 /-- A disc of radius `r` is defined as the collection of points `(p.1, p.2)` in `ℝ × ℝ` such that
   `p.1 ^ 2 + p.2 ^ 2 < r ^ 2`.
   Note that this definition is not equivalent to `metric.ball (0 : ℝ × ℝ) r`. This was done
@@ -115,3 +117,5 @@ begin
                          hcont hderiv (continuous_const.mul hf).continuous_on.interval_integrable
   ... = nnreal.pi * r ^ 2 : by norm_num [F, inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π],
 end
+
+end theorems_100

archive/examples/prop_encodable.lean

@@ -24,6 +24,8 @@ We mark the auxiliary constructions `private`, since their only purpose is to
 show encodability.
 -/
 
+namespace prop_encodable
+
 /-- Propositional formulas with labels from `α`. -/
 inductive prop_form (α : Type*)
 | var : α → prop_form
@@ -96,3 +98,5 @@ begin
 end
 
 end prop_form
+
+end prop_encodable

archive/imo/imo1959_q1.lean

@@ -18,6 +18,8 @@ as saying the numerator and denominator are relatively prime.
 
 open nat
 
+namespace imo
+
 lemma calculation (n k : ℕ) (h1 : k ∣ 21 * n + 4) (h2 : k ∣ 14 * n + 3) : k ∣ 1 :=
 have h3 : k ∣ 2 * (21 * n + 4), from h1.mul_left 2,
 have h4 : k ∣ 3 * (14 * n + 3), from h2.mul_left 3,
@@ -26,3 +28,5 @@ have h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1, by ring,
 
 theorem imo1959_q1 : ∀ n : ℕ, coprime (21 * n + 4) (14 * n + 3) :=
 assume n, coprime_of_dvd' $ λ k hp h1 h2, calculation n k h1 h2
+
+end imo

archive/imo/imo1962_q4.lean

@@ -17,6 +17,8 @@ in fact the simplest form of the set of solutions, and then prove it equals the
 
 open real
 open_locale real
+namespace imo
+
 noncomputable theory
 
 def problem_equation (x : ℝ) : Prop := cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1
@@ -129,3 +131,5 @@ calc problem_equation x
     ↔ cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1 : by refl
 ... ↔ cos (2 * x) = 0 ∨ cos (3 * x) = 0 : by simp [cos_two_mul, cos_three_mul, formula]
 ... ↔ x ∈ solution_set : by { rw [solve_cos2x_0, solve_cos3x_0, ← exists_or_distrib], refl }
+
+end imo

archive/imo/imo1972_q5.lean

@@ -15,6 +15,8 @@ Problem: `f` and `g` are real-valued functions defined on the real line. For all
 Prove that `|g(x)| ≤ 1` for all `x`.
 -/
 
+namespace imo
+
 /--
 This proof begins by introducing the supremum of `f`, `k ≤ 1` as well as `k' = k / ‖g y‖`. We then
 suppose that the conclusion does not hold (`hneg`) and show that `k ≤ k'` (by
@@ -120,3 +122,5 @@ begin
     ... ≤ 2 * k                     : by linarith [h (x+y), h (x -y)] },
   linarith,
 end
+
+end imo

archive/imo/imo1975_q1.lean

@@ -31,6 +31,8 @@ variables (hx : antitone_on x (finset.Icc 1 n))
 variables (hy : antitone_on y (finset.Icc 1 n))
 include hx hy hσ
 
+namespace imo
+
 theorem IMO_1975_Q1 :
   ∑ i in finset.Icc 1 n, (x i - y i) ^ 2 ≤ ∑ i in finset.Icc 1 n, (x i - y (σ i)) ^ 2 :=
 begin
@@ -46,3 +48,5 @@ begin
   -- them being `decreasing`
   exact antitone_on.monovary_on hx hy
 end
+
+end imo

archive/imo/imo1977_q6.lean

@@ -15,6 +15,8 @@ We first prove the problem statement for `f : ℕ → ℕ`
 then we use it to prove the statement for positive naturals.
 -/
 
+namespace imo
+
 theorem imo1977_q6_nat (f : ℕ → ℕ) (h : ∀ n, f (f n) < f (n + 1)) :
   ∀ n, f n = n :=
 begin
@@ -42,3 +44,5 @@ begin
     { simp },
     { simpa using h _ } }
 end
+
+end imo

archive/imo/imo1988_q6.lean

@@ -25,6 +25,8 @@ To illustrate the technique, we also prove a similar result.
 
 -- open_locale classical
 
+namespace imo
+
 local attribute [instance] classical.prop_decidable
 local attribute [simp] sq
 
@@ -296,3 +298,5 @@ begin
       obtain rfl|rfl := (nat.dvd_prime nat.prime_two).mp y_dvd; apply mul_left_cancel₀,
       exacts [one_ne_zero, h.symm, two_ne_zero, h.symm] } }
 end
+
+end imo

archive/imo/imo1994_q1.lean

@@ -32,6 +32,8 @@ open_locale big_operators
 
 open finset
 
+namespace imo
+
 lemma tedious (m : ℕ) (k : fin (m+1)) : m - (m + (m + 1 - ↑k)) % (m + 1) = ↑k  :=
 begin
   cases k with k hk,
@@ -97,3 +99,5 @@ begin
   -- A set of size `k+1` embed in one of size `k`, which yields a contradiction
   simpa [fin.coe_sub, tedious] using card_le_of_subset hf,
 end
+
+end imo

archive/imo/imo1998_q2.lean

@@ -38,6 +38,8 @@ Rearranging gives the result.
 -/
 
 open_locale classical
+namespace imo
+
 noncomputable theory
 
 /-- An ordered pair of judges. -/
@@ -212,3 +214,5 @@ begin
   { simp, },
   { exact le_of_mul_le_mul_right h z.succ_pos, },
 end
+
+end imo