merge

Author: kim-em

Archive.lean

@@ -74,7 +74,6 @@ import Archive.Wiedijk100Theorems.FriendshipGraphs
 import Archive.Wiedijk100Theorems.HeronsFormula
 import Archive.Wiedijk100Theorems.InverseTriangleSum
 import Archive.Wiedijk100Theorems.Konigsberg
-import Archive.Wiedijk100Theorems.Partition
 import Archive.Wiedijk100Theorems.PerfectNumbers
 import Archive.Wiedijk100Theorems.SolutionOfCubicQuartic
 import Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges

Archive/Wiedijk100Theorems/Partition.lean

@@ -220,6 +220,11 @@ def odds (n : ℕ) : Finset n.Partition := restricted n (¬ Even ·)
 def distincts (n : ℕ) : Finset n.Partition :=
   Finset.univ.filter fun c => c.parts.Nodup
 
+theorem countRestricted_two (n : ℕ) : countRestricted n 2 = distincts n := by
+  congrm Finset.univ.filter fun x ↦ ?_
+  rw [Multiset.nodup_iff_count_le_one]
+  grind [Multiset.count_eq_zero]
+
 /-- The finset of those partitions in which every part is odd and used at most once. -/
 def oddDistincts (n : ℕ) : Finset n.Partition :=
   odds n ∩ distincts n

Mathlib/Combinatorics/Enumerative/Partition/Basic.lean

@@ -17,6 +17,16 @@ times.
 
 ## Main declarations
 * `Nat.Partition.card_restricted_eq_card_countRestricted`: Glaisher's theorem.
+* `Nat.Partition.card_odds_eq_card_distincts`: Euler's partition theorem, a special case
+  of Glaisher's theorem when `m = 2`. This is also Theorem 45 from the
+  [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
+
+## Proof outline
+
+The proof is based on the generating functions for `restricted` and `countRestricted` partitions,
+which turn out to be equal:
+
+$$\prod_{i=1,i\nmid m}^\infty\frac{1}{1-X^i}=\prod_{i=0}^\infty (1+X^{i+1}+\cdots+X^{(m-1)(i+1)})$$
 
 ## References
 https://en.wikipedia.org/wiki/Glaisher%27s_theorem
@@ -34,7 +44,7 @@ variable [CommSemiring R]
 
 /-- The generating function of `Nat.Partition.restricted n p` is
 $$
-\prod_{i \mem p} \sum_{j = 0}^{\infty} X^{ij}
+\prod_{i \in p} \sum_{j = 0}^{\infty} X^{ij}
 $$ -/
 theorem hasProd_powerSeriesMk_card_restricted [IsTopologicalSemiring R]
     (p : ℕ → Prop) [DecidablePred p] :
@@ -145,4 +155,8 @@ theorem card_restricted_eq_card_countRestricted (n : ℕ) {m : ℕ} (hm : 0 < m)
   simpa using PowerSeries.ext_iff.mp
     (powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted ℤ hm) n
 
+theorem card_odds_eq_card_distincts (n : ℕ) : #(odds n) = #(distincts n) := by
+  simp_rw [← countRestricted_two, odds, even_iff_two_dvd]
+  exact card_restricted_eq_card_countRestricted n (by norm_num)
+
 end Nat.Partition

Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean

@@ -47,7 +47,8 @@ See also the type `Lean.ReservedNameAction`, invocations of `registerReservedNam
 
 Note that metaprograms should not add public declarations when run in private scopes. Doing so would
 likely be a bug in the metaprogram. As such, we do not perform further checks for automatically
-generated declarations such as those in `isAutoDecl`.
+generated declarations such as those detected by `isAutoDecl` or `isInternalDetail`, which would
+wrongly exclude e.g. public declarations generated by `initialize`.
 -/
 
 meta section

Mathlib/Tactic/Linter/PrivateModule.lean

@@ -0,0 +1,17 @@
+module
+
+import Mathlib.Tactic.Linter.PrivateModule
+
+set_option linter.privateModule true
+
+open Lean
+
+-- Should not fire, since `initialize` creates a genuinely public declaration.
+initialize pure ()
+
+/- Check that we have indeed created a declaration, and aren't not linting just due to being an
+empty file: -/
+/-- info: [initFn✝] -/
+#guard_msgs in
+run_cmd do
+  logInfo m!"{(← getEnv).constants.map₂.toArray.map (MessageData.ofConstName ·.1)}"

MathlibTest/PrivateModuleLinter/initialize.lean

@@ -185,8 +185,8 @@
   authors: Chris Hughes
 45:
   title  : The Partition Theorem
-  authors: Bhavik Mehta and Aaron Anderson
-  decl   : Theorems100.partition_theorem
+  authors: Bhavik Mehta, Aaron Anderson, and Weiyi Wang
+  decl   : Nat.Partition.card_odds_eq_card_distincts
 46:
   title  : The Solution of the General Quartic Equation
   decl   : Theorems100.quartic_eq_zero_iff

docs/100.yaml

@@ -1300,8 +1300,8 @@ Q1077741:
 
 Q1082910:
   title: Euler's partition theorem
-  authors: Bhavik Mehta and Aaron Anderson
-  decl: Theorems100.partition_theorem
+  authors: Bhavik Mehta, Aaron Anderson, and Weiyi Wang
+  decl: Nat.Partition.card_odds_eq_card_distincts
 
 Q1095330:
   title: Apéry's theorem

docs/1000.yaml

@@ -373,7 +373,9 @@ Analysis:
     First Main Theorem of Value Distribution Theory: 'ValueDistribution.characteristic_sub_characteristic_inv_le'
 
   Distribution theory:
+    Test functions: 'TestFunction'
     Schwartz space: 'SchwartzMap'
+    Distributions: 'Distribution'
 
   Fourier analysis:
     Fourier transform as an integral: 'Real.fourier_eq'

docs/overview.yaml

@@ -586,13 +586,13 @@ Probability Theory:
 # 12.
 Distribution calculus:
   Spaces $\mathcal{D}(\R^d)$:
-    smooth functions with compact support on $\R^d$: ''
+    smooth functions with compact support on $\R^d$: 'TestFunction'
     stability by derivation: ''
     stability by multiplication by a smooth function: ''
     partitions of unity: ''
     constructing approximations of probability density functions in spaces of common functions (trig, exp, rational, log, etc): ''
   Distributions on $\R^d$:
-    definition of distributions: ''
+    definition of distributions: 'Distribution'
     locally integrable functions as distributions: ''
     derivative of a distribution: ''
     Dirac measures: ''