From 881001d5e73c33039de363d24de5d9a80c50d08b Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Fri, 13 Mar 2026 00:12:56 +0800 Subject: [PATCH 01/39] golf --- .../Martingale/OptionalStopping.lean | 46 ++++++++----------- 1 file changed, 18 insertions(+), 28 deletions(-) diff --git a/Mathlib/Probability/Martingale/OptionalStopping.lean b/Mathlib/Probability/Martingale/OptionalStopping.lean index da234414a4c02e..39807d2e95f038 100644 --- a/Mathlib/Probability/Martingale/OptionalStopping.lean +++ b/Mathlib/Probability/Martingale/OptionalStopping.lean @@ -8,6 +8,8 @@ module public import Mathlib.Probability.Notation public import Mathlib.Probability.Process.HittingTime public import Mathlib.Probability.Martingale.Basic +public import Mathlib.Probability.Independence.Basic +public import Mathlib.Probability.Moments.Variance /-! # Optional stopping theorem (fair game theorem) @@ -125,10 +127,10 @@ theorem smul_le_stoppedValue_hittingBtwn [IsFiniteMeasure μ] (hsub : Submarting (n : ℕ) : ε • μ {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω} ≤ ENNReal.ofReal (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, - stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ↑ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by + stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by have hn : Set.Icc 0 n = {k | k ≤ n} := by ext x; simp have : ∀ ω, ((ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) → - (ε : ℝ) ≤ stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ↑ε ≤ y} 0 n ω : ℕ)) ω := by + (ε : ℝ) ≤ stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω := by intro x hx simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx refine stoppedValue_hittingBtwn_mem ?_ @@ -137,7 +139,7 @@ theorem smul_le_stoppedValue_hittingBtwn [IsFiniteMeasure μ] (hsub : Submarting let ⟨j, hj₁, hj₂⟩ := hx ⟨j, hj₁, hj₂⟩ have h := setIntegral_ge_of_const_le_real (measurableSet_le measurable_const - (Finset.measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n))) + (measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n))) (measure_ne_top _ _) this (Integrable.integrableOn (hsub.integrable_stoppedValue (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici) (mod_cast hittingBtwn_le))) @@ -156,7 +158,7 @@ we have `ε • μ {ε ≤ f* n} ≤ ∫ ω in {ε ≤ f* n}, f n` where `f* n In some literature, the Doob's maximal inequality refers to what we call Doob's Lp inequality (which is a corollary of this lemma and will be proved in an upcoming PR). -/ theorem maximal_ineq [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnonneg : 0 ≤ f) {ε : ℝ≥0} - (n : ℕ) : ε • μ {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω} ≤ + (n : ℕ) : ε * μ {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω} ≤ ENNReal.ofReal (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, f n ω ∂μ) := by @@ -167,9 +169,9 @@ theorem maximal_ineq [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnon ENNReal.ofReal (μ[f n]) by have hadd : ENNReal.ofReal (∫ ω, f n ω ∂μ) = ENNReal.ofReal - (∫ ω in {ω | ↑ε ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, f n ω ∂μ) + + (∫ ω in {ω | ε ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, f n ω ∂μ) + ENNReal.ofReal - (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ↑ε}, + (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε}, f n ω ∂μ) := by rw [← ENNReal.ofReal_add, ← setIntegral_union] · rw [← setIntegral_univ] @@ -177,37 +179,29 @@ theorem maximal_ineq [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnon ext ω change (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ) ↔ _ simp only [le_or_gt, Set.mem_univ] - · rw [disjoint_iff_inf_le] - rintro ω ⟨hω₁, hω₂⟩ - change (ε : ℝ) ≤ _ at hω₁ - change _ < (ε : ℝ) at hω₂ - exact (not_le.2 hω₂) hω₁ - · exact measurableSet_lt (Finset.measurable_range_sup'' fun n _ => + · grind + · exact measurableSet_lt (measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const exacts [(hsub.integrable _).integrableOn, (hsub.integrable _).integrableOn, integral_nonneg (hnonneg _), integral_nonneg (hnonneg _)] rwa [hadd, ENNReal.add_le_add_iff_right ENNReal.ofReal_ne_top] at this calc - ε • μ {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω} + - ENNReal.ofReal - (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε}, - f n ω ∂μ) ≤ - ENNReal.ofReal + _ ≤ ENNReal.ofReal (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, - stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ↑ε ≤ y} 0 n ω : ℕ)) ω ∂μ) + + stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) + ENNReal.ofReal (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε}, - stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ↑ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by + stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by gcongr with ω hω · exact smul_le_stoppedValue_hittingBtwn hsub n · exact (hsub.integrable n).integrableOn · refine Integrable.integrableOn ?_ refine hsub.integrable_stoppedValue ?_ (fun ω ↦ mod_cast hittingBtwn_le ω) exact hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici - · exact nullMeasurableSet_lt (Finset.measurable_range_sup'' fun n _ ↦ + · exact nullMeasurableSet_lt (measurable_range_sup'' fun n _ ↦ (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)).aemeasurable aemeasurable_const rw [Set.mem_setOf_eq] at hω - have : hittingBtwn f {y : ℝ | ↑ε ≤ y} 0 n ω = n := by + have : hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω = n := by classical simp only [hittingBtwn, Set.mem_setOf_eq, ite_eq_right_iff, forall_exists_index, and_imp] intro m hm hεm @@ -217,19 +211,15 @@ theorem maximal_ineq [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnon refine le_of_eq ?_ congr _ = ENNReal.ofReal - (∫ ω, stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ↑ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by + (∫ ω, stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by rw [← ENNReal.ofReal_add, ← setIntegral_union] · rw [← setIntegral_univ (μ := μ)] convert rfl ext ω change _ ↔ (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ) simp only [le_or_gt, Set.mem_univ] - · rw [disjoint_iff_inf_le] - rintro ω ⟨hω₁, hω₂⟩ - change (ε : ℝ) ≤ _ at hω₁ - change _ < (ε : ℝ) at hω₂ - exact (not_le.2 hω₂) hω₁ - · exact measurableSet_lt (Finset.measurable_range_sup'' fun n _ => + · grind + · exact measurableSet_lt (measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const · exact Integrable.integrableOn (hsub.integrable_stoppedValue (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici) From 5d0fee42ca0a06b4e6481c4dac8506d286dfd62e Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Fri, 13 Mar 2026 00:23:40 +0800 Subject: [PATCH 02/39] . --- .../Martingale/OptionalStopping.lean | 2 -- deriv.lean | 26 +++++++++++++++++++ 2 files changed, 26 insertions(+), 2 deletions(-) create mode 100644 deriv.lean diff --git a/Mathlib/Probability/Martingale/OptionalStopping.lean b/Mathlib/Probability/Martingale/OptionalStopping.lean index 39807d2e95f038..b705d02fdcfa53 100644 --- a/Mathlib/Probability/Martingale/OptionalStopping.lean +++ b/Mathlib/Probability/Martingale/OptionalStopping.lean @@ -8,8 +8,6 @@ module public import Mathlib.Probability.Notation public import Mathlib.Probability.Process.HittingTime public import Mathlib.Probability.Martingale.Basic -public import Mathlib.Probability.Independence.Basic -public import Mathlib.Probability.Moments.Variance /-! # Optional stopping theorem (fair game theorem) diff --git a/deriv.lean b/deriv.lean new file mode 100644 index 00000000000000..f796eedfb79a75 --- /dev/null +++ b/deriv.lean @@ -0,0 +1,26 @@ +import Mathlib + +variable + {𝕜 : Type*} [NontriviallyNormedField 𝕜] + {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] + {n : ℕ} {x : 𝕜} {s : Set 𝕜} {f g : 𝕜 → F} + {R : Type*} [DistribSMul R F] [inst : SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] + -- * `𝕝`: division semiring. (Addition in `𝕝` is not used, so the results would work with a + -- `GroupWithZero` if we had a `DistribSMulWithZero` typeclass.) + {𝕝 : Type*} [DivisionSemiring 𝕝] [Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] + -- * `𝔸`: normed `𝕜`-algebra. + +lemma iteratedFDerivWithin_comp_neg' (a : 𝕜) : iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a + = (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by + induction n generalizing a with + | zero => simp [iteratedFDerivWithin] + | succ n ih => + have ih' : iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s + = fun a ↦ (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by + ext b + rw [ih b] + rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left, + Function.comp_apply, Function.comp_apply, ih', ← Pi.smul_def, + fderivWithin_const_smul_field' ((-1 : 𝕜) ^ n) + (f := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) (-a)), fderivWithin_comp_neg a, + ← neg_one_smul 𝕜 (fderivWithin 𝕜 _ (-s) (-a)), ← mul_smul _ (-1), ← pow_succ (-1) n, map_smul] From 55ce23caf5408564540d3a5115ca07a44cc853f8 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Fri, 13 Mar 2026 00:25:34 +0800 Subject: [PATCH 03/39] . --- deriv.lean | 26 -------------------------- 1 file changed, 26 deletions(-) delete mode 100644 deriv.lean diff --git a/deriv.lean b/deriv.lean deleted file mode 100644 index f796eedfb79a75..00000000000000 --- a/deriv.lean +++ /dev/null @@ -1,26 +0,0 @@ -import Mathlib - -variable - {𝕜 : Type*} [NontriviallyNormedField 𝕜] - {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] - {n : ℕ} {x : 𝕜} {s : Set 𝕜} {f g : 𝕜 → F} - {R : Type*} [DistribSMul R F] [inst : SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] - -- * `𝕝`: division semiring. (Addition in `𝕝` is not used, so the results would work with a - -- `GroupWithZero` if we had a `DistribSMulWithZero` typeclass.) - {𝕝 : Type*} [DivisionSemiring 𝕝] [Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] - -- * `𝔸`: normed `𝕜`-algebra. - -lemma iteratedFDerivWithin_comp_neg' (a : 𝕜) : iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a - = (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by - induction n generalizing a with - | zero => simp [iteratedFDerivWithin] - | succ n ih => - have ih' : iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s - = fun a ↦ (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by - ext b - rw [ih b] - rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left, - Function.comp_apply, Function.comp_apply, ih', ← Pi.smul_def, - fderivWithin_const_smul_field' ((-1 : 𝕜) ^ n) - (f := fun a ↦ iteratedFDerivWithin 𝕜 n f (-s) (-a)), fderivWithin_comp_neg a, - ← neg_one_smul 𝕜 (fderivWithin 𝕜 _ (-s) (-a)), ← mul_smul _ (-1), ← pow_succ (-1) n, map_smul] From ce6514f0d8067abf5d2d0625727219f0f00460b8 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Fri, 13 Mar 2026 00:34:36 +0800 Subject: [PATCH 04/39] . --- Mathlib/Probability/Martingale/OptionalStopping.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/Probability/Martingale/OptionalStopping.lean b/Mathlib/Probability/Martingale/OptionalStopping.lean index b705d02fdcfa53..199f7399cc38d5 100644 --- a/Mathlib/Probability/Martingale/OptionalStopping.lean +++ b/Mathlib/Probability/Martingale/OptionalStopping.lean @@ -126,13 +126,12 @@ theorem smul_le_stoppedValue_hittingBtwn [IsFiniteMeasure μ] (hsub : Submarting ENNReal.ofReal (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by - have hn : Set.Icc 0 n = {k | k ≤ n} := by ext x; simp have : ∀ ω, ((ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) → (ε : ℝ) ≤ stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω := by intro x hx simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx refine stoppedValue_hittingBtwn_mem ?_ - simp only [Set.mem_setOf_eq, hn] + simp only [Set.mem_Icc, zero_le, true_and, Set.mem_setOf_eq] exact let ⟨j, hj₁, hj₂⟩ := hx ⟨j, hj₁, hj₂⟩ @@ -200,8 +199,7 @@ theorem maximal_ineq [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnon (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)).aemeasurable aemeasurable_const rw [Set.mem_setOf_eq] at hω have : hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω = n := by - classical simp only [hittingBtwn, Set.mem_setOf_eq, - ite_eq_right_iff, forall_exists_index, and_imp] + simp only [hittingBtwn, Set.mem_setOf_eq, ite_eq_right_iff, forall_exists_index, and_imp] intro m hm hεm exact False.elim ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩)) From 51897b9f8da5049d4f8ababd06fa4c8ceafb9c0e Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 2 Apr 2026 23:58:50 +0800 Subject: [PATCH 05/39] golf TrapezoidalRule.lean --- .../IntervalIntegral/TrapezoidalRule.lean | 56 +++++++------------ 1 file changed, 21 insertions(+), 35 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean index 886bffdc0ca5e3..ed84e09b9f6827 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean @@ -118,7 +118,6 @@ the general error bound later on. -/ private lemma trapezoidal_error_le_of_lt' {f : ℝ → ℝ} {ζ : ℝ} {a b : ℝ} (a_lt_b : a < b) (h_df : DifferentiableOn ℝ f (Icc a b)) (h_ddf : DifferentiableOn ℝ (derivWithin f (Icc a b)) (Icc a b)) - (h_ddf_integrable : IntervalIntegrable (iteratedDerivWithin 2 f (Icc a b)) volume a b) (fpp_bound : ∀ x, |iteratedDerivWithin 2 f (Icc a b) x| ≤ ζ) : |trapezoidal_error f 1 a b| ≤ (b - a) ^ 3 * ζ / 12 := by rw [mul_div_assoc, mul_comm] @@ -155,26 +154,20 @@ private lemma trapezoidal_error_le_of_lt' {f : ℝ → ℝ} {ζ : ℝ} {a b : simp_rw [pow_one, ddg, abs_mul, abs_div, abs_two] grw [fpp_bound x, abs_of_nonneg (sub_nonneg.mpr hx.1), div_mul_comm] have key {φ φ' : ℝ → ℝ} (h : ∀ x ∈ Icc a b, HasDerivWithinAt φ (φ' x) (Icc a b) x) (h0 : φ a = 0) - {c : ℝ} {n : ℕ} (h_bound : ∀ t ∈ Icc a b, |φ' t| ≤ c * (t - a) ^ n) - (hφ' : IntervalIntegrable φ' volume a b) : + {c : ℝ} {n : ℕ} (h_bound : ∀ t ∈ Icc a b, |φ' t| ≤ c * (t - a) ^ n) : ∀ t ∈ Icc a b, |φ t| ≤ c / (n + 1) * (t - a) ^ (n + 1) := by intro t ht - have hs : Icc a t ⊆ Icc a b := Icc_subset_Icc_right ht.2 - have hs' : Ioo a t ⊆ Ioo a b := Ioo_subset_Ioo_right ht.2 - have hs'' : uIcc a t ⊆ uIcc a b := by rwa [uIcc_of_lt a_lt_b, uIcc_of_le ht.1] - replace hφ' := hφ'.mono hs'' le_rfl - have key := integral_eq_sub_of_hasDerivAt_of_le (f := φ) (f' := φ') ht.1 - (fun x hx ↦ (h x (hs hx)).continuousWithinAt.mono hs) - (fun x hx ↦ (h x (hs (mem_Icc_of_Ioo hx))).hasDerivAt (Icc_mem_nhds_iff.mpr (hs' hx))) hφ' - rw [h0, sub_zero] at key - grw [← key, abs_integral_le_integral_abs ht.1, integral_mono_on ht.1 hφ'.abs - (Continuous.intervalIntegrable (by fun_prop) a t) fun x hx ↦ h_bound x (hs hx), - integral_comp_sub_right (c * · ^ n), ← mul_div_right_comm, mul_div_assoc] - simp - have bound_dg := key h_ddg (by ring) bound_ddg (h_ddf_integrable.continuousOn_mul (by fun_prop)) - have bound_g := key h_dg (trapezoidal_error_eq f 1 a) bound_dg - (ContinuousOn.intervalIntegrable_of_Icc a_lt_b.le fun x hx ↦ (h_ddg x hx).continuousWithinAt) - exact (bound_g b ⟨a_lt_b.le, le_rfl⟩).trans_eq (by ring_nf) + have hB : ∀ x, HasDerivAt (fun y ↦ c / (n + 1) * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x := by + intro x + convert (hasDerivAt_const x (c / (n + 1))).mul + (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1)) using 1 + · simp [sub_eq_add_neg, field] + simpa [Real.norm_eq_abs, h0] using image_norm_le_of_norm_deriv_right_le_deriv_boundary + (fun x hx ↦ (h x hx).continuousWithinAt) + (fun x hx ↦ by grind [Icc_mem_nhdsGE_of_mem, mono_of_mem_nhdsWithin]) + (by simp [h0]) hB (fun x hx ↦ h_bound x (Ico_subset_Icc_self hx)) ht + exact (key h_dg (trapezoidal_error_eq f 1 a) (key h_ddg (by ring) bound_ddg) b + ⟨a_lt_b.le, le_rfl⟩).trans_eq (by ring_nf) set_option linter.style.whitespace false in -- manual alignment is not recognised /-- The hard part of the trapezoidal rule error bound: proving it in the case of a non-empty closed @@ -183,7 +176,6 @@ on. -/ private lemma trapezoidal_error_le_of_lt {f : ℝ → ℝ} {ζ : ℝ} {a b : ℝ} (a_lt_b : a < b) (h_df : DifferentiableOn ℝ f (Icc a b)) (h_ddf : DifferentiableOn ℝ (derivWithin f (Icc a b)) (Icc a b)) - (h_ddf_integrable : IntervalIntegrable (iteratedDerivWithin 2 f (Icc a b)) volume a b) (fpp_bound : ∀ x, |iteratedDerivWithin 2 f (Icc a b) x| ≤ ζ) {N : ℕ} (N_nonzero : 0 < N) : |trapezoidal_error f N a b| ≤ (b - a) ^ 3 * ζ / (12 * N ^ 2) := by @@ -208,48 +200,44 @@ private lemma trapezoidal_error_le_of_lt {f : ℝ → ℝ} {ζ : ℝ} {a b : ℝ have h2 : ak (k + 1) ≤ b := by simp only [ak, hb]; grw [Nat.lt_iff_add_one_le.mp hk] have h3 : Icc (ak k) (ak (k + 1)) ⊆ Icc a b := Icc_subset_Icc h1 h2 have h4 : ak k < ak (k + 1) := by rwa [← sub_pos, h0] - have h5 : EqOn (derivWithin f (Icc a b)) - (derivWithin f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by - intro x hx - rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))] have h6 : EqOn (iteratedDerivWithin 2 f (Icc a b)) (iteratedDerivWithin 2 f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by intro x hx simp only [iteratedDerivWithin_succ', iteratedDerivWithin_zero] rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_ddf x (h3 hx))] - exact derivWithin_congr h5 (h5 hx) + exact derivWithin_congr + (fun y hy ↦ by + rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 y hy) (h_df y (h3 hy))]) + (by rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))]) have h7 (x : ℝ) : |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ := by by_cases hx : x ∈ Icc (ak k) (ak (k + 1)) · grw [← h6 hx, fpp_bound] · rw [iteratedDerivWithin_succ, derivWithin_zero_of_notMem_closure (by rwa [closure_Icc]), abs_zero] exact (abs_nonneg _).trans (fpp_bound 0) - refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ ?_ h7).trans_eq ?_ + refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h7).trans_eq ?_ · refine h_ddf.congr_mono (fun x hx ↦ ?_) h3 exact derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx)) - · exact (h_ddf_integrable.mono_set (by rwa [Set.uIcc_of_lt h4, Set.uIcc_of_lt a_lt_b])).congr - (h6.mono (Set.uIoc_subset_uIcc.trans_eq (Set.uIcc_of_lt h4))) · rw [h0, mul_div_assoc, mul_comm] /-- The standard error bound for trapezoidal integration on the general interval `[[a, b]]`. -/ theorem trapezoidal_error_le {f : ℝ → ℝ} {a b : ℝ} (h_df : DifferentiableOn ℝ f [[a, b]]) - (h_ddf : DifferentiableOn ℝ (derivWithin f [[a, b]]) [[a, b]]) - (h_ddf_integrable : IntervalIntegrable (iteratedDerivWithin 2 f [[a, b]]) volume a b) {ζ : ℝ} + (h_ddf : DifferentiableOn ℝ (derivWithin f [[a, b]]) [[a, b]]) {ζ : ℝ} (fpp_bound : ∀ x, |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ) {N : ℕ} (N_nonzero : 0 < N) : |trapezoidal_error f N a b| ≤ |b - a| ^ 3 * ζ / (12 * N ^ 2) := by rcases lt_trichotomy a b with h_lt | h_eq | h_gt -- Standard case: a < b · rw [uIcc_of_lt h_lt] at * rw [abs_of_pos (sub_pos.mpr h_lt)] - exact trapezoidal_error_le_of_lt h_lt h_df h_ddf h_ddf_integrable fpp_bound N_nonzero + exact trapezoidal_error_le_of_lt h_lt h_df h_ddf fpp_bound N_nonzero -- Trivial case: a = b · simp [h_eq] -- Slightly trickier case: a > b (requires flipping the direction and sign of the true and -- approximate integrals) · rw [uIcc_of_gt h_gt] at * rw [abs_of_neg (sub_neg.mpr h_gt), neg_sub, trapezoidal_error_symm f N_nonzero a b, abs_neg] - exact trapezoidal_error_le_of_lt h_gt h_df h_ddf h_ddf_integrable.symm fpp_bound N_nonzero + exact trapezoidal_error_le_of_lt h_gt h_df h_ddf fpp_bound N_nonzero /-- The error bound for trapezoidal integration in the slightly weaker, but very common, case where `f` is `C^2`. -/ @@ -267,6 +255,4 @@ theorem trapezoidal_error_le_of_c2 {f : ℝ → ℝ} {a b : ℝ} (h_f_c2 : ContD have h_ddf : DifferentiableOn ℝ (derivWithin f [[a, b]]) [[a, b]] := by rw [← iteratedDerivWithin_one] exact ContDiffOn.differentiableOn_iteratedDerivWithin h_f_c2 (by norm_cast) ud - have h_ddf_integrable : IntervalIntegrable (iteratedDerivWithin 2 f [[a, b]]) volume a b := - (ContDiffOn.continuousOn_iteratedDerivWithin h_f_c2 (le_refl 2) ud).intervalIntegrable - exact trapezoidal_error_le h_df h_ddf h_ddf_integrable fpp_bound N_nonzero + exact trapezoidal_error_le h_df h_ddf fpp_bound N_nonzero From b8c6c9b6b18a4dc10bb38c170aa5ea36a65cde67 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 3 Apr 2026 00:13:16 +0800 Subject: [PATCH 06/39] remove useless unfold --- .../IntervalIntegral/TrapezoidalRule.lean | 22 +++++++++---------- 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean index ed84e09b9f6827..3a696382c91e2a 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean @@ -169,7 +169,6 @@ private lemma trapezoidal_error_le_of_lt' {f : ℝ → ℝ} {ζ : ℝ} {a b : exact (key h_dg (trapezoidal_error_eq f 1 a) (key h_ddg (by ring) bound_ddg) b ⟨a_lt_b.le, le_rfl⟩).trans_eq (by ring_nf) -set_option linter.style.whitespace false in -- manual alignment is not recognised /-- The hard part of the trapezoidal rule error bound: proving it in the case of a non-empty closed interval with ordered endpoints. This lemma is used in the proof of the general error bound later on. -/ @@ -184,7 +183,7 @@ private lemma trapezoidal_error_le_of_lt {f : ℝ → ℝ} {ζ : ℝ} {a b : ℝ have h0 : ∀ k : ℕ, ak (k + 1) - ak k = h := by simp [ak, ← sub_mul] have hab : 0 < b - a := sub_pos.mpr a_lt_b have hpos : 0 < h := by positivity - have hb : b = a + N * h := by unfold h; field + have hb : b = a + N * h := by field rw [hb, ← sum_trapezoidal_error_adjacent_intervals N_nonzero (hb ▸ h_df.continuousOn.intervalIntegrable_of_Icc a_lt_b.le)] grw [abs_sum_le_sum_abs] @@ -193,14 +192,14 @@ private lemma trapezoidal_error_le_of_lt {f : ℝ → ℝ} {ζ : ℝ} {a b : ℝ calc _ ≤ ∑ k ∈ range N, ζ / 12 * h ^ 3 := sum_le_sum this _ = N * (ζ / 12 * h ^ 3) := by simp [sum_const] - _ = _ := by unfold h; push_cast; field + _ = _ := by push_cast; field intro k hk rw [Finset.mem_range] at hk have h1 : a ≤ ak k := by simp only [ak, le_add_iff_nonneg_right]; positivity have h2 : ak (k + 1) ≤ b := by simp only [ak, hb]; grw [Nat.lt_iff_add_one_le.mp hk] have h3 : Icc (ak k) (ak (k + 1)) ⊆ Icc a b := Icc_subset_Icc h1 h2 have h4 : ak k < ak (k + 1) := by rwa [← sub_pos, h0] - have h6 : EqOn (iteratedDerivWithin 2 f (Icc a b)) + have h5 : EqOn (iteratedDerivWithin 2 f (Icc a b)) (iteratedDerivWithin 2 f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by intro x hx simp only [iteratedDerivWithin_succ', iteratedDerivWithin_zero] @@ -209,13 +208,13 @@ private lemma trapezoidal_error_le_of_lt {f : ℝ → ℝ} {ζ : ℝ} {a b : ℝ (fun y hy ↦ by rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 y hy) (h_df y (h3 hy))]) (by rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))]) - have h7 (x : ℝ) : |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ := by + have h6 (x : ℝ) : |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ := by by_cases hx : x ∈ Icc (ak k) (ak (k + 1)) - · grw [← h6 hx, fpp_bound] + · grw [← h5 hx, fpp_bound] · rw [iteratedDerivWithin_succ, derivWithin_zero_of_notMem_closure (by rwa [closure_Icc]), abs_zero] exact (abs_nonneg _).trans (fpp_bound 0) - refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h7).trans_eq ?_ + refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h6).trans_eq ?_ · refine h_ddf.congr_mono (fun x hx ↦ ?_) h3 exact derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx)) · rw [h0, mul_div_assoc, mul_comm] @@ -251,8 +250,7 @@ theorem trapezoidal_error_le_of_c2 {f : ℝ → ℝ} {a b : ℝ} (h_f_c2 : ContD -- Once we have a ≠ b, all the necessary assumptions on f follow pretty quickly from its being -- C^2. have ud : UniqueDiffOn ℝ [[a, b]] := uniqueDiffOn_Icc (inf_lt_sup.mpr h_ne) - have h_df : DifferentiableOn ℝ f [[a, b]] := ContDiffOn.differentiableOn h_f_c2 two_ne_zero - have h_ddf : DifferentiableOn ℝ (derivWithin f [[a, b]]) [[a, b]] := by - rw [← iteratedDerivWithin_one] - exact ContDiffOn.differentiableOn_iteratedDerivWithin h_f_c2 (by norm_cast) ud - exact trapezoidal_error_le h_df h_ddf fpp_bound N_nonzero + refine trapezoidal_error_le (ContDiffOn.differentiableOn h_f_c2 two_ne_zero) ?_ fpp_bound + N_nonzero + rw [← iteratedDerivWithin_one] + exact ContDiffOn.differentiableOn_iteratedDerivWithin h_f_c2 (by norm_cast) ud From 22eec38b6e7d7ef3bb4c0e0d29111ec4127e8075 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 3 Apr 2026 00:32:53 +0800 Subject: [PATCH 07/39] revert change --- .../IntervalIntegral/TrapezoidalRule.lean | 26 ++++++++++--------- 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean index 3a696382c91e2a..5a61aec2d87c3e 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean @@ -199,22 +199,23 @@ private lemma trapezoidal_error_le_of_lt {f : ℝ → ℝ} {ζ : ℝ} {a b : ℝ have h2 : ak (k + 1) ≤ b := by simp only [ak, hb]; grw [Nat.lt_iff_add_one_le.mp hk] have h3 : Icc (ak k) (ak (k + 1)) ⊆ Icc a b := Icc_subset_Icc h1 h2 have h4 : ak k < ak (k + 1) := by rwa [← sub_pos, h0] - have h5 : EqOn (iteratedDerivWithin 2 f (Icc a b)) + have h5 : EqOn (derivWithin f (Icc a b)) + (derivWithin f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by + intro x hx + rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))] + have h6 : EqOn (iteratedDerivWithin 2 f (Icc a b)) (iteratedDerivWithin 2 f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by intro x hx simp only [iteratedDerivWithin_succ', iteratedDerivWithin_zero] rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_ddf x (h3 hx))] - exact derivWithin_congr - (fun y hy ↦ by - rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 y hy) (h_df y (h3 hy))]) - (by rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))]) - have h6 (x : ℝ) : |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ := by + exact derivWithin_congr h5 (h5 hx) + have h7 (x : ℝ) : |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ := by by_cases hx : x ∈ Icc (ak k) (ak (k + 1)) - · grw [← h5 hx, fpp_bound] + · grw [← h6 hx, fpp_bound] · rw [iteratedDerivWithin_succ, derivWithin_zero_of_notMem_closure (by rwa [closure_Icc]), abs_zero] exact (abs_nonneg _).trans (fpp_bound 0) - refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h6).trans_eq ?_ + refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h7).trans_eq ?_ · refine h_ddf.congr_mono (fun x hx ↦ ?_) h3 exact derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx)) · rw [h0, mul_div_assoc, mul_comm] @@ -250,7 +251,8 @@ theorem trapezoidal_error_le_of_c2 {f : ℝ → ℝ} {a b : ℝ} (h_f_c2 : ContD -- Once we have a ≠ b, all the necessary assumptions on f follow pretty quickly from its being -- C^2. have ud : UniqueDiffOn ℝ [[a, b]] := uniqueDiffOn_Icc (inf_lt_sup.mpr h_ne) - refine trapezoidal_error_le (ContDiffOn.differentiableOn h_f_c2 two_ne_zero) ?_ fpp_bound - N_nonzero - rw [← iteratedDerivWithin_one] - exact ContDiffOn.differentiableOn_iteratedDerivWithin h_f_c2 (by norm_cast) ud + have h_df : DifferentiableOn ℝ f [[a, b]] := ContDiffOn.differentiableOn h_f_c2 two_ne_zero + have h_ddf : DifferentiableOn ℝ (derivWithin f [[a, b]]) [[a, b]] := by + rw [← iteratedDerivWithin_one] + exact ContDiffOn.differentiableOn_iteratedDerivWithin h_f_c2 (by norm_cast) ud + exact trapezoidal_error_le h_df h_ddf fpp_bound N_nonzero From 159794da970a81de74f302801dc4b292dfe33e3c Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 3 Apr 2026 01:18:08 +0800 Subject: [PATCH 08/39] Update Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com> --- .../Integral/IntervalIntegral/TrapezoidalRule.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean index 5a61aec2d87c3e..7b9f1657ed9c6c 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean @@ -157,11 +157,10 @@ private lemma trapezoidal_error_le_of_lt' {f : ℝ → ℝ} {ζ : ℝ} {a b : {c : ℝ} {n : ℕ} (h_bound : ∀ t ∈ Icc a b, |φ' t| ≤ c * (t - a) ^ n) : ∀ t ∈ Icc a b, |φ t| ≤ c / (n + 1) * (t - a) ^ (n + 1) := by intro t ht - have hB : ∀ x, HasDerivAt (fun y ↦ c / (n + 1) * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x := by - intro x + have hB (x) : HasDerivAt (fun y ↦ c / (n + 1) * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x := by convert (hasDerivAt_const x (c / (n + 1))).mul (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1)) using 1 - · simp [sub_eq_add_neg, field] + simp [sub_eq_add_neg, field] simpa [Real.norm_eq_abs, h0] using image_norm_le_of_norm_deriv_right_le_deriv_boundary (fun x hx ↦ (h x hx).continuousWithinAt) (fun x hx ↦ by grind [Icc_mem_nhdsGE_of_mem, mono_of_mem_nhdsWithin]) From f50d287813db56882b9cd6144869107aafc38860 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 6 Apr 2026 13:15:33 +0800 Subject: [PATCH 09/39] init --- Mathlib/Combinatorics/Enumerative/Bell.lean | 238 ++++++++++++++++++++ 1 file changed, 238 insertions(+) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 51de56b170f4f0..294ec05834f74e 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -5,6 +5,7 @@ Authors: Antoine Chambert-Loir, María-Inés de Frutos—Fernández, Yu Shao, Be -/ module +public import Mathlib.Combinatorics.Enumerative.Partition.Basic public import Mathlib.Data.Nat.Choose.Multinomial /-! # Bell numbers for multisets @@ -119,6 +120,66 @@ theorem bell_eq (m : Multiset ℕ) : · apply Finset.prod_pos exact fun _ _ ↦ Nat.factorial_pos _ +theorem prod_count_factorial_eq_count_factorial_mul_prod_erase + {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : + ∏ j ∈ m.toFinset.erase 0, (m.count j)! = + (m.count a)! * ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by + by_cases hmem : a ∈ m.toFinset.erase 0 + · rw [← Finset.mul_prod_erase _ _ hmem] + · rw [Finset.erase_eq_of_notMem hmem] + have hcount : m.count a = 0 := by + apply Multiset.count_eq_zero_of_notMem + intro hm + exact hmem <| by simpa [ha] using hm + simp [hcount] + +theorem prod_count_factorial_cons_erase {m : Multiset ℕ} {a : ℕ} : + ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! = + ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by + have hset : ((a ::ₘ m).toFinset.erase 0).erase a = (m.toFinset.erase 0).erase a := by + ext x + by_cases hx : x = a + · simp [hx] + · simp [Multiset.toFinset_cons, hx] + rw [hset] + refine Finset.prod_congr rfl ?_ + intro j hj + simp [(Finset.mem_erase.mp hj).1] + +theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)).prod := by + simpa only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, + forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ + +theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : + (a ::ₘ m).bell * (a ::ₘ m).count a = Nat.choose (m.sum + a) a * m.bell := by + let rest := ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! + let c := a ! * ((m.map (fun j ↦ j !)).prod * ((m.count a)! * rest)) + have hm0 : m.bell * ((m.map (fun j ↦ j !)).prod * ((m.count a)! * rest)) = m.sum ! := by + have hm := Multiset.bell_mul_eq m + rw [prod_count_factorial_eq_count_factorial_mul_prod_erase (a := a) ha] at hm + simpa [rest, mul_assoc, mul_comm, mul_left_comm] using hm + have hm : m.bell * c = m.sum ! * a ! := by + simpa [c, mul_assoc, mul_comm, mul_left_comm] using congrArg (fun t => a ! * t) hm0 + have ha_mem : a ∈ (a ::ₘ m).toFinset.erase 0 := by + simp [ha] + have hc : 0 < c := Nat.mul_pos (Nat.factorial_pos _) <| + Nat.mul_pos (map_factorial_prod_pos m) <| by positivity + apply Nat.eq_of_mul_eq_mul_right hc + calc + _ = (a ::ₘ m).bell * ((m.count a + 1) * c) := by + simp [mul_assoc] + _ = (m.sum + a)! := by + have hq := Multiset.bell_mul_eq (a ::ₘ m) + rw [← Finset.mul_prod_erase _ _ ha_mem, prod_count_factorial_cons_erase] at hq + simpa [c, rest, Nat.factorial_succ, Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, + add_comm, mul_assoc, mul_comm, mul_left_comm] using hq + _ = Nat.choose (m.sum + a) a * (m.sum ! * a !) := by + rw [← Nat.add_choose_mul_factorial_mul_factorial] + ring + _ = Nat.choose (m.sum + a) a * (m.bell * c) := by rw [hm] + _ = (Nat.choose (m.sum + a) a * m.bell) * c := by + simp [mul_assoc, mul_comm, mul_left_comm] + end Multiset namespace Nat @@ -211,4 +272,181 @@ theorem bell_one : Nat.bell 1 = 1 := by theorem bell_two : Nat.bell 2 = 2 := by simp [Nat.bell] +private theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : + ∑ a ∈ p.parts.toFinset, Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a) = + Multiset.bell p.parts := by + apply Nat.eq_of_mul_eq_mul_left (Nat.succ_pos n) + calc + (n + 1) * (∑ a ∈ p.parts.toFinset, Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) + = ∑ a ∈ p.parts.toFinset, + (n + 1) * (Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by + rw [Finset.mul_sum] + _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * Multiset.bell p.parts) := by + refine Finset.sum_congr rfl ?_ + intro a ha + have ha_mem : a ∈ p.parts := by simpa using ha + have ha0 : a ≠ 0 := by + intro h + exact (p.parts_pos ha_mem).ne' h + have hsum : (p.parts.erase a).sum + a = n + 1 := by + simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) + have hbell : + Nat.choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by + simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using + (Multiset.bell_cons_mul_count (m := p.parts.erase a) (a := a) ha0).symm + calc + (n + 1) * (Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) + = ((n + 1) * Nat.choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring + _ = (Nat.choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by + have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) + rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel ha1] + _ = a * (Nat.choose (n + 1) a * Multiset.bell (p.parts.erase a)) := by ring + _ = a * (p.parts.count a * Multiset.bell p.parts) := by rw [hbell] + _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * Multiset.bell p.parts := by + rw [Finset.sum_mul] + refine Finset.sum_congr rfl ?_ + intro a ha + ring + _ = (n + 1) * Multiset.bell p.parts := by + have hsum : ∑ a ∈ p.parts.toFinset, p.parts.count a * a = n + 1 := by + simpa [smul_eq_mul, p.parts_sum, mul_comm] using + (Finset.sum_multiset_count (s := p.parts)).symm + rw [hsum] + +private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1) : + {p : Nat.Partition (n + 1) // a ∈ p.parts} ≃ Nat.Partition (n + 1 - a) where + toFun p := by + refine ⟨p.1.parts.erase a, ?_, ?_⟩ + · intro i hi + exact p.1.parts_pos (Multiset.erase_subset a p.1.parts hi) + · have hs : a + (p.1.parts.erase a).sum = n + 1 := by + simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) + omega + invFun q := by + refine ⟨⟨a ::ₘ q.parts, ?_, ?_⟩, by simp⟩ + · intro i hi + rw [Multiset.mem_cons] at hi + rcases hi with rfl | hi + · exact ha1 + · exact q.parts_pos hi + · simp [q.parts_sum, ha] + left_inv p := by + apply Subtype.ext + apply Nat.Partition.ext + change a ::ₘ p.1.parts.erase a = p.1.parts + exact Multiset.cons_erase p.2 + right_inv q := by + apply Nat.Partition.ext + change (a ::ₘ q.parts).erase a = q.parts + exact Multiset.erase_cons_head a q.parts + +private def partitionPartEquiv (n : ℕ) : + (Σ p : Nat.Partition (n + 1), {a // a ∈ p.parts.toFinset}) ≃ + Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a) where + toFun x := by + let a : ℕ := x.2 + have ha_mem : a ∈ x.1.parts := by + dsimp [a] + exact Multiset.mem_toFinset.mp x.2.2 + have ha1 : 1 ≤ a := Nat.succ_le_of_lt (x.1.parts_pos ha_mem) + have ha_le : a ≤ n + 1 := Nat.Partition.le_of_mem_parts ha_mem + exact ⟨⟨a, by simp [ha1, ha_le]⟩, partitionWithPartEquiv ha1 ha_le ⟨x.1, ha_mem⟩⟩ + invFun x := by + rcases x with ⟨⟨a, ha⟩, q⟩ + simp only [Finset.mem_Icc] at ha + let p : Nat.Partition (n + 1) := (partitionWithPartEquiv ha.1 ha.2).symm q + refine ⟨p, ⟨a, by simpa using ((partitionWithPartEquiv ha.1 ha.2).symm q).2⟩⟩ + left_inv x := by + rcases x with ⟨p, ⟨a, ha⟩⟩ + have ha_mem : a ∈ p.parts := Multiset.mem_toFinset.mp ha + have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) + have ha_le : a ≤ n + 1 := Nat.Partition.le_of_mem_parts ha_mem + simpa using congrArg + (fun y : {p : Nat.Partition (n + 1) // a ∈ p.parts} => + (⟨y.1, ⟨a, by simpa using y.2⟩⟩ : + Σ p : Nat.Partition (n + 1), {a // a ∈ p.parts.toFinset})) + ((partitionWithPartEquiv ha1 ha_le).left_inv ⟨p, ha_mem⟩) + right_inv x := by + rcases x with ⟨⟨a, ha⟩, q⟩ + simp only [Finset.mem_Icc] at ha + simpa only using + congrArg + (fun q : Nat.Partition (n + 1 - a) => + (⟨⟨a, by simpa only⟩, q⟩ : + Σ a : { a : ℕ // a ∈ Finset.Icc 1 (n + 1) }, Nat.Partition (n + 1 - a))) + ((partitionWithPartEquiv ha.1 ha.2).right_inv q) + +private def finSuccEquivIcc (n : ℕ) : + Fin n.succ ≃ {a : ℕ // a ∈ Finset.Icc 1 (n + 1)} where + toFun i := ⟨i + 1, by + simp [Finset.mem_Icc, Nat.le_of_lt_succ i.is_lt]⟩ + invFun a := ⟨a - 1, by + rcases a with ⟨a, ha⟩ + simp only [Finset.mem_Icc] at ha + have hle : a - 1 + 1 ≤ n + 1 := by simpa [Nat.sub_add_cancel ha.1] using ha.2 + exact lt_of_lt_of_le (Nat.lt_succ_self (a - 1)) hle⟩ + left_inv i := by + ext + exact Nat.add_sub_cancel_right i 1 + right_inv a := by + rcases a with ⟨a, ha⟩ + ext + simp only [Finset.mem_Icc] at ha + exact Nat.sub_add_cancel ha.1 + +theorem bell_eq_sum_partition (n : ℕ) : + Nat.bell n = ∑ p : Nat.Partition n, Multiset.bell p.parts := by + classical + refine Nat.strong_induction_on n ?_ + intro n ih + cases n with + | zero => simp + | succ n => + symm + calc + _ = ∑ p : Nat.Partition (n + 1), + ∑ a ∈ p.parts.toFinset, Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a) := by + congr with p + exact (bell_eq_sum_erase p).symm + _ = ∑ p : Nat.Partition (n + 1), + ∑ a : {a // a ∈ p.parts.toFinset}, + Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a) := by + congr with p + rw [← Finset.sum_coe_sort] + _ = ∑ x : Σ p : Nat.Partition (n + 1), {a // a ∈ p.parts.toFinset}, + Nat.choose n (x.2 - 1) * Multiset.bell (x.1.parts.erase x.2) := by + simpa using + (Fintype.sum_sigma' + (fun p : Nat.Partition (n + 1) => + fun a : {a // a ∈ p.parts.toFinset} => + Nat.choose n ((a : ℕ) - 1) * Multiset.bell (p.parts.erase a))).symm + _ = ∑ y : Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a), + Nat.choose n (y.1 - 1) * Multiset.bell y.2.parts := by + exact Fintype.sum_equiv (partitionPartEquiv n) + (fun x => Nat.choose n (x.2 - 1) * Multiset.bell (x.1.parts.erase x.2)) + (fun y => Nat.choose n (y.1 - 1) * Multiset.bell y.2.parts) (by + intro x + dsimp [partitionPartEquiv, partitionWithPartEquiv]) + _ = ∑ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, + ∑ q : Nat.Partition (n + 1 - a), Nat.choose n (a - 1) * Multiset.bell q.parts := by + simpa using + (Fintype.sum_sigma' + (fun a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)} => + fun q : Nat.Partition (n + 1 - (a : ℕ)) => + Nat.choose n ((a : ℕ) - 1) * Multiset.bell q.parts)) + _ = ∑ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, + Nat.choose n (a - 1) * ∑ q : Nat.Partition (n + 1 - a), Multiset.bell q.parts := by + congr with a + rw [← Finset.mul_sum] + _ = ∑ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, + Nat.choose n (a - 1) * Nat.bell (n + 1 - a) := by + congr with a + grind + _ = ∑ i : Fin n.succ, Nat.choose n i * Nat.bell (n - i) := by + simpa [finSuccEquivIcc] using + ((finSuccEquivIcc n).sum_comp + (fun a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)} => + Nat.choose n (a - 1) * Nat.bell (n + 1 - a))).symm + _ = Nat.bell (n + 1) := by rw [Nat.bell_succ] + end Nat From 6f71d3a24b53187d6b360851bf473b6a6536faf2 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 6 Apr 2026 15:24:08 +0800 Subject: [PATCH 10/39] snapshot --- Mathlib/Combinatorics/Enumerative/Bell.lean | 115 ++++++++++++-------- 1 file changed, 67 insertions(+), 48 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 294ec05834f74e..fae2fb8ca07e8b 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -277,41 +277,40 @@ private theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : Multiset.bell p.parts := by apply Nat.eq_of_mul_eq_mul_left (Nat.succ_pos n) calc - (n + 1) * (∑ a ∈ p.parts.toFinset, Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) - = ∑ a ∈ p.parts.toFinset, - (n + 1) * (Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by - rw [Finset.mul_sum] + _ = ∑ a ∈ p.parts.toFinset, + (n + 1) * (Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by + rw [Finset.mul_sum] _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * Multiset.bell p.parts) := by - refine Finset.sum_congr rfl ?_ - intro a ha - have ha_mem : a ∈ p.parts := by simpa using ha - have ha0 : a ≠ 0 := by - intro h - exact (p.parts_pos ha_mem).ne' h - have hsum : (p.parts.erase a).sum + a = n + 1 := by - simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) - have hbell : - Nat.choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by - simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using - (Multiset.bell_cons_mul_count (m := p.parts.erase a) (a := a) ha0).symm - calc - (n + 1) * (Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) - = ((n + 1) * Nat.choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring - _ = (Nat.choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by - have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) - rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel ha1] - _ = a * (Nat.choose (n + 1) a * Multiset.bell (p.parts.erase a)) := by ring - _ = a * (p.parts.count a * Multiset.bell p.parts) := by rw [hbell] + refine Finset.sum_congr rfl ?_ + intro a ha + have ha_mem : a ∈ p.parts := by simpa using ha + have ha0 : a ≠ 0 := by + intro h + exact (p.parts_pos ha_mem).ne' h + have hsum : (p.parts.erase a).sum + a = n + 1 := by + simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) + have hbell : + Nat.choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by + simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using + (Multiset.bell_cons_mul_count (m := p.parts.erase a) (a := a) ha0).symm + calc + (n + 1) * (Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) + = ((n + 1) * Nat.choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring + _ = (Nat.choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by + have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) + rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel ha1] + _ = a * (Nat.choose (n + 1) a * Multiset.bell (p.parts.erase a)) := by ring + _ = a * (p.parts.count a * Multiset.bell p.parts) := by rw [hbell] _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * Multiset.bell p.parts := by - rw [Finset.sum_mul] - refine Finset.sum_congr rfl ?_ - intro a ha - ring + rw [Finset.sum_mul] + refine Finset.sum_congr rfl ?_ + intro a ha + ring _ = (n + 1) * Multiset.bell p.parts := by - have hsum : ∑ a ∈ p.parts.toFinset, p.parts.count a * a = n + 1 := by - simpa [smul_eq_mul, p.parts_sum, mul_comm] using - (Finset.sum_multiset_count (s := p.parts)).symm - rw [hsum] + have hsum : ∑ a ∈ p.parts.toFinset, p.parts.count a * a = n + 1 := by + simpa [smul_eq_mul, p.parts_sum, mul_comm] using + (Finset.sum_multiset_count (s := p.parts)).symm + rw [hsum] private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1) : {p : Nat.Partition (n + 1) // a ∈ p.parts} ≃ Nat.Partition (n + 1 - a) where @@ -394,6 +393,19 @@ private def finSuccEquivIcc (n : ℕ) : simp only [Finset.mem_Icc] at ha exact Nat.sub_add_cancel ha.1 +private def finPartitionEquiv (n : ℕ) : + (Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a)) ≃ + Σ i : Fin n.succ, Nat.Partition (n - i) := + (Equiv.sigmaCongrLeft' (finSuccEquivIcc n).symm).trans <| + Equiv.sigmaCongrRight fun i => + Equiv.cast <| by + simp [finSuccEquivIcc] + +private theorem bell_parts_cast_symm {m n : ℕ} (h : m = n) (p : Nat.Partition n) : + Multiset.bell (((Equiv.cast (congrArg Nat.Partition h)).symm p).parts) = Multiset.bell p.parts := by + cases h + rfl + theorem bell_eq_sum_partition (n : ℕ) : Nat.bell n = ∑ p : Nat.Partition n, Multiset.bell p.parts := by classical @@ -427,26 +439,33 @@ theorem bell_eq_sum_partition (n : ℕ) : (fun y => Nat.choose n (y.1 - 1) * Multiset.bell y.2.parts) (by intro x dsimp [partitionPartEquiv, partitionWithPartEquiv]) - _ = ∑ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, - ∑ q : Nat.Partition (n + 1 - a), Nat.choose n (a - 1) * Multiset.bell q.parts := by + _ = ∑ z : Σ i : Fin n.succ, Nat.Partition (n - i), + (fun y : Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a) => + Nat.choose n (y.1 - 1) * Multiset.bell y.2.parts) ((finPartitionEquiv n).symm z) := by + symm + exact ((finPartitionEquiv n).symm).sum_comp + (fun y : Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a) => + Nat.choose n (y.1 - 1) * Multiset.bell y.2.parts) + _ = ∑ z : Σ i : Fin n.succ, Nat.Partition (n - i), + Nat.choose n z.1 * Multiset.bell z.2.parts := by + congr with z + rcases z with ⟨i, q⟩ + dsimp [finPartitionEquiv, finSuccEquivIcc, Equiv.sigmaCongrLeft', Equiv.sigmaCongrLeft, + Equiv.sigmaCongrRight] + rw [bell_parts_cast_symm (p := q)] + simp + _ = ∑ i : Fin n.succ, ∑ q : Nat.Partition (n - i), Nat.choose n i * Multiset.bell q.parts := by simpa using (Fintype.sum_sigma' - (fun a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)} => - fun q : Nat.Partition (n + 1 - (a : ℕ)) => - Nat.choose n ((a : ℕ) - 1) * Multiset.bell q.parts)) - _ = ∑ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, - Nat.choose n (a - 1) * ∑ q : Nat.Partition (n + 1 - a), Multiset.bell q.parts := by - congr with a + (fun i : Fin n.succ => + fun q : Nat.Partition (n - i) => + Nat.choose n i * Multiset.bell q.parts)) + _ = ∑ i : Fin n.succ, Nat.choose n i * ∑ q : Nat.Partition (n - i), Multiset.bell q.parts := by + congr with i rw [← Finset.mul_sum] - _ = ∑ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, - Nat.choose n (a - 1) * Nat.bell (n + 1 - a) := by - congr with a - grind _ = ∑ i : Fin n.succ, Nat.choose n i * Nat.bell (n - i) := by - simpa [finSuccEquivIcc] using - ((finSuccEquivIcc n).sum_comp - (fun a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)} => - Nat.choose n (a - 1) * Nat.bell (n + 1 - a))).symm + congr with i + rw [ih (n - i) (Nat.lt_succ_of_le (Nat.sub_le _ _))] _ = Nat.bell (n + 1) := by rw [Nat.bell_succ] end Nat From 2f8b763438fa5e6584d76c79107907e3cf331c98 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 6 Apr 2026 15:49:59 +0800 Subject: [PATCH 11/39] cleanup --- Mathlib/Combinatorics/Enumerative/Bell.lean | 182 ++------------------ 1 file changed, 17 insertions(+), 165 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index fae2fb8ca07e8b..6d6df45bf99f30 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -272,7 +272,7 @@ theorem bell_one : Nat.bell 1 = 1 := by theorem bell_two : Nat.bell 2 = 2 := by simp [Nat.bell] -private theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : +theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : ∑ a ∈ p.parts.toFinset, Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a) = Multiset.bell p.parts := by apply Nat.eq_of_mul_eq_mul_left (Nat.succ_pos n) @@ -281,191 +281,43 @@ private theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : (n + 1) * (Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by rw [Finset.mul_sum] _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * Multiset.bell p.parts) := by - refine Finset.sum_congr rfl ?_ - intro a ha - have ha_mem : a ∈ p.parts := by simpa using ha - have ha0 : a ≠ 0 := by - intro h - exact (p.parts_pos ha_mem).ne' h + refine Finset.sum_congr rfl fun a ha => ?_ + have ha_mem : a ∈ p.parts := mem_dedup.mp ha + have ha0 : a ≠ 0 := fun h ↦ LT.lt.ne' (p.parts_pos ha_mem) h have hsum : (p.parts.erase a).sum + a = n + 1 := by simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) have hbell : Nat.choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using - (Multiset.bell_cons_mul_count (m := p.parts.erase a) (a := a) ha0).symm + (Multiset.bell_cons_mul_count (m := p.parts.erase a) ha0).symm calc - (n + 1) * (Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) - = ((n + 1) * Nat.choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring + _ = ((n + 1) * Nat.choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring _ = (Nat.choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by - have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) - rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel ha1] - _ = a * (Nat.choose (n + 1) a * Multiset.bell (p.parts.erase a)) := by ring - _ = a * (p.parts.count a * Multiset.bell p.parts) := by rw [hbell] + have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) + rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel ha1] + _ = _ := by grind _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * Multiset.bell p.parts := by - rw [Finset.sum_mul] - refine Finset.sum_congr rfl ?_ - intro a ha - ring - _ = (n + 1) * Multiset.bell p.parts := by + grind [Finset.sum_mul] + _ = _ := by have hsum : ∑ a ∈ p.parts.toFinset, p.parts.count a * a = n + 1 := by - simpa [smul_eq_mul, p.parts_sum, mul_comm] using - (Finset.sum_multiset_count (s := p.parts)).symm + simpa [smul_eq_mul, p.parts_sum, mul_comm] using (Finset.sum_multiset_count p.parts).symm rw [hsum] private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1) : {p : Nat.Partition (n + 1) // a ∈ p.parts} ≃ Nat.Partition (n + 1 - a) where toFun p := by refine ⟨p.1.parts.erase a, ?_, ?_⟩ - · intro i hi + · intro _ hi exact p.1.parts_pos (Multiset.erase_subset a p.1.parts hi) · have hs : a + (p.1.parts.erase a).sum = n + 1 := by simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) omega - invFun q := by - refine ⟨⟨a ::ₘ q.parts, ?_, ?_⟩, by simp⟩ - · intro i hi - rw [Multiset.mem_cons] at hi - rcases hi with rfl | hi - · exact ha1 - · exact q.parts_pos hi - · simp [q.parts_sum, ha] - left_inv p := by - apply Subtype.ext - apply Nat.Partition.ext - change a ::ₘ p.1.parts.erase a = p.1.parts - exact Multiset.cons_erase p.2 - right_inv q := by - apply Nat.Partition.ext - change (a ::ₘ q.parts).erase a = q.parts - exact Multiset.erase_cons_head a q.parts - -private def partitionPartEquiv (n : ℕ) : - (Σ p : Nat.Partition (n + 1), {a // a ∈ p.parts.toFinset}) ≃ - Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a) where - toFun x := by - let a : ℕ := x.2 - have ha_mem : a ∈ x.1.parts := by - dsimp [a] - exact Multiset.mem_toFinset.mp x.2.2 - have ha1 : 1 ≤ a := Nat.succ_le_of_lt (x.1.parts_pos ha_mem) - have ha_le : a ≤ n + 1 := Nat.Partition.le_of_mem_parts ha_mem - exact ⟨⟨a, by simp [ha1, ha_le]⟩, partitionWithPartEquiv ha1 ha_le ⟨x.1, ha_mem⟩⟩ - invFun x := by - rcases x with ⟨⟨a, ha⟩, q⟩ - simp only [Finset.mem_Icc] at ha - let p : Nat.Partition (n + 1) := (partitionWithPartEquiv ha.1 ha.2).symm q - refine ⟨p, ⟨a, by simpa using ((partitionWithPartEquiv ha.1 ha.2).symm q).2⟩⟩ - left_inv x := by - rcases x with ⟨p, ⟨a, ha⟩⟩ - have ha_mem : a ∈ p.parts := Multiset.mem_toFinset.mp ha - have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) - have ha_le : a ≤ n + 1 := Nat.Partition.le_of_mem_parts ha_mem - simpa using congrArg - (fun y : {p : Nat.Partition (n + 1) // a ∈ p.parts} => - (⟨y.1, ⟨a, by simpa using y.2⟩⟩ : - Σ p : Nat.Partition (n + 1), {a // a ∈ p.parts.toFinset})) - ((partitionWithPartEquiv ha1 ha_le).left_inv ⟨p, ha_mem⟩) - right_inv x := by - rcases x with ⟨⟨a, ha⟩, q⟩ - simp only [Finset.mem_Icc] at ha - simpa only using - congrArg - (fun q : Nat.Partition (n + 1 - a) => - (⟨⟨a, by simpa only⟩, q⟩ : - Σ a : { a : ℕ // a ∈ Finset.Icc 1 (n + 1) }, Nat.Partition (n + 1 - a))) - ((partitionWithPartEquiv ha.1 ha.2).right_inv q) - -private def finSuccEquivIcc (n : ℕ) : - Fin n.succ ≃ {a : ℕ // a ∈ Finset.Icc 1 (n + 1)} where - toFun i := ⟨i + 1, by - simp [Finset.mem_Icc, Nat.le_of_lt_succ i.is_lt]⟩ - invFun a := ⟨a - 1, by - rcases a with ⟨a, ha⟩ - simp only [Finset.mem_Icc] at ha - have hle : a - 1 + 1 ≤ n + 1 := by simpa [Nat.sub_add_cancel ha.1] using ha.2 - exact lt_of_lt_of_le (Nat.lt_succ_self (a - 1)) hle⟩ - left_inv i := by - ext - exact Nat.add_sub_cancel_right i 1 - right_inv a := by - rcases a with ⟨a, ha⟩ - ext - simp only [Finset.mem_Icc] at ha - exact Nat.sub_add_cancel ha.1 - -private def finPartitionEquiv (n : ℕ) : - (Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a)) ≃ - Σ i : Fin n.succ, Nat.Partition (n - i) := - (Equiv.sigmaCongrLeft' (finSuccEquivIcc n).symm).trans <| - Equiv.sigmaCongrRight fun i => - Equiv.cast <| by - simp [finSuccEquivIcc] - -private theorem bell_parts_cast_symm {m n : ℕ} (h : m = n) (p : Nat.Partition n) : - Multiset.bell (((Equiv.cast (congrArg Nat.Partition h)).symm p).parts) = Multiset.bell p.parts := by - cases h - rfl + invFun q := ⟨⟨a ::ₘ q.parts, by grind, by simp [q.parts_sum, ha]⟩, by simp⟩ + left_inv p := Subtype.ext <| Partition.ext <| cons_erase p.property + right_inv q := Partition.ext <| erase_cons_head a q.parts theorem bell_eq_sum_partition (n : ℕ) : Nat.bell n = ∑ p : Nat.Partition n, Multiset.bell p.parts := by - classical - refine Nat.strong_induction_on n ?_ - intro n ih - cases n with - | zero => simp - | succ n => - symm - calc - _ = ∑ p : Nat.Partition (n + 1), - ∑ a ∈ p.parts.toFinset, Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a) := by - congr with p - exact (bell_eq_sum_erase p).symm - _ = ∑ p : Nat.Partition (n + 1), - ∑ a : {a // a ∈ p.parts.toFinset}, - Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a) := by - congr with p - rw [← Finset.sum_coe_sort] - _ = ∑ x : Σ p : Nat.Partition (n + 1), {a // a ∈ p.parts.toFinset}, - Nat.choose n (x.2 - 1) * Multiset.bell (x.1.parts.erase x.2) := by - simpa using - (Fintype.sum_sigma' - (fun p : Nat.Partition (n + 1) => - fun a : {a // a ∈ p.parts.toFinset} => - Nat.choose n ((a : ℕ) - 1) * Multiset.bell (p.parts.erase a))).symm - _ = ∑ y : Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a), - Nat.choose n (y.1 - 1) * Multiset.bell y.2.parts := by - exact Fintype.sum_equiv (partitionPartEquiv n) - (fun x => Nat.choose n (x.2 - 1) * Multiset.bell (x.1.parts.erase x.2)) - (fun y => Nat.choose n (y.1 - 1) * Multiset.bell y.2.parts) (by - intro x - dsimp [partitionPartEquiv, partitionWithPartEquiv]) - _ = ∑ z : Σ i : Fin n.succ, Nat.Partition (n - i), - (fun y : Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a) => - Nat.choose n (y.1 - 1) * Multiset.bell y.2.parts) ((finPartitionEquiv n).symm z) := by - symm - exact ((finPartitionEquiv n).symm).sum_comp - (fun y : Σ a : {a : ℕ // a ∈ Finset.Icc 1 (n + 1)}, Nat.Partition (n + 1 - a) => - Nat.choose n (y.1 - 1) * Multiset.bell y.2.parts) - _ = ∑ z : Σ i : Fin n.succ, Nat.Partition (n - i), - Nat.choose n z.1 * Multiset.bell z.2.parts := by - congr with z - rcases z with ⟨i, q⟩ - dsimp [finPartitionEquiv, finSuccEquivIcc, Equiv.sigmaCongrLeft', Equiv.sigmaCongrLeft, - Equiv.sigmaCongrRight] - rw [bell_parts_cast_symm (p := q)] - simp - _ = ∑ i : Fin n.succ, ∑ q : Nat.Partition (n - i), Nat.choose n i * Multiset.bell q.parts := by - simpa using - (Fintype.sum_sigma' - (fun i : Fin n.succ => - fun q : Nat.Partition (n - i) => - Nat.choose n i * Multiset.bell q.parts)) - _ = ∑ i : Fin n.succ, Nat.choose n i * ∑ q : Nat.Partition (n - i), Multiset.bell q.parts := by - congr with i - rw [← Finset.mul_sum] - _ = ∑ i : Fin n.succ, Nat.choose n i * Nat.bell (n - i) := by - congr with i - rw [ih (n - i) (Nat.lt_succ_of_le (Nat.sub_le _ _))] - _ = Nat.bell (n + 1) := by rw [Nat.bell_succ] + sorry end Nat From df1aded5a6f51284a08f6eb37bc79d4c33143d83 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 6 Apr 2026 16:15:29 +0800 Subject: [PATCH 12/39] finish proof --- Mathlib/Combinatorics/Enumerative/Bell.lean | 82 +++++++++++++++++---- 1 file changed, 67 insertions(+), 15 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 6d6df45bf99f30..7ce5c8f3252632 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -189,7 +189,7 @@ of `n`-element subsets. -/ def uniformBell (m n : ℕ) : ℕ := bell (replicate m n) theorem uniformBell_eq (m n : ℕ) : m.uniformBell n = - ∏ p ∈ (Finset.range m), Nat.choose (p * n + n - 1) (n - 1) := by + ∏ p ∈ (Finset.range m), choose (p * n + n - 1) (n - 1) := by unfold uniformBell bell rw [toFinset_replicate] split_ifs with hm @@ -239,24 +239,19 @@ theorem uniformBell_eq_div (m : ℕ) {n : ℕ} (hn : n ≠ 0) : /-- The `n`th standard Bell number, which counts the number of partitions of a set of cardinality `n`. - -## TODO - -Prove that `Nat.bell n` is equal to the sum of `Multiset.bell m` -over all multisets `m : Multiset ℕ` such that `m.sum = n`. -/ protected def bell : ℕ → ℕ | 0 => 1 | n + 1 => ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) theorem bell_succ (n : ℕ) : - Nat.bell (n + 1) = ∑ i : Fin n.succ, Nat.choose n i * Nat.bell (n - i) := by + Nat.bell (n + 1) = ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) := by rw [Nat.bell] theorem bell_succ' (n : ℕ) : - Nat.bell (n + 1) = ∑ ij ∈ Finset.antidiagonal n, Nat.choose n ij.1 * Nat.bell ij.2 := by + Nat.bell (n + 1) = ∑ ij ∈ Finset.antidiagonal n, choose n ij.1 * Nat.bell ij.2 := by rw [Nat.bell_succ, - Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => Nat.choose n x * Nat.bell y) n, + Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => choose n x * Nat.bell y) n, Finset.sum_range] @@ -273,12 +268,12 @@ theorem bell_two : Nat.bell 2 = 2 := by simp [Nat.bell] theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : - ∑ a ∈ p.parts.toFinset, Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a) = + ∑ a ∈ p.parts.toFinset, choose n (a - 1) * Multiset.bell (p.parts.erase a) = Multiset.bell p.parts := by apply Nat.eq_of_mul_eq_mul_left (Nat.succ_pos n) calc _ = ∑ a ∈ p.parts.toFinset, - (n + 1) * (Nat.choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by + (n + 1) * (choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by rw [Finset.mul_sum] _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * Multiset.bell p.parts) := by refine Finset.sum_congr rfl fun a ha => ?_ @@ -287,12 +282,12 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : have hsum : (p.parts.erase a).sum + a = n + 1 := by simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) have hbell : - Nat.choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by + choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using (Multiset.bell_cons_mul_count (m := p.parts.erase a) ha0).symm calc - _ = ((n + 1) * Nat.choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring - _ = (Nat.choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by + _ = ((n + 1) * choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring + _ = (choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel ha1] _ = _ := by grind @@ -316,8 +311,65 @@ private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1 left_inv p := Subtype.ext <| Partition.ext <| cons_erase p.property right_inv q := Partition.ext <| erase_cons_head a q.parts +private def sigmaPartitionWithPartEquiv (n : ℕ) : + (Σ i : Fin n.succ, {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}) ≃ + Σ p : Nat.Partition (n + 1), {a : ℕ // a ∈ p.parts.toFinset} where + toFun x := ⟨x.2.1, ⟨(x.1 + 1 : ℕ), by simpa using x.2.2⟩⟩ + invFun x := by + refine ⟨⟨x.2.1 - 1, by grind⟩, ⟨x.1, by grind⟩⟩ + left_inv x := by simp + right_inv x := by grind + +/-- `Nat.bell n` is equal to the sum of `Multiset.bell m` over all multisets `m : Multiset ℕ` such +that `m.sum = n`. -/ theorem bell_eq_sum_partition (n : ℕ) : Nat.bell n = ∑ p : Nat.Partition n, Multiset.bell p.parts := by - sorry + refine Nat.strong_induction_on n ?_ + intro n ih + cases n with + | zero => simp + | succ n => + rw [Nat.bell_succ] + calc + _ = ∑ i : Fin n.succ, ∑ q : Nat.Partition (n - i), choose n i * Multiset.bell q.parts := by + refine Fintype.sum_congr _ _ fun i => ?_ + rw [ih (n - i) (by omega)] + simpa using (Finset.mul_sum (⊤ : Finset (Nat.Partition (n - i))) + (fun q => Multiset.bell q.parts) (choose n i)) + _ = ∑ i : Fin n.succ, ∑ p : {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, + choose n i * Multiset.bell (p.1.parts.erase (i + 1)) := by + refine Fintype.sum_congr _ _ fun i => ?_ + have h1 : 1 ≤ (i + 1 : ℕ) := by omega + have h2 : (i + 1 : ℕ) ≤ n + 1 := by omega + have hsub : n + 1 - (i + 1 : ℕ) = n - i := by omega + have hEq : ∑ p : {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, + choose n i * Multiset.bell (p.1.parts.erase (i + 1)) + = ∑ q : Nat.Partition (n + 1 - (i + 1 : ℕ)), + choose n i * Multiset.bell q.parts := + (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) + (fun p => choose n i * Multiset.bell ((partitionWithPartEquiv h1 h2 p).parts)) + (fun q => choose n i * Multiset.bell q.parts) (fun _ => rfl)) + exact hsub ▸ Eq.symm hEq + _ = ∑ x : Σ i : Fin n.succ, {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, + choose n x.1 * Multiset.bell (x.2.1.parts.erase (x.1 + 1)) := by + rw [← Fintype.sum_sigma'] + _ = ∑ x : Σ p : Nat.Partition (n + 1), {a : ℕ // a ∈ p.parts.toFinset}, + choose n (x.2.1 - 1) * Multiset.bell (x.1.parts.erase x.2.1) := by + refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ + rintro ⟨i, p⟩ + simp [sigmaPartitionWithPartEquiv] + _ = ∑ p : Nat.Partition (n + 1), ∑ a : {a : ℕ // a ∈ p.parts.toFinset}, + choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1) := by + simpa using + (Fintype.sum_sigma' fun (p : Nat.Partition (n + 1)) + (a : {a : ℕ // a ∈ p.parts.toFinset}) => + choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1)) + _ = ∑ p : Nat.Partition (n + 1), + ∑ a ∈ p.parts.toFinset, choose n (a - 1) * Multiset.bell (p.parts.erase a) := by + refine Fintype.sum_congr _ _ fun p => ?_ + simpa using Finset.sum_coe_sort p.parts.toFinset + (f := fun a => choose n (a - 1) * Multiset.bell (p.parts.erase a)) + _ = ∑ p : Nat.Partition (n + 1), Multiset.bell p.parts := + Fintype.sum_congr _ _ fun p => bell_eq_sum_erase p end Nat From 052ae2dd0827a7d013fb65344bed57dd8c2cd279 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 6 Apr 2026 16:26:16 +0800 Subject: [PATCH 13/39] golf a bit --- Mathlib/Combinatorics/Enumerative/Bell.lean | 80 +++++++++------------ 1 file changed, 34 insertions(+), 46 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 7ce5c8f3252632..2f92edf9224739 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -272,31 +272,30 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : Multiset.bell p.parts := by apply Nat.eq_of_mul_eq_mul_left (Nat.succ_pos n) calc - _ = ∑ a ∈ p.parts.toFinset, - (n + 1) * (choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by - rw [Finset.mul_sum] - _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * Multiset.bell p.parts) := by - refine Finset.sum_congr rfl fun a ha => ?_ - have ha_mem : a ∈ p.parts := mem_dedup.mp ha - have ha0 : a ≠ 0 := fun h ↦ LT.lt.ne' (p.parts_pos ha_mem) h - have hsum : (p.parts.erase a).sum + a = n + 1 := by - simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) - have hbell : - choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by - simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using - (Multiset.bell_cons_mul_count (m := p.parts.erase a) ha0).symm - calc - _ = ((n + 1) * choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring - _ = (choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by - have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) - rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel ha1] - _ = _ := by grind - _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * Multiset.bell p.parts := by - grind [Finset.sum_mul] - _ = _ := by - have hsum : ∑ a ∈ p.parts.toFinset, p.parts.count a * a = n + 1 := by - simpa [smul_eq_mul, p.parts_sum, mul_comm] using (Finset.sum_multiset_count p.parts).symm - rw [hsum] + _ = ∑ a ∈ p.parts.toFinset, + (n + 1) * (choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by + rw [Finset.mul_sum] + _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * Multiset.bell p.parts) := by + refine Finset.sum_congr rfl fun a ha => ?_ + have ha_mem : a ∈ p.parts := mem_dedup.mp ha + have ha0 : a ≠ 0 := fun h ↦ LT.lt.ne' (p.parts_pos ha_mem) h + have hsum : (p.parts.erase a).sum + a = n + 1 := by + simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) + have hbell : choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by + simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using + (bell_cons_mul_count (m := p.parts.erase a) ha0).symm + calc + _ = ((n + 1) * choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring + _ = (choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by + have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) + rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel ha1] + _ = _ := by grind + _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * Multiset.bell p.parts := by + grind [Finset.sum_mul] + _ = _ := by + have hsum : ∑ a ∈ p.parts.toFinset, p.parts.count a * a = n + 1 := by + simpa [smul_eq_mul, p.parts_sum, mul_comm] using (Finset.sum_multiset_count p.parts).symm + rw [hsum] private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1) : {p : Nat.Partition (n + 1) // a ∈ p.parts} ≃ Nat.Partition (n + 1 - a) where @@ -333,43 +332,32 @@ theorem bell_eq_sum_partition (n : ℕ) : calc _ = ∑ i : Fin n.succ, ∑ q : Nat.Partition (n - i), choose n i * Multiset.bell q.parts := by refine Fintype.sum_congr _ _ fun i => ?_ - rw [ih (n - i) (by omega)] - simpa using (Finset.mul_sum (⊤ : Finset (Nat.Partition (n - i))) - (fun q => Multiset.bell q.parts) (choose n i)) + simpa [ih (n - i) (by omega)] using Finset.mul_sum (⊤ : Finset (Nat.Partition (n - i))) + (fun q => Multiset.bell q.parts) (choose n i) _ = ∑ i : Fin n.succ, ∑ p : {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, choose n i * Multiset.bell (p.1.parts.erase (i + 1)) := by refine Fintype.sum_congr _ _ fun i => ?_ have h1 : 1 ≤ (i + 1 : ℕ) := by omega have h2 : (i + 1 : ℕ) ≤ n + 1 := by omega have hsub : n + 1 - (i + 1 : ℕ) = n - i := by omega - have hEq : ∑ p : {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, - choose n i * Multiset.bell (p.1.parts.erase (i + 1)) - = ∑ q : Nat.Partition (n + 1 - (i + 1 : ℕ)), - choose n i * Multiset.bell q.parts := - (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) + exact hsub ▸ Eq.symm (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) (fun p => choose n i * Multiset.bell ((partitionWithPartEquiv h1 h2 p).parts)) (fun q => choose n i * Multiset.bell q.parts) (fun _ => rfl)) - exact hsub ▸ Eq.symm hEq _ = ∑ x : Σ i : Fin n.succ, {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, - choose n x.1 * Multiset.bell (x.2.1.parts.erase (x.1 + 1)) := by - rw [← Fintype.sum_sigma'] + choose n x.1 * Multiset.bell (x.2.1.parts.erase (x.1 + 1)) := by rw [← Fintype.sum_sigma'] _ = ∑ x : Σ p : Nat.Partition (n + 1), {a : ℕ // a ∈ p.parts.toFinset}, - choose n (x.2.1 - 1) * Multiset.bell (x.1.parts.erase x.2.1) := by - refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ - rintro ⟨i, p⟩ - simp [sigmaPartitionWithPartEquiv] + choose n (x.2.1 - 1) * Multiset.bell (x.1.parts.erase x.2.1) := + Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ (by simp [sigmaPartitionWithPartEquiv]) _ = ∑ p : Nat.Partition (n + 1), ∑ a : {a : ℕ // a ∈ p.parts.toFinset}, choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1) := by - simpa using - (Fintype.sum_sigma' fun (p : Nat.Partition (n + 1)) - (a : {a : ℕ // a ∈ p.parts.toFinset}) => - choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1)) + simpa using (Fintype.sum_sigma' fun (p : Nat.Partition (n + 1)) + (a : {a : ℕ // a ∈ p.parts.toFinset}) => + choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1)) _ = ∑ p : Nat.Partition (n + 1), ∑ a ∈ p.parts.toFinset, choose n (a - 1) * Multiset.bell (p.parts.erase a) := by refine Fintype.sum_congr _ _ fun p => ?_ simpa using Finset.sum_coe_sort p.parts.toFinset (f := fun a => choose n (a - 1) * Multiset.bell (p.parts.erase a)) - _ = ∑ p : Nat.Partition (n + 1), Multiset.bell p.parts := - Fintype.sum_congr _ _ fun p => bell_eq_sum_erase p + _ = _ := Fintype.sum_congr _ _ fun p => bell_eq_sum_erase p end Nat From 2b6dd5c6cb528bfb32d6ed1866e8d64efd578a36 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 6 Apr 2026 16:41:38 +0800 Subject: [PATCH 14/39] golf a bit --- Mathlib/Combinatorics/Enumerative/Bell.lean | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 2f92edf9224739..cde495913e4e27 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -1,7 +1,8 @@ /- Copyright (c) 2024 Antoine Chambert-Loir & María-Inés de Frutos—Fernández. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Antoine Chambert-Loir, María-Inés de Frutos—Fernández, Yu Shao, Beibei Xiong, Weijie Jiang +Authors: Antoine Chambert-Loir, María-Inés de Frutos—Fernández, Yu Shao, Beibei Xiong, Weijie Jiang, +Yi Yuan -/ module @@ -121,9 +122,8 @@ theorem bell_eq (m : Multiset ℕ) : exact fun _ _ ↦ Nat.factorial_pos _ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase - {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : - ∏ j ∈ m.toFinset.erase 0, (m.count j)! = - (m.count a)! * ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by + {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : ∏ j ∈ m.toFinset.erase 0, (m.count j)! = + (m.count a)! * ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by by_cases hmem : a ∈ m.toFinset.erase 0 · rw [← Finset.mul_prod_erase _ _ hmem] · rw [Finset.erase_eq_of_notMem hmem] @@ -156,12 +156,11 @@ theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : let c := a ! * ((m.map (fun j ↦ j !)).prod * ((m.count a)! * rest)) have hm0 : m.bell * ((m.map (fun j ↦ j !)).prod * ((m.count a)! * rest)) = m.sum ! := by have hm := Multiset.bell_mul_eq m - rw [prod_count_factorial_eq_count_factorial_mul_prod_erase (a := a) ha] at hm + rw [prod_count_factorial_eq_count_factorial_mul_prod_erase ha] at hm simpa [rest, mul_assoc, mul_comm, mul_left_comm] using hm have hm : m.bell * c = m.sum ! * a ! := by simpa [c, mul_assoc, mul_comm, mul_left_comm] using congrArg (fun t => a ! * t) hm0 - have ha_mem : a ∈ (a ::ₘ m).toFinset.erase 0 := by - simp [ha] + have ha_mem : a ∈ (a ::ₘ m).toFinset.erase 0 := by simp [ha] have hc : 0 < c := Nat.mul_pos (Nat.factorial_pos _) <| Nat.mul_pos (map_factorial_prod_pos m) <| by positivity apply Nat.eq_of_mul_eq_mul_right hc @@ -287,8 +286,7 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : calc _ = ((n + 1) * choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring _ = (choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by - have ha1 : 1 ≤ a := Nat.succ_le_of_lt (p.parts_pos ha_mem) - rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel ha1] + rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel (by omega)] _ = _ := by grind _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * Multiset.bell p.parts := by grind [Finset.sum_mul] @@ -314,8 +312,7 @@ private def sigmaPartitionWithPartEquiv (n : ℕ) : (Σ i : Fin n.succ, {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}) ≃ Σ p : Nat.Partition (n + 1), {a : ℕ // a ∈ p.parts.toFinset} where toFun x := ⟨x.2.1, ⟨(x.1 + 1 : ℕ), by simpa using x.2.2⟩⟩ - invFun x := by - refine ⟨⟨x.2.1 - 1, by grind⟩, ⟨x.1, by grind⟩⟩ + invFun x := ⟨⟨x.2.1 - 1, by grind⟩, ⟨x.1, by grind⟩⟩ left_inv x := by simp right_inv x := by grind @@ -332,7 +329,7 @@ theorem bell_eq_sum_partition (n : ℕ) : calc _ = ∑ i : Fin n.succ, ∑ q : Nat.Partition (n - i), choose n i * Multiset.bell q.parts := by refine Fintype.sum_congr _ _ fun i => ?_ - simpa [ih (n - i) (by omega)] using Finset.mul_sum (⊤ : Finset (Nat.Partition (n - i))) + simpa [ih (n - i) _] using Finset.mul_sum (⊤ : Finset (Nat.Partition (n - i))) (fun q => Multiset.bell q.parts) (choose n i) _ = ∑ i : Fin n.succ, ∑ p : {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, choose n i * Multiset.bell (p.1.parts.erase (i + 1)) := by From 7e29fcf630c3603f7297d822fd30500d5f40cfeb Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 6 Apr 2026 16:52:53 +0800 Subject: [PATCH 15/39] golf a bit --- Mathlib/Combinatorics/Enumerative/Bell.lean | 52 +++++++-------------- 1 file changed, 17 insertions(+), 35 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index cde495913e4e27..9d3b9bd72a8fda 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -105,6 +105,10 @@ theorem bell_mul_eq (m : Multiset ℕ) : rw [Finset.sum_multiset_count] simp only [smul_eq_mul, mul_comm] +theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)).prod := by + simpa only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, + forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ + theorem bell_eq (m : Multiset ℕ) : m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)!) := by @@ -114,18 +118,13 @@ theorem bell_eq (m : Multiset ℕ) : · rw [← bell_mul_eq, mul_assoc] apply Nat.dvd_mul_left · rw [← Nat.pos_iff_ne_zero] - apply Nat.mul_pos - · simp only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, - forall_apply_eq_imp_iff₂] - exact fun _ _ ↦ Nat.factorial_pos _ - · apply Finset.prod_pos - exact fun _ _ ↦ Nat.factorial_pos _ + exact Nat.mul_pos (map_factorial_prod_pos m) <| Finset.prod_pos fun _ _ ↦ Nat.factorial_pos _ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : ∏ j ∈ m.toFinset.erase 0, (m.count j)! = (m.count a)! * ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by by_cases hmem : a ∈ m.toFinset.erase 0 - · rw [← Finset.mul_prod_erase _ _ hmem] + · simpa using (Finset.mul_prod_erase (m.toFinset.erase 0) (fun j ↦ (m.count j)!) hmem).symm · rw [Finset.erase_eq_of_notMem hmem] have hcount : m.count a = 0 := by apply Multiset.count_eq_zero_of_notMem @@ -136,19 +135,11 @@ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase theorem prod_count_factorial_cons_erase {m : Multiset ℕ} {a : ℕ} : ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! = ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by - have hset : ((a ::ₘ m).toFinset.erase 0).erase a = (m.toFinset.erase 0).erase a := by - ext x - by_cases hx : x = a - · simp [hx] - · simp [Multiset.toFinset_cons, hx] - rw [hset] - refine Finset.prod_congr rfl ?_ - intro j hj - simp [(Finset.mem_erase.mp hj).1] - -theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)).prod := by - simpa only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, - forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ + refine Finset.prod_congr ?_ ?_ + · ext x + by_cases hx : x = a <;> simp [Multiset.toFinset_cons, hx] + · intro j hj + simp [(Finset.mem_erase.mp hj).1] theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : (a ::ₘ m).bell * (a ::ₘ m).count a = Nat.choose (m.sum + a) a * m.bell := by @@ -198,11 +189,9 @@ theorem uniformBell_eq (m n : ℕ) : m.uniformBell n = · rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]] simp [count_replicate] -theorem uniformBell_zero_left (n : ℕ) : uniformBell 0 n = 1 := by - simp [uniformBell_eq] +theorem uniformBell_zero_left (n : ℕ) : uniformBell 0 n = 1 := by simp [uniformBell_eq] -theorem uniformBell_zero_right (m : ℕ) : uniformBell m 0 = 1 := by - simp [uniformBell_eq] +theorem uniformBell_zero_right (m : ℕ) : uniformBell m 0 = 1 := by simp [uniformBell_eq] theorem uniformBell_succ_left (m n : ℕ) : uniformBell (m + 1) n = choose (m * n + n - 1) (n - 1) * uniformBell m n := by @@ -244,8 +233,7 @@ protected def bell : ℕ → ℕ | n + 1 => ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) theorem bell_succ (n : ℕ) : - Nat.bell (n + 1) = ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) := by - rw [Nat.bell] + Nat.bell (n + 1) = ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) := by rw [Nat.bell] theorem bell_succ' (n : ℕ) : Nat.bell (n + 1) = ∑ ij ∈ Finset.antidiagonal n, choose n ij.1 * Nat.bell ij.2 := by @@ -254,17 +242,11 @@ theorem bell_succ' (n : ℕ) : Finset.sum_range] -@[simp] -theorem bell_zero : Nat.bell 0 = 1 := by - simp [Nat.bell] +@[simp] theorem bell_zero : Nat.bell 0 = 1 := by simp [Nat.bell] -@[simp] -theorem bell_one : Nat.bell 1 = 1 := by - simp [Nat.bell] +@[simp] theorem bell_one : Nat.bell 1 = 1 := by simp [Nat.bell] -@[simp] -theorem bell_two : Nat.bell 2 = 2 := by - simp [Nat.bell] +@[simp] theorem bell_two : Nat.bell 2 = 2 := by simp [Nat.bell] theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : ∑ a ∈ p.parts.toFinset, choose n (a - 1) * Multiset.bell (p.parts.erase a) = From 727d168b7b83cec985f64b443c110ac93c82abaf Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 6 Apr 2026 16:54:49 +0800 Subject: [PATCH 16/39] Revert "golf a bit" This reverts commit 7e29fcf630c3603f7297d822fd30500d5f40cfeb. --- Mathlib/Combinatorics/Enumerative/Bell.lean | 52 ++++++++++++++------- 1 file changed, 35 insertions(+), 17 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 9d3b9bd72a8fda..cde495913e4e27 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -105,10 +105,6 @@ theorem bell_mul_eq (m : Multiset ℕ) : rw [Finset.sum_multiset_count] simp only [smul_eq_mul, mul_comm] -theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)).prod := by - simpa only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, - forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ - theorem bell_eq (m : Multiset ℕ) : m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)!) := by @@ -118,13 +114,18 @@ theorem bell_eq (m : Multiset ℕ) : · rw [← bell_mul_eq, mul_assoc] apply Nat.dvd_mul_left · rw [← Nat.pos_iff_ne_zero] - exact Nat.mul_pos (map_factorial_prod_pos m) <| Finset.prod_pos fun _ _ ↦ Nat.factorial_pos _ + apply Nat.mul_pos + · simp only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, + forall_apply_eq_imp_iff₂] + exact fun _ _ ↦ Nat.factorial_pos _ + · apply Finset.prod_pos + exact fun _ _ ↦ Nat.factorial_pos _ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : ∏ j ∈ m.toFinset.erase 0, (m.count j)! = (m.count a)! * ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by by_cases hmem : a ∈ m.toFinset.erase 0 - · simpa using (Finset.mul_prod_erase (m.toFinset.erase 0) (fun j ↦ (m.count j)!) hmem).symm + · rw [← Finset.mul_prod_erase _ _ hmem] · rw [Finset.erase_eq_of_notMem hmem] have hcount : m.count a = 0 := by apply Multiset.count_eq_zero_of_notMem @@ -135,11 +136,19 @@ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase theorem prod_count_factorial_cons_erase {m : Multiset ℕ} {a : ℕ} : ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! = ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by - refine Finset.prod_congr ?_ ?_ - · ext x - by_cases hx : x = a <;> simp [Multiset.toFinset_cons, hx] - · intro j hj - simp [(Finset.mem_erase.mp hj).1] + have hset : ((a ::ₘ m).toFinset.erase 0).erase a = (m.toFinset.erase 0).erase a := by + ext x + by_cases hx : x = a + · simp [hx] + · simp [Multiset.toFinset_cons, hx] + rw [hset] + refine Finset.prod_congr rfl ?_ + intro j hj + simp [(Finset.mem_erase.mp hj).1] + +theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)).prod := by + simpa only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, + forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : (a ::ₘ m).bell * (a ::ₘ m).count a = Nat.choose (m.sum + a) a * m.bell := by @@ -189,9 +198,11 @@ theorem uniformBell_eq (m n : ℕ) : m.uniformBell n = · rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]] simp [count_replicate] -theorem uniformBell_zero_left (n : ℕ) : uniformBell 0 n = 1 := by simp [uniformBell_eq] +theorem uniformBell_zero_left (n : ℕ) : uniformBell 0 n = 1 := by + simp [uniformBell_eq] -theorem uniformBell_zero_right (m : ℕ) : uniformBell m 0 = 1 := by simp [uniformBell_eq] +theorem uniformBell_zero_right (m : ℕ) : uniformBell m 0 = 1 := by + simp [uniformBell_eq] theorem uniformBell_succ_left (m n : ℕ) : uniformBell (m + 1) n = choose (m * n + n - 1) (n - 1) * uniformBell m n := by @@ -233,7 +244,8 @@ protected def bell : ℕ → ℕ | n + 1 => ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) theorem bell_succ (n : ℕ) : - Nat.bell (n + 1) = ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) := by rw [Nat.bell] + Nat.bell (n + 1) = ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) := by + rw [Nat.bell] theorem bell_succ' (n : ℕ) : Nat.bell (n + 1) = ∑ ij ∈ Finset.antidiagonal n, choose n ij.1 * Nat.bell ij.2 := by @@ -242,11 +254,17 @@ theorem bell_succ' (n : ℕ) : Finset.sum_range] -@[simp] theorem bell_zero : Nat.bell 0 = 1 := by simp [Nat.bell] +@[simp] +theorem bell_zero : Nat.bell 0 = 1 := by + simp [Nat.bell] -@[simp] theorem bell_one : Nat.bell 1 = 1 := by simp [Nat.bell] +@[simp] +theorem bell_one : Nat.bell 1 = 1 := by + simp [Nat.bell] -@[simp] theorem bell_two : Nat.bell 2 = 2 := by simp [Nat.bell] +@[simp] +theorem bell_two : Nat.bell 2 = 2 := by + simp [Nat.bell] theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : ∑ a ∈ p.parts.toFinset, choose n (a - 1) * Multiset.bell (p.parts.erase a) = From e160e265848fae0dfe7d2d0a6987c16b2b6f4196 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 6 Apr 2026 16:58:24 +0800 Subject: [PATCH 17/39] avoid Reinventing the wheel --- Mathlib/Combinatorics/Enumerative/Bell.lean | 29 +++++++-------------- 1 file changed, 10 insertions(+), 19 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index cde495913e4e27..e4a1ce1ed56d5e 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -105,6 +105,10 @@ theorem bell_mul_eq (m : Multiset ℕ) : rw [Finset.sum_multiset_count] simp only [smul_eq_mul, mul_comm] +theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)).prod := by + simpa only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, + forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ + theorem bell_eq (m : Multiset ℕ) : m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)!) := by @@ -114,12 +118,7 @@ theorem bell_eq (m : Multiset ℕ) : · rw [← bell_mul_eq, mul_assoc] apply Nat.dvd_mul_left · rw [← Nat.pos_iff_ne_zero] - apply Nat.mul_pos - · simp only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, - forall_apply_eq_imp_iff₂] - exact fun _ _ ↦ Nat.factorial_pos _ - · apply Finset.prod_pos - exact fun _ _ ↦ Nat.factorial_pos _ + exact Nat.mul_pos (map_factorial_prod_pos m) <| Finset.prod_pos fun _ _ ↦ Nat.factorial_pos _ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : ∏ j ∈ m.toFinset.erase 0, (m.count j)! = @@ -136,19 +135,11 @@ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase theorem prod_count_factorial_cons_erase {m : Multiset ℕ} {a : ℕ} : ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! = ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by - have hset : ((a ::ₘ m).toFinset.erase 0).erase a = (m.toFinset.erase 0).erase a := by - ext x - by_cases hx : x = a - · simp [hx] - · simp [Multiset.toFinset_cons, hx] - rw [hset] - refine Finset.prod_congr rfl ?_ - intro j hj - simp [(Finset.mem_erase.mp hj).1] - -theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)).prod := by - simpa only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, - forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ + refine Finset.prod_congr ?_ ?_ + · ext x + by_cases hx : x = a <;> simp [Multiset.toFinset_cons, hx] + · intro j hj + simp [(Finset.mem_erase.mp hj).1] theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : (a ::ₘ m).bell * (a ::ₘ m).count a = Nat.choose (m.sum + a) a * m.bell := by From 944f743b3bb2b32d00a58c8c460048aeeb67810a Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Tue, 7 Apr 2026 16:07:31 +0800 Subject: [PATCH 18/39] golf --- Mathlib/Combinatorics/Enumerative/Bell.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index e4a1ce1ed56d5e..c68c49e7369c1f 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -331,11 +331,11 @@ theorem bell_eq_sum_partition (n : ℕ) : exact hsub ▸ Eq.symm (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) (fun p => choose n i * Multiset.bell ((partitionWithPartEquiv h1 h2 p).parts)) (fun q => choose n i * Multiset.bell q.parts) (fun _ => rfl)) - _ = ∑ x : Σ i : Fin n.succ, {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, - choose n x.1 * Multiset.bell (x.2.1.parts.erase (x.1 + 1)) := by rw [← Fintype.sum_sigma'] _ = ∑ x : Σ p : Nat.Partition (n + 1), {a : ℕ // a ∈ p.parts.toFinset}, - choose n (x.2.1 - 1) * Multiset.bell (x.1.parts.erase x.2.1) := - Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ (by simp [sigmaPartitionWithPartEquiv]) + choose n (x.2.1 - 1) * Multiset.bell (x.1.parts.erase x.2.1) := by + rw [← Fintype.sum_sigma'] + refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ + simp [sigmaPartitionWithPartEquiv] _ = ∑ p : Nat.Partition (n + 1), ∑ a : {a : ℕ // a ∈ p.parts.toFinset}, choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1) := by simpa using (Fintype.sum_sigma' fun (p : Nat.Partition (n + 1)) From 316c3c263c5989c678ee18046f04f95426cf8726 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 01:17:19 +0800 Subject: [PATCH 19/39] fix --- Mathlib/Combinatorics/Enumerative/Bell.lean | 62 ++++++++++----------- 1 file changed, 29 insertions(+), 33 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index c68c49e7369c1f..699abf7f83a6cb 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -110,8 +110,7 @@ theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)). forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ theorem bell_eq (m : Multiset ℕ) : - m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod * - ∏ j ∈ (m.toFinset.erase 0), (m.count j)!) := by + m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)!) := by rw [← Nat.mul_left_inj, Nat.div_mul_cancel _] · rw [← mul_assoc] exact bell_mul_eq m @@ -127,9 +126,8 @@ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase · rw [← Finset.mul_prod_erase _ _ hmem] · rw [Finset.erase_eq_of_notMem hmem] have hcount : m.count a = 0 := by - apply Multiset.count_eq_zero_of_notMem - intro hm - exact hmem <| by simpa [ha] using hm + refine Multiset.count_eq_zero_of_notMem fun hm ↦ hmem ?_ + simpa [ha] using hm simp [hcount] theorem prod_count_factorial_cons_erase {m : Multiset ℕ} {a : ℕ} : @@ -144,16 +142,16 @@ theorem prod_count_factorial_cons_erase {m : Multiset ℕ} {a : ℕ} : theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : (a ::ₘ m).bell * (a ::ₘ m).count a = Nat.choose (m.sum + a) a * m.bell := by let rest := ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! - let c := a ! * ((m.map (fun j ↦ j !)).prod * ((m.count a)! * rest)) - have hm0 : m.bell * ((m.map (fun j ↦ j !)).prod * ((m.count a)! * rest)) = m.sum ! := by + let c := a ! * ((m.map (· !)).prod * ((m.count a)! * rest)) + have hm0 : m.bell * ((m.map (· !)).prod * ((m.count a)! * rest)) = m.sum ! := by have hm := Multiset.bell_mul_eq m rw [prod_count_factorial_eq_count_factorial_mul_prod_erase ha] at hm simpa [rest, mul_assoc, mul_comm, mul_left_comm] using hm have hm : m.bell * c = m.sum ! * a ! := by - simpa [c, mul_assoc, mul_comm, mul_left_comm] using congrArg (fun t => a ! * t) hm0 + simpa [c, mul_assoc, mul_comm, mul_left_comm] using congrArg (a ! * ·) hm0 have ha_mem : a ∈ (a ::ₘ m).toFinset.erase 0 := by simp [ha] - have hc : 0 < c := Nat.mul_pos (Nat.factorial_pos _) <| - Nat.mul_pos (map_factorial_prod_pos m) <| by positivity + have hc : 0 < c := Nat.mul_pos (by positivity) <| + Nat.mul_pos (map_factorial_prod_pos m) <| by positivity apply Nat.eq_of_mul_eq_mul_right hc calc _ = (a ::ₘ m).bell * ((m.count a + 1) * c) := by @@ -166,9 +164,7 @@ theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : _ = Nat.choose (m.sum + a) a * (m.sum ! * a !) := by rw [← Nat.add_choose_mul_factorial_mul_factorial] ring - _ = Nat.choose (m.sum + a) a * (m.bell * c) := by rw [hm] - _ = (Nat.choose (m.sum + a) a * m.bell) * c := by - simp [mul_assoc, mul_comm, mul_left_comm] + _ = (Nat.choose (m.sum + a) a * m.bell) * c := by simp [← hm, mul_assoc, mul_left_comm] end Multiset @@ -262,11 +258,10 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : Multiset.bell p.parts := by apply Nat.eq_of_mul_eq_mul_left (Nat.succ_pos n) calc - _ = ∑ a ∈ p.parts.toFinset, - (n + 1) * (choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by + _ = ∑ a ∈ p.parts.toFinset, (n + 1) * (choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by rw [Finset.mul_sum] _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * Multiset.bell p.parts) := by - refine Finset.sum_congr rfl fun a ha => ?_ + congr! 1 with a ha have ha_mem : a ∈ p.parts := mem_dedup.mp ha have ha0 : a ≠ 0 := fun h ↦ LT.lt.ne' (p.parts_pos ha_mem) h have hsum : (p.parts.erase a).sum + a = n + 1 := by @@ -275,8 +270,8 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using (bell_cons_mul_count (m := p.parts.erase a) ha0).symm calc - _ = ((n + 1) * choose n (a - 1)) * Multiset.bell (p.parts.erase a) := by ring - _ = (choose (n + 1) a * a) * Multiset.bell (p.parts.erase a) := by + _ = (n + 1) * choose n (a - 1) * Multiset.bell (p.parts.erase a) := by ring + _ = choose (n + 1) a * a * Multiset.bell (p.parts.erase a) := by rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel (by omega)] _ = _ := by grind _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * Multiset.bell p.parts := by @@ -319,33 +314,34 @@ theorem bell_eq_sum_partition (n : ℕ) : rw [Nat.bell_succ] calc _ = ∑ i : Fin n.succ, ∑ q : Nat.Partition (n - i), choose n i * Multiset.bell q.parts := by - refine Fintype.sum_congr _ _ fun i => ?_ + congr! with i simpa [ih (n - i) _] using Finset.mul_sum (⊤ : Finset (Nat.Partition (n - i))) - (fun q => Multiset.bell q.parts) (choose n i) + (fun q ↦ Multiset.bell q.parts) (choose n i) _ = ∑ i : Fin n.succ, ∑ p : {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, choose n i * Multiset.bell (p.1.parts.erase (i + 1)) := by - refine Fintype.sum_congr _ _ fun i => ?_ + congr! with i have h1 : 1 ≤ (i + 1 : ℕ) := by omega have h2 : (i + 1 : ℕ) ≤ n + 1 := by omega have hsub : n + 1 - (i + 1 : ℕ) = n - i := by omega exact hsub ▸ Eq.symm (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) - (fun p => choose n i * Multiset.bell ((partitionWithPartEquiv h1 h2 p).parts)) - (fun q => choose n i * Multiset.bell q.parts) (fun _ => rfl)) - _ = ∑ x : Σ p : Nat.Partition (n + 1), {a : ℕ // a ∈ p.parts.toFinset}, + (fun p ↦ choose n i * Multiset.bell ((partitionWithPartEquiv h1 h2 p).parts)) + (fun q ↦ choose n i * Multiset.bell q.parts) (fun _ => rfl)) + _ = ∑ x : Σ p : Nat.Partition (n + 1), p.parts.toFinset, choose n (x.2.1 - 1) * Multiset.bell (x.1.parts.erase x.2.1) := by rw [← Fintype.sum_sigma'] refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ simp [sigmaPartitionWithPartEquiv] - _ = ∑ p : Nat.Partition (n + 1), ∑ a : {a : ℕ // a ∈ p.parts.toFinset}, - choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1) := by - simpa using (Fintype.sum_sigma' fun (p : Nat.Partition (n + 1)) - (a : {a : ℕ // a ∈ p.parts.toFinset}) => - choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1)) + _ = ∑ p : Nat.Partition (n + 1), ∑ a : p.parts.toFinset, + choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1) := + Fintype.sum_sigma' fun (p : Nat.Partition (n + 1)) (a : p.parts.toFinset) ↦ + choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1) _ = ∑ p : Nat.Partition (n + 1), ∑ a ∈ p.parts.toFinset, choose n (a - 1) * Multiset.bell (p.parts.erase a) := by - refine Fintype.sum_congr _ _ fun p => ?_ - simpa using Finset.sum_coe_sort p.parts.toFinset - (f := fun a => choose n (a - 1) * Multiset.bell (p.parts.erase a)) - _ = _ := Fintype.sum_congr _ _ fun p => bell_eq_sum_erase p + congr! with p + exact p.parts.toFinset.sum_coe_sort + (fun a ↦ choose n (a - 1) * Multiset.bell (p.parts.erase a)) + _ = _ := by + congr! with p + exact bell_eq_sum_erase p end Nat From 186806dbb481fdddaade3606c40898dccdb1f6bf Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 01:42:19 +0800 Subject: [PATCH 20/39] fix --- Mathlib/Combinatorics/Enumerative/Bell.lean | 42 ++++++++++----------- 1 file changed, 19 insertions(+), 23 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 699abf7f83a6cb..6413fbd5dbcae5 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -254,13 +254,12 @@ theorem bell_two : Nat.bell 2 = 2 := by simp [Nat.bell] theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : - ∑ a ∈ p.parts.toFinset, choose n (a - 1) * Multiset.bell (p.parts.erase a) = - Multiset.bell p.parts := by + ∑ a ∈ p.parts.toFinset, choose n (a - 1) * (p.parts.erase a).bell = p.parts.bell := by apply Nat.eq_of_mul_eq_mul_left (Nat.succ_pos n) calc - _ = ∑ a ∈ p.parts.toFinset, (n + 1) * (choose n (a - 1) * Multiset.bell (p.parts.erase a)) := by + _ = ∑ a ∈ p.parts.toFinset, (n + 1) * (choose n (a - 1) * (p.parts.erase a).bell) := by rw [Finset.mul_sum] - _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * Multiset.bell p.parts) := by + _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * p.parts.bell) := by congr! 1 with a ha have ha_mem : a ∈ p.parts := mem_dedup.mp ha have ha0 : a ≠ 0 := fun h ↦ LT.lt.ne' (p.parts_pos ha_mem) h @@ -270,12 +269,11 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using (bell_cons_mul_count (m := p.parts.erase a) ha0).symm calc - _ = (n + 1) * choose n (a - 1) * Multiset.bell (p.parts.erase a) := by ring - _ = choose (n + 1) a * a * Multiset.bell (p.parts.erase a) := by + _ = (n + 1) * choose n (a - 1) * (p.parts.erase a).bell := by ring + _ = choose (n + 1) a * a * (p.parts.erase a).bell := by rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel (by omega)] _ = _ := by grind - _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * Multiset.bell p.parts := by - grind [Finset.sum_mul] + _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * p.parts.bell := by grind [Finset.sum_mul] _ = _ := by have hsum : ∑ a ∈ p.parts.toFinset, p.parts.count a * a = n + 1 := by simpa [smul_eq_mul, p.parts_sum, mul_comm] using (Finset.sum_multiset_count p.parts).symm @@ -286,7 +284,7 @@ private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1 toFun p := by refine ⟨p.1.parts.erase a, ?_, ?_⟩ · intro _ hi - exact p.1.parts_pos (Multiset.erase_subset a p.1.parts hi) + exact p.1.parts_pos (p.1.parts.erase_subset a hi) · have hs : a + (p.1.parts.erase a).sum = n + 1 := by simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) omega @@ -304,8 +302,7 @@ private def sigmaPartitionWithPartEquiv (n : ℕ) : /-- `Nat.bell n` is equal to the sum of `Multiset.bell m` over all multisets `m : Multiset ℕ` such that `m.sum = n`. -/ -theorem bell_eq_sum_partition (n : ℕ) : - Nat.bell n = ∑ p : Nat.Partition n, Multiset.bell p.parts := by +theorem bell_eq_sum_partition (n : ℕ) : Nat.bell n = ∑ p : Nat.Partition n, p.parts.bell := by refine Nat.strong_induction_on n ?_ intro n ih cases n with @@ -313,33 +310,32 @@ theorem bell_eq_sum_partition (n : ℕ) : | succ n => rw [Nat.bell_succ] calc - _ = ∑ i : Fin n.succ, ∑ q : Nat.Partition (n - i), choose n i * Multiset.bell q.parts := by + _ = ∑ i : Fin n.succ, ∑ q : Nat.Partition (n - i), choose n i * q.parts.bell := by congr! with i simpa [ih (n - i) _] using Finset.mul_sum (⊤ : Finset (Nat.Partition (n - i))) - (fun q ↦ Multiset.bell q.parts) (choose n i) + (fun q ↦ q.parts.bell) (choose n i) _ = ∑ i : Fin n.succ, ∑ p : {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, - choose n i * Multiset.bell (p.1.parts.erase (i + 1)) := by + choose n i * (p.1.parts.erase (i + 1)).bell := by congr! with i have h1 : 1 ≤ (i + 1 : ℕ) := by omega have h2 : (i + 1 : ℕ) ≤ n + 1 := by omega have hsub : n + 1 - (i + 1 : ℕ) = n - i := by omega exact hsub ▸ Eq.symm (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) - (fun p ↦ choose n i * Multiset.bell ((partitionWithPartEquiv h1 h2 p).parts)) - (fun q ↦ choose n i * Multiset.bell q.parts) (fun _ => rfl)) + (fun p ↦ choose n i * (partitionWithPartEquiv h1 h2 p).parts.bell) + (fun q ↦ choose n i * q.parts.bell) (fun _ => rfl)) _ = ∑ x : Σ p : Nat.Partition (n + 1), p.parts.toFinset, - choose n (x.2.1 - 1) * Multiset.bell (x.1.parts.erase x.2.1) := by + choose n (x.2.1 - 1) * (x.1.parts.erase x.2.1).bell := by rw [← Fintype.sum_sigma'] refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ simp [sigmaPartitionWithPartEquiv] _ = ∑ p : Nat.Partition (n + 1), ∑ a : p.parts.toFinset, - choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1) := + choose n (a - 1) * (p.parts.erase a).bell := Fintype.sum_sigma' fun (p : Nat.Partition (n + 1)) (a : p.parts.toFinset) ↦ - choose n (a.1 - 1) * Multiset.bell (p.parts.erase a.1) - _ = ∑ p : Nat.Partition (n + 1), - ∑ a ∈ p.parts.toFinset, choose n (a - 1) * Multiset.bell (p.parts.erase a) := by + choose n (a - 1) * (p.parts.erase a.1).bell + _ = ∑ p : Nat.Partition (n + 1), ∑ a ∈ p.parts.toFinset, + choose n (a - 1) * (p.parts.erase a).bell := by congr! with p - exact p.parts.toFinset.sum_coe_sort - (fun a ↦ choose n (a - 1) * Multiset.bell (p.parts.erase a)) + exact p.parts.toFinset.sum_coe_sort (fun a ↦ choose n (a - 1) * (p.parts.erase a).bell) _ = _ := by congr! with p exact bell_eq_sum_erase p From 918f29b1cf3a06602be9f6591eb926c50e93d7a3 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 08:47:04 +0800 Subject: [PATCH 21/39] fix --- Mathlib/Combinatorics/Enumerative/Bell.lean | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 6413fbd5dbcae5..5ad172fb94a559 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -110,7 +110,7 @@ theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)). forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ theorem bell_eq (m : Multiset ℕ) : - m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)!) := by + m.bell = m.sum ! / ((m.map fun j ↦ j !).prod * ∏ j ∈ m.toFinset.erase 0, (m.count j)!) := by rw [← Nat.mul_left_inj, Nat.div_mul_cancel _] · rw [← mul_assoc] exact bell_mul_eq m @@ -240,7 +240,6 @@ theorem bell_succ' (n : ℕ) : Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => choose n x * Nat.bell y) n, Finset.sum_range] - @[simp] theorem bell_zero : Nat.bell 0 = 1 := by simp [Nat.bell] @@ -266,8 +265,8 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : have hsum : (p.parts.erase a).sum + a = n + 1 := by simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) have hbell : choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by - simpa [hsum, Multiset.cons_erase ha_mem, mul_comm, mul_left_comm, mul_assoc] using - (bell_cons_mul_count (m := p.parts.erase a) ha0).symm + simpa [hsum, cons_erase ha_mem, mul_comm] using + ((p.parts.erase a).bell_cons_mul_count ha0).symm calc _ = (n + 1) * choose n (a - 1) * (p.parts.erase a).bell := by ring _ = choose (n + 1) a * a * (p.parts.erase a).bell := by @@ -275,9 +274,9 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : _ = _ := by grind _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * p.parts.bell := by grind [Finset.sum_mul] _ = _ := by - have hsum : ∑ a ∈ p.parts.toFinset, p.parts.count a * a = n + 1 := by - simpa [smul_eq_mul, p.parts_sum, mul_comm] using (Finset.sum_multiset_count p.parts).symm - rw [hsum] + rw [succ_eq_add_one, mul_eq_mul_right_iff] + left + simpa [smul_eq_mul, p.parts_sum, mul_comm] using (Finset.sum_multiset_count p.parts).symm private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1) : {p : Nat.Partition (n + 1) // a ∈ p.parts} ≃ Nat.Partition (n + 1 - a) where From 468a6301f438bf43489e6861359664d7b3b3415a Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 08:56:32 +0800 Subject: [PATCH 22/39] fix --- Mathlib/Combinatorics/Enumerative/Bell.lean | 24 +++++++-------------- 1 file changed, 8 insertions(+), 16 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 5ad172fb94a559..eb3c8ab230f2d4 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -105,10 +105,6 @@ theorem bell_mul_eq (m : Multiset ℕ) : rw [Finset.sum_multiset_count] simp only [smul_eq_mul, mul_comm] -theorem map_factorial_prod_pos (m : Multiset ℕ) : 0 < (m.map (fun j ↦ j !)).prod := by - simpa only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp, - forall_apply_eq_imp_iff₂] using fun _ _ ↦ Nat.factorial_pos _ - theorem bell_eq (m : Multiset ℕ) : m.bell = m.sum ! / ((m.map fun j ↦ j !).prod * ∏ j ∈ m.toFinset.erase 0, (m.count j)!) := by rw [← Nat.mul_left_inj, Nat.div_mul_cancel _] @@ -117,7 +113,7 @@ theorem bell_eq (m : Multiset ℕ) : · rw [← bell_mul_eq, mul_assoc] apply Nat.dvd_mul_left · rw [← Nat.pos_iff_ne_zero] - exact Nat.mul_pos (map_factorial_prod_pos m) <| Finset.prod_pos fun _ _ ↦ Nat.factorial_pos _ + exact Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity) theorem prod_count_factorial_eq_count_factorial_mul_prod_erase {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : ∏ j ∈ m.toFinset.erase 0, (m.count j)! = @@ -142,8 +138,8 @@ theorem prod_count_factorial_cons_erase {m : Multiset ℕ} {a : ℕ} : theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : (a ::ₘ m).bell * (a ::ₘ m).count a = Nat.choose (m.sum + a) a * m.bell := by let rest := ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! - let c := a ! * ((m.map (· !)).prod * ((m.count a)! * rest)) - have hm0 : m.bell * ((m.map (· !)).prod * ((m.count a)! * rest)) = m.sum ! := by + let c := a ! * ((m.map (· !)).prod * (m.count a)! * rest) + have hm0 : m.bell * ((m.map (· !)).prod * (m.count a)! * rest) = m.sum ! := by have hm := Multiset.bell_mul_eq m rw [prod_count_factorial_eq_count_factorial_mul_prod_erase ha] at hm simpa [rest, mul_assoc, mul_comm, mul_left_comm] using hm @@ -151,20 +147,16 @@ theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : simpa [c, mul_assoc, mul_comm, mul_left_comm] using congrArg (a ! * ·) hm0 have ha_mem : a ∈ (a ::ₘ m).toFinset.erase 0 := by simp [ha] have hc : 0 < c := Nat.mul_pos (by positivity) <| - Nat.mul_pos (map_factorial_prod_pos m) <| by positivity + Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity) apply Nat.eq_of_mul_eq_mul_right hc calc - _ = (a ::ₘ m).bell * ((m.count a + 1) * c) := by - simp [mul_assoc] + _ = (a ::ₘ m).bell * (m.count a + 1) * c := by simp [mul_assoc] _ = (m.sum + a)! := by have hq := Multiset.bell_mul_eq (a ::ₘ m) rw [← Finset.mul_prod_erase _ _ ha_mem, prod_count_factorial_cons_erase] at hq - simpa [c, rest, Nat.factorial_succ, Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, - add_comm, mul_assoc, mul_comm, mul_left_comm] using hq - _ = Nat.choose (m.sum + a) a * (m.sum ! * a !) := by - rw [← Nat.add_choose_mul_factorial_mul_factorial] - ring - _ = (Nat.choose (m.sum + a) a * m.bell) * c := by simp [← hm, mul_assoc, mul_left_comm] + simpa [c, Nat.factorial_succ, add_comm, mul_assoc, mul_left_comm] using hq + _ = (Nat.choose (m.sum + a) a * m.bell) * c := by + simp [← Nat.add_choose_mul_factorial_mul_factorial, mul_assoc, ← hm] end Multiset From d0b91ce179baaee6e727b56bb5c22eec0e7aa407 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 09:03:29 +0800 Subject: [PATCH 23/39] fix --- Mathlib/Combinatorics/Enumerative/Bell.lean | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index eb3c8ab230f2d4..dd382f0f68fcf9 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -76,12 +76,10 @@ private theorem bell_mul_eq_lemma {x : ℕ} (hx : x ≠ 0) : ring_nf theorem bell_mul_eq (m : Multiset ℕ) : - m.bell * (m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)! - = m.sum ! := by + m.bell * (m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)! = m.sum ! := by unfold bell rw [← Nat.mul_right_inj (a := ∏ i ∈ m.toFinset, (i * count i m)!) (by positivity)] - simp only [← mul_assoc] - rw [Nat.multinomial_spec] + simp only [← mul_assoc, Nat.multinomial_spec] simp only [mul_assoc] rw [mul_comm] apply congr_arg₂ @@ -253,7 +251,7 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * p.parts.bell) := by congr! 1 with a ha have ha_mem : a ∈ p.parts := mem_dedup.mp ha - have ha0 : a ≠ 0 := fun h ↦ LT.lt.ne' (p.parts_pos ha_mem) h + have ha0 : a ≠ 0 := by grind have hsum : (p.parts.erase a).sum + a = n + 1 := by simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) have hbell : choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by @@ -323,12 +321,9 @@ theorem bell_eq_sum_partition (n : ℕ) : Nat.bell n = ∑ p : Nat.Partition n, choose n (a - 1) * (p.parts.erase a).bell := Fintype.sum_sigma' fun (p : Nat.Partition (n + 1)) (a : p.parts.toFinset) ↦ choose n (a - 1) * (p.parts.erase a.1).bell - _ = ∑ p : Nat.Partition (n + 1), ∑ a ∈ p.parts.toFinset, - choose n (a - 1) * (p.parts.erase a).bell := by - congr! with p - exact p.parts.toFinset.sum_coe_sort (fun a ↦ choose n (a - 1) * (p.parts.erase a).bell) _ = _ := by congr! with p - exact bell_eq_sum_erase p + rw [← bell_eq_sum_erase p] + exact p.parts.toFinset.sum_coe_sort (fun a ↦ choose n (a - 1) * (p.parts.erase a).bell) end Nat From 4de519a088cf7d64a6435dc43b0c3f0acef82e66 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 09:12:39 +0800 Subject: [PATCH 24/39] fix --- Mathlib/Combinatorics/Enumerative/Bell.lean | 36 ++++++++++----------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index dd382f0f68fcf9..4f206a06cc790b 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -153,7 +153,7 @@ theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : have hq := Multiset.bell_mul_eq (a ::ₘ m) rw [← Finset.mul_prod_erase _ _ ha_mem, prod_count_factorial_cons_erase] at hq simpa [c, Nat.factorial_succ, add_comm, mul_assoc, mul_left_comm] using hq - _ = (Nat.choose (m.sum + a) a * m.bell) * c := by + _ = ((m.sum + a).choose a * m.bell) * c := by simp [← Nat.add_choose_mul_factorial_mul_factorial, mul_assoc, ← hm] end Multiset @@ -209,7 +209,7 @@ theorem uniformBell_eq_div (m : ℕ) {n : ℕ} (hn : n ≠ 0) : uniformBell m n = (m * n)! / (n ! ^ m * m !) := by rw [eq_comm] apply Nat.div_eq_of_eq_mul_left - · exact Nat.mul_pos (Nat.pow_pos (Nat.factorial_pos n)) m.factorial_pos + · exact Nat.mul_pos (Nat.pow_pos n.factorial_pos) m.factorial_pos · rw [← mul_assoc, ← uniformBell_mul_eq _ hn] /-- @@ -218,16 +218,16 @@ which counts the number of partitions of a set of cardinality `n`. -/ protected def bell : ℕ → ℕ | 0 => 1 - | n + 1 => ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) + | n + 1 => ∑ i : Fin n.succ, choose n i * (n - i).bell theorem bell_succ (n : ℕ) : - Nat.bell (n + 1) = ∑ i : Fin n.succ, choose n i * Nat.bell (n - i) := by + (n + 1).bell = ∑ i : Fin n.succ, choose n i * (n - i).bell := by rw [Nat.bell] theorem bell_succ' (n : ℕ) : - Nat.bell (n + 1) = ∑ ij ∈ Finset.antidiagonal n, choose n ij.1 * Nat.bell ij.2 := by + (n + 1).bell = ∑ ij ∈ Finset.antidiagonal n, choose n ij.1 * ij.2.bell := by rw [Nat.bell_succ, - Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => choose n x * Nat.bell y) n, + Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y ↦ choose n x * y.bell) n, Finset.sum_range] @[simp] @@ -242,9 +242,9 @@ theorem bell_one : Nat.bell 1 = 1 := by theorem bell_two : Nat.bell 2 = 2 := by simp [Nat.bell] -theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : +theorem bell_eq_sum_erase {n : ℕ} (p : (n + 1).Partition) : ∑ a ∈ p.parts.toFinset, choose n (a - 1) * (p.parts.erase a).bell = p.parts.bell := by - apply Nat.eq_of_mul_eq_mul_left (Nat.succ_pos n) + apply Nat.eq_of_mul_eq_mul_left n.succ_pos calc _ = ∑ a ∈ p.parts.toFinset, (n + 1) * (choose n (a - 1) * (p.parts.erase a).bell) := by rw [Finset.mul_sum] @@ -269,7 +269,7 @@ theorem bell_eq_sum_erase {n : ℕ} (p : Nat.Partition (n + 1)) : simpa [smul_eq_mul, p.parts_sum, mul_comm] using (Finset.sum_multiset_count p.parts).symm private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1) : - {p : Nat.Partition (n + 1) // a ∈ p.parts} ≃ Nat.Partition (n + 1 - a) where + {p : (n + 1).Partition // a ∈ p.parts} ≃ (n + 1 - a).Partition where toFun p := by refine ⟨p.1.parts.erase a, ?_, ?_⟩ · intro _ hi @@ -282,8 +282,8 @@ private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1 right_inv q := Partition.ext <| erase_cons_head a q.parts private def sigmaPartitionWithPartEquiv (n : ℕ) : - (Σ i : Fin n.succ, {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}) ≃ - Σ p : Nat.Partition (n + 1), {a : ℕ // a ∈ p.parts.toFinset} where + (Σ i : Fin n.succ, {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}) ≃ + Σ p : (n + 1).Partition, {a : ℕ // a ∈ p.parts.toFinset} where toFun x := ⟨x.2.1, ⟨(x.1 + 1 : ℕ), by simpa using x.2.2⟩⟩ invFun x := ⟨⟨x.2.1 - 1, by grind⟩, ⟨x.1, by grind⟩⟩ left_inv x := by simp @@ -291,7 +291,7 @@ private def sigmaPartitionWithPartEquiv (n : ℕ) : /-- `Nat.bell n` is equal to the sum of `Multiset.bell m` over all multisets `m : Multiset ℕ` such that `m.sum = n`. -/ -theorem bell_eq_sum_partition (n : ℕ) : Nat.bell n = ∑ p : Nat.Partition n, p.parts.bell := by +theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts.bell := by refine Nat.strong_induction_on n ?_ intro n ih cases n with @@ -299,11 +299,11 @@ theorem bell_eq_sum_partition (n : ℕ) : Nat.bell n = ∑ p : Nat.Partition n, | succ n => rw [Nat.bell_succ] calc - _ = ∑ i : Fin n.succ, ∑ q : Nat.Partition (n - i), choose n i * q.parts.bell := by + _ = ∑ i : Fin n.succ, ∑ q : (n - i).Partition, choose n i * q.parts.bell := by congr! with i - simpa [ih (n - i) _] using Finset.mul_sum (⊤ : Finset (Nat.Partition (n - i))) + simpa [ih (n - i) _] using Finset.mul_sum (⊤ : Finset (n - i).Partition) (fun q ↦ q.parts.bell) (choose n i) - _ = ∑ i : Fin n.succ, ∑ p : {p : Nat.Partition (n + 1) // (i + 1 : ℕ) ∈ p.parts}, + _ = ∑ i : Fin n.succ, ∑ p : {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}, choose n i * (p.1.parts.erase (i + 1)).bell := by congr! with i have h1 : 1 ≤ (i + 1 : ℕ) := by omega @@ -312,14 +312,14 @@ theorem bell_eq_sum_partition (n : ℕ) : Nat.bell n = ∑ p : Nat.Partition n, exact hsub ▸ Eq.symm (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) (fun p ↦ choose n i * (partitionWithPartEquiv h1 h2 p).parts.bell) (fun q ↦ choose n i * q.parts.bell) (fun _ => rfl)) - _ = ∑ x : Σ p : Nat.Partition (n + 1), p.parts.toFinset, + _ = ∑ x : Σ p : (n + 1).Partition, p.parts.toFinset, choose n (x.2.1 - 1) * (x.1.parts.erase x.2.1).bell := by rw [← Fintype.sum_sigma'] refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ simp [sigmaPartitionWithPartEquiv] - _ = ∑ p : Nat.Partition (n + 1), ∑ a : p.parts.toFinset, + _ = ∑ p : (n + 1).Partition, ∑ a : p.parts.toFinset, choose n (a - 1) * (p.parts.erase a).bell := - Fintype.sum_sigma' fun (p : Nat.Partition (n + 1)) (a : p.parts.toFinset) ↦ + Fintype.sum_sigma' fun (p : (n + 1).Partition) (a : p.parts.toFinset) ↦ choose n (a - 1) * (p.parts.erase a.1).bell _ = _ := by congr! with p From f8cc2aaedb14d0622c7fcbf777897bbaa180fdd1 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 09:16:29 +0800 Subject: [PATCH 25/39] fix --- Mathlib/Combinatorics/Enumerative/Bell.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 4f206a06cc790b..1c9b4a900449f6 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -266,7 +266,7 @@ theorem bell_eq_sum_erase {n : ℕ} (p : (n + 1).Partition) : _ = _ := by rw [succ_eq_add_one, mul_eq_mul_right_iff] left - simpa [smul_eq_mul, p.parts_sum, mul_comm] using (Finset.sum_multiset_count p.parts).symm + simpa [smul_eq_mul, p.parts_sum] using (Finset.sum_multiset_count p.parts).symm private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1) : {p : (n + 1).Partition // a ∈ p.parts} ≃ (n + 1 - a).Partition where @@ -301,17 +301,14 @@ theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts. calc _ = ∑ i : Fin n.succ, ∑ q : (n - i).Partition, choose n i * q.parts.bell := by congr! with i - simpa [ih (n - i) _] using Finset.mul_sum (⊤ : Finset (n - i).Partition) - (fun q ↦ q.parts.bell) (choose n i) + simp [ih (n - i) _, Finset.mul_sum] _ = ∑ i : Fin n.succ, ∑ p : {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}, choose n i * (p.1.parts.erase (i + 1)).bell := by congr! with i have h1 : 1 ≤ (i + 1 : ℕ) := by omega have h2 : (i + 1 : ℕ) ≤ n + 1 := by omega have hsub : n + 1 - (i + 1 : ℕ) = n - i := by omega - exact hsub ▸ Eq.symm (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) - (fun p ↦ choose n i * (partitionWithPartEquiv h1 h2 p).parts.bell) - (fun q ↦ choose n i * q.parts.bell) (fun _ => rfl)) + exact hsub ▸ (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) _ _ (fun _ ↦ rfl)).symm _ = ∑ x : Σ p : (n + 1).Partition, p.parts.toFinset, choose n (x.2.1 - 1) * (x.1.parts.erase x.2.1).bell := by rw [← Fintype.sum_sigma'] From 15ab8a8ea65ae043ea68192e9e6894291aa165a2 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 16:45:50 +0800 Subject: [PATCH 26/39] Update Mathlib/Combinatorics/Enumerative/Bell.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/Combinatorics/Enumerative/Bell.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 1c9b4a900449f6..af42b642506c20 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -221,7 +221,7 @@ protected def bell : ℕ → ℕ | n + 1 => ∑ i : Fin n.succ, choose n i * (n - i).bell theorem bell_succ (n : ℕ) : - (n + 1).bell = ∑ i : Fin n.succ, choose n i * (n - i).bell := by + (n + 1).bell = ∑ i : Fin n.succ, choose n i * (n - i).bell := by rw [Nat.bell] theorem bell_succ' (n : ℕ) : From 778380bf62b3c33b904fdad747fd44a47dde964f Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 18:02:23 +0800 Subject: [PATCH 27/39] reduce worthless lemmas --- Mathlib/Combinatorics/Enumerative/Bell.lean | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 1c9b4a900449f6..a8de96a146a6da 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -124,18 +124,14 @@ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase simpa [ha] using hm simp [hcount] -theorem prod_count_factorial_cons_erase {m : Multiset ℕ} {a : ℕ} : - ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! = - ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by - refine Finset.prod_congr ?_ ?_ - · ext x - by_cases hx : x = a <;> simp [Multiset.toFinset_cons, hx] - · intro j hj - simp [(Finset.mem_erase.mp hj).1] - theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : (a ::ₘ m).bell * (a ::ₘ m).count a = Nat.choose (m.sum + a) a * m.bell := by let rest := ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! + have hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! := by + refine Finset.prod_congr ?_ ?_ + · grind [Multiset.toFinset_cons] + · intro _ hj + simp [Finset.mem_erase.mp hj] let c := a ! * ((m.map (· !)).prod * (m.count a)! * rest) have hm0 : m.bell * ((m.map (· !)).prod * (m.count a)! * rest) = m.sum ! := by have hm := Multiset.bell_mul_eq m @@ -151,7 +147,7 @@ theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : _ = (a ::ₘ m).bell * (m.count a + 1) * c := by simp [mul_assoc] _ = (m.sum + a)! := by have hq := Multiset.bell_mul_eq (a ::ₘ m) - rw [← Finset.mul_prod_erase _ _ ha_mem, prod_count_factorial_cons_erase] at hq + rw [← Finset.mul_prod_erase _ _ ha_mem, ← hrest] at hq simpa [c, Nat.factorial_succ, add_comm, mul_assoc, mul_left_comm] using hq _ = ((m.sum + a).choose a * m.bell) * c := by simp [← Nat.add_choose_mul_factorial_mul_factorial, mul_assoc, ← hm] From 6b3c657a1af8106ebb4d96328ec8c46278db516c Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 21 May 2026 18:49:29 +0800 Subject: [PATCH 28/39] reduce worthless lemmas --- Mathlib/Combinatorics/Enumerative/Bell.lean | 31 ++++++++++----------- 1 file changed, 15 insertions(+), 16 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 47c982c6789117..a7a8834ffe4777 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -113,8 +113,8 @@ theorem bell_eq (m : Multiset ℕ) : · rw [← Nat.pos_iff_ne_zero] exact Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity) -theorem prod_count_factorial_eq_count_factorial_mul_prod_erase - {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : ∏ j ∈ m.toFinset.erase 0, (m.count j)! = +private theorem prod_count_factorial_eq_count_factorial_mul_prod_erase + (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) : ∏ j ∈ m.toFinset.erase 0, (m.count j)! = (m.count a)! * ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by by_cases hmem : a ∈ m.toFinset.erase 0 · rw [← Finset.mul_prod_erase _ _ hmem] @@ -124,32 +124,31 @@ theorem prod_count_factorial_eq_count_factorial_mul_prod_erase simpa [ha] using hm simp [hcount] -theorem bell_cons_mul_count {m : Multiset ℕ} {a : ℕ} (ha : a ≠ 0) : - (a ::ₘ m).bell * (a ::ₘ m).count a = Nat.choose (m.sum + a) a * m.bell := by +private theorem bell_cons_mul_count (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) : + (a ::ₘ m).bell * (a ::ₘ m).count a = (m.sum + a).choose a * m.bell := by let rest := ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! have hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! := by refine Finset.prod_congr ?_ ?_ · grind [Multiset.toFinset_cons] · intro _ hj simp [Finset.mem_erase.mp hj] - let c := a ! * ((m.map (· !)).prod * (m.count a)! * rest) + let c := (m.map (· !)).prod * (m.count a)! * rest have hm0 : m.bell * ((m.map (· !)).prod * (m.count a)! * rest) = m.sum ! := by have hm := Multiset.bell_mul_eq m - rw [prod_count_factorial_eq_count_factorial_mul_prod_erase ha] at hm + rw [prod_count_factorial_eq_count_factorial_mul_prod_erase m ha] at hm simpa [rest, mul_assoc, mul_comm, mul_left_comm] using hm - have hm : m.bell * c = m.sum ! * a ! := by + have hm : m.bell * a ! * c = m.sum ! * a ! := by simpa [c, mul_assoc, mul_comm, mul_left_comm] using congrArg (a ! * ·) hm0 have ha_mem : a ∈ (a ::ₘ m).toFinset.erase 0 := by simp [ha] - have hc : 0 < c := Nat.mul_pos (by positivity) <| + have hc : 0 < a ! * c := Nat.mul_pos (by positivity) <| Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity) apply Nat.eq_of_mul_eq_mul_right hc calc - _ = (a ::ₘ m).bell * (m.count a + 1) * c := by simp [mul_assoc] _ = (m.sum + a)! := by have hq := Multiset.bell_mul_eq (a ::ₘ m) rw [← Finset.mul_prod_erase _ _ ha_mem, ← hrest] at hq simpa [c, Nat.factorial_succ, add_comm, mul_assoc, mul_left_comm] using hq - _ = ((m.sum + a).choose a * m.bell) * c := by + _ = ((m.sum + a).choose a * m.bell) * (a ! * c) := by simp [← Nat.add_choose_mul_factorial_mul_factorial, mul_assoc, ← hm] end Multiset @@ -239,10 +238,10 @@ theorem bell_two : Nat.bell 2 = 2 := by simp [Nat.bell] theorem bell_eq_sum_erase {n : ℕ} (p : (n + 1).Partition) : - ∑ a ∈ p.parts.toFinset, choose n (a - 1) * (p.parts.erase a).bell = p.parts.bell := by + ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell = p.parts.bell := by apply Nat.eq_of_mul_eq_mul_left n.succ_pos calc - _ = ∑ a ∈ p.parts.toFinset, (n + 1) * (choose n (a - 1) * (p.parts.erase a).bell) := by + _ = ∑ a ∈ p.parts.toFinset, (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell) := by rw [Finset.mul_sum] _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * p.parts.bell) := by congr! 1 with a ha @@ -250,12 +249,12 @@ theorem bell_eq_sum_erase {n : ℕ} (p : (n + 1).Partition) : have ha0 : a ≠ 0 := by grind have hsum : (p.parts.erase a).sum + a = n + 1 := by simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) - have hbell : choose (n + 1) a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by + have hbell : (n + 1).choose a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by simpa [hsum, cons_erase ha_mem, mul_comm] using ((p.parts.erase a).bell_cons_mul_count ha0).symm calc - _ = (n + 1) * choose n (a - 1) * (p.parts.erase a).bell := by ring - _ = choose (n + 1) a * a * (p.parts.erase a).bell := by + _ = (n + 1) * n.choose (a - 1) * (p.parts.erase a).bell := by ring + _ = (n + 1).choose a * a * (p.parts.erase a).bell := by rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel (by omega)] _ = _ := by grind _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * p.parts.bell := by grind [Finset.sum_mul] @@ -295,7 +294,7 @@ theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts. | succ n => rw [Nat.bell_succ] calc - _ = ∑ i : Fin n.succ, ∑ q : (n - i).Partition, choose n i * q.parts.bell := by + _ = ∑ i : Fin n.succ, ∑ q : (n - i).Partition, n.choose i * q.parts.bell := by congr! with i simp [ih (n - i) _, Finset.mul_sum] _ = ∑ i : Fin n.succ, ∑ p : {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}, From e279236d54adbdda9370e9e108f2d6071f8aff5f Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 22 May 2026 17:00:16 +0800 Subject: [PATCH 29/39] golf --- Mathlib/Combinatorics/Enumerative/Bell.lean | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index a7a8834ffe4777..7fe2f30abcfdc5 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -119,9 +119,7 @@ private theorem prod_count_factorial_eq_count_factorial_mul_prod_erase by_cases hmem : a ∈ m.toFinset.erase 0 · rw [← Finset.mul_prod_erase _ _ hmem] · rw [Finset.erase_eq_of_notMem hmem] - have hcount : m.count a = 0 := by - refine Multiset.count_eq_zero_of_notMem fun hm ↦ hmem ?_ - simpa [ha] using hm + have hcount : m.count a = 0 := by grind [Multiset.count_eq_zero_of_notMem] simp [hcount] private theorem bell_cons_mul_count (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) : @@ -133,12 +131,11 @@ private theorem bell_cons_mul_count (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) · intro _ hj simp [Finset.mem_erase.mp hj] let c := (m.map (· !)).prod * (m.count a)! * rest - have hm0 : m.bell * ((m.map (· !)).prod * (m.count a)! * rest) = m.sum ! := by + have hm0 : m.bell * c = m.sum ! := by have hm := Multiset.bell_mul_eq m rw [prod_count_factorial_eq_count_factorial_mul_prod_erase m ha] at hm - simpa [rest, mul_assoc, mul_comm, mul_left_comm] using hm - have hm : m.bell * a ! * c = m.sum ! * a ! := by - simpa [c, mul_assoc, mul_comm, mul_left_comm] using congrArg (a ! * ·) hm0 + simpa [c, rest, mul_assoc, mul_comm, mul_left_comm] using hm + have hm : m.sum ! * a ! = m.bell * a ! * c := by grind have ha_mem : a ∈ (a ::ₘ m).toFinset.erase 0 := by simp [ha] have hc : 0 < a ! * c := Nat.mul_pos (by positivity) <| Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity) @@ -149,7 +146,7 @@ private theorem bell_cons_mul_count (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) rw [← Finset.mul_prod_erase _ _ ha_mem, ← hrest] at hq simpa [c, Nat.factorial_succ, add_comm, mul_assoc, mul_left_comm] using hq _ = ((m.sum + a).choose a * m.bell) * (a ! * c) := by - simp [← Nat.add_choose_mul_factorial_mul_factorial, mul_assoc, ← hm] + simp [← Nat.add_choose_mul_factorial_mul_factorial, mul_assoc, hm] end Multiset @@ -254,9 +251,7 @@ theorem bell_eq_sum_erase {n : ℕ} (p : (n + 1).Partition) : ((p.parts.erase a).bell_cons_mul_count ha0).symm calc _ = (n + 1) * n.choose (a - 1) * (p.parts.erase a).bell := by ring - _ = (n + 1).choose a * a * (p.parts.erase a).bell := by - rw [Nat.add_one_mul_choose_eq, Nat.sub_add_cancel (by omega)] - _ = _ := by grind + _ = _ := by grind [Nat.add_one_mul_choose_eq] _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * p.parts.bell := by grind [Finset.sum_mul] _ = _ := by rw [succ_eq_add_one, mul_eq_mul_right_iff] From 60285ea542fdd47466f00de1fd6ddf4c80f1afa9 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 22 May 2026 17:12:24 +0800 Subject: [PATCH 30/39] golf --- Mathlib/Combinatorics/Enumerative/Bell.lean | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 7fe2f30abcfdc5..b17a59c9127b1d 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -113,15 +113,6 @@ theorem bell_eq (m : Multiset ℕ) : · rw [← Nat.pos_iff_ne_zero] exact Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity) -private theorem prod_count_factorial_eq_count_factorial_mul_prod_erase - (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) : ∏ j ∈ m.toFinset.erase 0, (m.count j)! = - (m.count a)! * ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! := by - by_cases hmem : a ∈ m.toFinset.erase 0 - · rw [← Finset.mul_prod_erase _ _ hmem] - · rw [Finset.erase_eq_of_notMem hmem] - have hcount : m.count a = 0 := by grind [Multiset.count_eq_zero_of_notMem] - simp [hcount] - private theorem bell_cons_mul_count (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) : (a ::ₘ m).bell * (a ::ₘ m).count a = (m.sum + a).choose a * m.bell := by let rest := ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! @@ -132,9 +123,12 @@ private theorem bell_cons_mul_count (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) simp [Finset.mem_erase.mp hj] let c := (m.map (· !)).prod * (m.count a)! * rest have hm0 : m.bell * c = m.sum ! := by - have hm := Multiset.bell_mul_eq m - rw [prod_count_factorial_eq_count_factorial_mul_prod_erase m ha] at hm - simpa [c, rest, mul_assoc, mul_comm, mul_left_comm] using hm + have hsplit : (m.count a)! * rest = ∏ j ∈ m.toFinset.erase 0, (m.count j)! := by + by_cases hmem : a ∈ m.toFinset.erase 0 + · rw [← Finset.mul_prod_erase _ _ hmem] + · have hcount : m.count a = 0 := by grind [Multiset.count_eq_zero_of_notMem] + simp [rest, Finset.erase_eq_of_notMem hmem, hcount] + simpa [c, hsplit, mul_assoc] using Multiset.bell_mul_eq m have hm : m.sum ! * a ! = m.bell * a ! * c := by grind have ha_mem : a ∈ (a ::ₘ m).toFinset.erase 0 := by simp [ha] have hc : 0 < a ! * c := Nat.mul_pos (by positivity) <| From ef050abab1099aec680182e7e361253f63669b28 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 22 May 2026 18:36:56 +0800 Subject: [PATCH 31/39] Update Mathlib/Combinatorics/Enumerative/Bell.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/Combinatorics/Enumerative/Bell.lean | 50 ++++++++++----------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index b17a59c9127b1d..cd61effca0f9b1 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -281,30 +281,30 @@ theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts. cases n with | zero => simp | succ n => - rw [Nat.bell_succ] - calc - _ = ∑ i : Fin n.succ, ∑ q : (n - i).Partition, n.choose i * q.parts.bell := by - congr! with i - simp [ih (n - i) _, Finset.mul_sum] - _ = ∑ i : Fin n.succ, ∑ p : {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}, - choose n i * (p.1.parts.erase (i + 1)).bell := by - congr! with i - have h1 : 1 ≤ (i + 1 : ℕ) := by omega - have h2 : (i + 1 : ℕ) ≤ n + 1 := by omega - have hsub : n + 1 - (i + 1 : ℕ) = n - i := by omega - exact hsub ▸ (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) _ _ (fun _ ↦ rfl)).symm - _ = ∑ x : Σ p : (n + 1).Partition, p.parts.toFinset, - choose n (x.2.1 - 1) * (x.1.parts.erase x.2.1).bell := by - rw [← Fintype.sum_sigma'] - refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ - simp [sigmaPartitionWithPartEquiv] - _ = ∑ p : (n + 1).Partition, ∑ a : p.parts.toFinset, - choose n (a - 1) * (p.parts.erase a).bell := - Fintype.sum_sigma' fun (p : (n + 1).Partition) (a : p.parts.toFinset) ↦ - choose n (a - 1) * (p.parts.erase a.1).bell - _ = _ := by - congr! with p - rw [← bell_eq_sum_erase p] - exact p.parts.toFinset.sum_coe_sort (fun a ↦ choose n (a - 1) * (p.parts.erase a).bell) + rw [Nat.bell_succ] + calc + _ = ∑ i : Fin n.succ, ∑ q : (n - i).Partition, n.choose i * q.parts.bell := by + congr! with i + simp [ih (n - i) _, Finset.mul_sum] + _ = ∑ i : Fin n.succ, ∑ p : {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}, + choose n i * (p.1.parts.erase (i + 1)).bell := by + congr! with i + have h1 : 1 ≤ (i + 1 : ℕ) := by omega + have h2 : (i + 1 : ℕ) ≤ n + 1 := by omega + have hsub : n + 1 - (i + 1 : ℕ) = n - i := by omega + exact hsub ▸ (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) _ _ (fun _ ↦ rfl)).symm + _ = ∑ x : Σ p : (n + 1).Partition, p.parts.toFinset, + choose n (x.2.1 - 1) * (x.1.parts.erase x.2.1).bell := by + rw [← Fintype.sum_sigma'] + refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ + simp [sigmaPartitionWithPartEquiv] + _ = ∑ p : (n + 1).Partition, ∑ a : p.parts.toFinset, + choose n (a - 1) * (p.parts.erase a).bell := + Fintype.sum_sigma' fun (p : (n + 1).Partition) (a : p.parts.toFinset) ↦ + choose n (a - 1) * (p.parts.erase a.1).bell + _ = _ := by + congr! with p + rw [← bell_eq_sum_erase p] + exact p.parts.toFinset.sum_coe_sort (fun a ↦ choose n (a - 1) * (p.parts.erase a).bell) end Nat From 350ef461a97c6912c5ff4b2e75030459a046575f Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 22 May 2026 18:59:00 +0800 Subject: [PATCH 32/39] use lia instead of omega --- Mathlib/Combinatorics/Enumerative/Bell.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index cd61effca0f9b1..85e33ae9d0863a 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -260,7 +260,7 @@ private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1 exact p.1.parts_pos (p.1.parts.erase_subset a hi) · have hs : a + (p.1.parts.erase a).sum = n + 1 := by simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) - omega + lia invFun q := ⟨⟨a ::ₘ q.parts, by grind, by simp [q.parts_sum, ha]⟩, by simp⟩ left_inv p := Subtype.ext <| Partition.ext <| cons_erase p.property right_inv q := Partition.ext <| erase_cons_head a q.parts @@ -289,9 +289,9 @@ theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts. _ = ∑ i : Fin n.succ, ∑ p : {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}, choose n i * (p.1.parts.erase (i + 1)).bell := by congr! with i - have h1 : 1 ≤ (i + 1 : ℕ) := by omega - have h2 : (i + 1 : ℕ) ≤ n + 1 := by omega - have hsub : n + 1 - (i + 1 : ℕ) = n - i := by omega + have h1 : 1 ≤ (i + 1 : ℕ) := by lia + have h2 : (i + 1 : ℕ) ≤ n + 1 := by lia + have hsub : n + 1 - (i + 1 : ℕ) = n - i := by lia exact hsub ▸ (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) _ _ (fun _ ↦ rfl)).symm _ = ∑ x : Σ p : (n + 1).Partition, p.parts.toFinset, choose n (x.2.1 - 1) * (x.1.parts.erase x.2.1).bell := by From 0fdbd3f94b5d340936b0fff916ceb431818bf664 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 22 May 2026 23:52:18 +0800 Subject: [PATCH 33/39] fix --- Mathlib/Combinatorics/Enumerative/Bell.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 85e33ae9d0863a..37dabb244df8fd 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -130,14 +130,13 @@ private theorem bell_cons_mul_count (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) simp [rest, Finset.erase_eq_of_notMem hmem, hcount] simpa [c, hsplit, mul_assoc] using Multiset.bell_mul_eq m have hm : m.sum ! * a ! = m.bell * a ! * c := by grind - have ha_mem : a ∈ (a ::ₘ m).toFinset.erase 0 := by simp [ha] have hc : 0 < a ! * c := Nat.mul_pos (by positivity) <| Nat.mul_pos (by simp [Nat.factorial_pos]) (by positivity) apply Nat.eq_of_mul_eq_mul_right hc calc _ = (m.sum + a)! := by have hq := Multiset.bell_mul_eq (a ::ₘ m) - rw [← Finset.mul_prod_erase _ _ ha_mem, ← hrest] at hq + rw [← Finset.mul_prod_erase _ _ (a := a) (by simp [*]), ← hrest] at hq simpa [c, Nat.factorial_succ, add_comm, mul_assoc, mul_left_comm] using hq _ = ((m.sum + a).choose a * m.bell) * (a ! * c) := by simp [← Nat.add_choose_mul_factorial_mul_factorial, mul_assoc, hm] @@ -277,10 +276,8 @@ private def sigmaPartitionWithPartEquiv (n : ℕ) : that `m.sum = n`. -/ theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts.bell := by refine Nat.strong_induction_on n ?_ - intro n ih - cases n with - | zero => simp - | succ n => + rintro (_ | n) ih + · simp rw [Nat.bell_succ] calc _ = ∑ i : Fin n.succ, ∑ q : (n - i).Partition, n.choose i * q.parts.bell := by From 3804209d8c08dad05f4d7ad930d1d6edb3611dc9 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 23 May 2026 21:49:47 +0800 Subject: [PATCH 34/39] golf using congr --- Mathlib/Combinatorics/Enumerative/Bell.lean | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 37dabb244df8fd..65a0eb19aab26b 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -80,9 +80,8 @@ theorem bell_mul_eq (m : Multiset ℕ) : unfold bell rw [← Nat.mul_right_inj (a := ∏ i ∈ m.toFinset, (i * count i m)!) (by positivity)] simp only [← mul_assoc, Nat.multinomial_spec] - simp only [mul_assoc] - rw [mul_comm] - apply congr_arg₂ + rw [mul_assoc, mul_assoc, mul_comm] + congr · rw [mul_comm, mul_assoc, ← Finset.prod_mul_distrib, Finset.prod_multiset_map_count] suffices this : _ by by_cases hm : 0 ∈ m.toFinset @@ -94,13 +93,11 @@ theorem bell_mul_eq (m : Multiset ℕ) : nth_rewrite 3 [← Finset.erase_eq_of_notMem hm] exact this rw [← Finset.prod_mul_distrib] - apply Finset.prod_congr rfl - intro x hx + congr! 1 with x hx rw [← mul_assoc, bell_mul_eq_lemma] simp only [Finset.mem_erase, ne_eq, mem_toFinset] at hx simp only [ne_eq, hx.1, not_false_eq_true] - · apply congr_arg - rw [Finset.sum_multiset_count] + · rw [Finset.sum_multiset_count] simp only [smul_eq_mul, mul_comm] theorem bell_eq (m : Multiset ℕ) : @@ -117,10 +114,10 @@ private theorem bell_cons_mul_count (m : Multiset ℕ) {a : ℕ} (ha : a ≠ 0) (a ::ₘ m).bell * (a ::ₘ m).count a = (m.sum + a).choose a * m.bell := by let rest := ∏ j ∈ (m.toFinset.erase 0).erase a, (m.count j)! have hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! := by - refine Finset.prod_congr ?_ ?_ + unfold rest + congr! 1 with j hj · grind [Multiset.toFinset_cons] - · intro _ hj - simp [Finset.mem_erase.mp hj] + · simp [Finset.mem_erase.mp hj] let c := (m.map (· !)).prod * (m.count a)! * rest have hm0 : m.bell * c = m.sum ! := by have hsplit : (m.count a)! * rest = ∏ j ∈ m.toFinset.erase 0, (m.count j)! := by From 5f83f7723f192080f18719e6d685d567135c6ec2 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 23 May 2026 22:29:56 +0800 Subject: [PATCH 35/39] use le instead of Fin --- Mathlib/Combinatorics/Enumerative/Bell.lean | 23 ++++++++++++--------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 65a0eb19aab26b..5b8e54b538e1bc 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -200,17 +200,17 @@ which counts the number of partitions of a set of cardinality `n`. -/ protected def bell : ℕ → ℕ | 0 => 1 - | n + 1 => ∑ i : Fin n.succ, choose n i * (n - i).bell + | n + 1 => ∑ i ≤ n, choose n i * (n - i).bell theorem bell_succ (n : ℕ) : - (n + 1).bell = ∑ i : Fin n.succ, choose n i * (n - i).bell := by + (n + 1).bell = ∑ i ≤ n, choose n i * (n - i).bell := by rw [Nat.bell] theorem bell_succ' (n : ℕ) : (n + 1).bell = ∑ ij ∈ Finset.antidiagonal n, choose n ij.1 * ij.2.bell := by rw [Nat.bell_succ, - Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y ↦ choose n x * y.bell) n, - Finset.sum_range] + ← Nat.range_succ_eq_Iic, + ← Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y ↦ choose n x * y.bell) n] @[simp] theorem bell_zero : Nat.bell 0 = 1 := by @@ -218,11 +218,13 @@ theorem bell_zero : Nat.bell 0 = 1 := by @[simp] theorem bell_one : Nat.bell 1 = 1 := by - simp [Nat.bell] + have : Finset.Iic 0 = {0} := Eq.symm (Finset.eq_of_veq rfl) + simp [Nat.bell, this] @[simp] theorem bell_two : Nat.bell 2 = 2 := by - simp [Nat.bell] + have : Finset.Iic 1 = {0, 1} := Finset.eq_of_veq rfl + simp [Nat.bell, this] theorem bell_eq_sum_erase {n : ℕ} (p : (n + 1).Partition) : ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell = p.parts.bell := by @@ -277,19 +279,20 @@ theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts. · simp rw [Nat.bell_succ] calc - _ = ∑ i : Fin n.succ, ∑ q : (n - i).Partition, n.choose i * q.parts.bell := by + _ = ∑ i ≤ n, ∑ q : (n - i).Partition, n.choose i * q.parts.bell := by congr! with i simp [ih (n - i) _, Finset.mul_sum] - _ = ∑ i : Fin n.succ, ∑ p : {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}, + _ = ∑ i ≤ n, ∑ p : {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}, choose n i * (p.1.parts.erase (i + 1)).bell := by - congr! with i + congr! with i hi + have : i ≤ n := Finset.mem_Iic.mp hi have h1 : 1 ≤ (i + 1 : ℕ) := by lia have h2 : (i + 1 : ℕ) ≤ n + 1 := by lia have hsub : n + 1 - (i + 1 : ℕ) = n - i := by lia exact hsub ▸ (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) _ _ (fun _ ↦ rfl)).symm _ = ∑ x : Σ p : (n + 1).Partition, p.parts.toFinset, choose n (x.2.1 - 1) * (x.1.parts.erase x.2.1).bell := by - rw [← Fintype.sum_sigma'] + rw [← Nat.range_succ_eq_Iic, Finset.sum_range, ← Fintype.sum_sigma'] refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ simp [sigmaPartitionWithPartEquiv] _ = ∑ p : (n + 1).Partition, ∑ a : p.parts.toFinset, From 4ef3081141de638bbf5891fc008e72cfe954b05d Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 20 Jun 2026 08:37:39 +0800 Subject: [PATCH 36/39] Apply suggestion from @eric-wieser Co-authored-by: Eric Wieser --- Mathlib/Combinatorics/Enumerative/Bell.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index 5b8e54b538e1bc..e5d307a0d49df4 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -250,13 +250,15 @@ theorem bell_eq_sum_erase {n : ℕ} (p : (n + 1).Partition) : left simpa [smul_eq_mul, p.parts_sum] using (Finset.sum_multiset_count p.parts).symm -private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n + 1) : - {p : (n + 1).Partition // a ∈ p.parts} ≃ (n + 1 - a).Partition where +private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) : + {p : n.Partition // a ∈ p.parts} ≃ (n - a).Partition where toFun p := by refine ⟨p.1.parts.erase a, ?_, ?_⟩ · intro _ hi exact p.1.parts_pos (p.1.parts.erase_subset a hi) - · have hs : a + (p.1.parts.erase a).sum = n + 1 := by + · cases n + · lia + have hs : a + (p.1.parts.erase a).sum = n + 1 := by simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) lia invFun q := ⟨⟨a ::ₘ q.parts, by grind, by simp [q.parts_sum, ha]⟩, by simp⟩ From ba0928cb666ff66ff08aa33f62ea998114beafc1 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 20 Jun 2026 09:13:02 +0800 Subject: [PATCH 37/39] apply suggestions --- Mathlib/Combinatorics/Enumerative/Bell.lean | 31 ++++++++------------- 1 file changed, 11 insertions(+), 20 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index cc7bd404f7f4d8..e9b3a15e4777df 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -227,28 +227,21 @@ theorem bell_two : Nat.bell 2 = 2 := by simp [Nat.bell, this] theorem bell_eq_sum_erase {n : ℕ} (p : (n + 1).Partition) : - ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell = p.parts.bell := by + p.parts.bell = ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell := by apply Nat.eq_of_mul_eq_mul_left n.succ_pos calc + _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * p.parts.bell := by + rw [succ_eq_add_one, mul_eq_mul_right_iff] + left + simpa [smul_eq_mul, p.parts_sum] using Finset.sum_multiset_count p.parts + _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * p.parts.bell) := by grind [Finset.sum_mul] _ = ∑ a ∈ p.parts.toFinset, (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell) := by - rw [Finset.mul_sum] - _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * p.parts.bell) := by congr! 1 with a ha - have ha_mem : a ∈ p.parts := mem_dedup.mp ha have ha0 : a ≠ 0 := by grind have hsum : (p.parts.erase a).sum + a = n + 1 := by - simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (Multiset.cons_erase ha_mem) - have hbell : (n + 1).choose a * (p.parts.erase a).bell = p.parts.count a * p.parts.bell := by - simpa [hsum, cons_erase ha_mem, mul_comm] using - ((p.parts.erase a).bell_cons_mul_count ha0).symm - calc - _ = (n + 1) * n.choose (a - 1) * (p.parts.erase a).bell := by ring - _ = _ := by grind [Nat.add_one_mul_choose_eq] - _ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * p.parts.bell := by grind [Finset.sum_mul] - _ = _ := by - rw [succ_eq_add_one, mul_eq_mul_right_iff] - left - simpa [smul_eq_mul, p.parts_sum] using (Finset.sum_multiset_count p.parts).symm + simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (cons_erase (mem_dedup.mp ha)) + grind [Nat.add_one_mul_choose_eq, cons_erase, bell_cons_mul_count] + _ = _ := by rw [Finset.mul_sum] private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) : {p : n.Partition // a ∈ p.parts} ≃ (n - a).Partition where @@ -256,9 +249,7 @@ private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) : refine ⟨p.1.parts.erase a, ?_, ?_⟩ · intro _ hi exact p.1.parts_pos (p.1.parts.erase_subset a hi) - · cases n - · lia - have hs : a + (p.1.parts.erase a).sum = n + 1 := by + · have hs : a + (p.1.parts.erase a).sum = n := by simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) lia invFun q := ⟨⟨a ::ₘ q.parts, by grind, by simp [q.parts_sum, ha]⟩, by simp⟩ @@ -303,7 +294,7 @@ theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts. choose n (a - 1) * (p.parts.erase a.1).bell _ = _ := by congr! with p - rw [← bell_eq_sum_erase p] + rw [bell_eq_sum_erase p] exact p.parts.toFinset.sum_coe_sort (fun a ↦ choose n (a - 1) * (p.parts.erase a).bell) end Nat From d5566e87aae97735f245db9d49f7075969644eec Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Wed, 24 Jun 2026 09:31:51 +0800 Subject: [PATCH 38/39] apply suggestions --- Mathlib/Combinatorics/Enumerative/Bell.lean | 18 ++---------------- .../Enumerative/Partition/Basic.lean | 16 ++++++++++++++++ 2 files changed, 18 insertions(+), 16 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index e9b3a15e4777df..b4a6ea99c6b401 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -243,19 +243,6 @@ theorem bell_eq_sum_erase {n : ℕ} (p : (n + 1).Partition) : grind [Nat.add_one_mul_choose_eq, cons_erase, bell_cons_mul_count] _ = _ := by rw [Finset.mul_sum] -private def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) : - {p : n.Partition // a ∈ p.parts} ≃ (n - a).Partition where - toFun p := by - refine ⟨p.1.parts.erase a, ?_, ?_⟩ - · intro _ hi - exact p.1.parts_pos (p.1.parts.erase_subset a hi) - · have hs : a + (p.1.parts.erase a).sum = n := by - simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) - lia - invFun q := ⟨⟨a ::ₘ q.parts, by grind, by simp [q.parts_sum, ha]⟩, by simp⟩ - left_inv p := Subtype.ext <| Partition.ext <| cons_erase p.property - right_inv q := Partition.ext <| erase_cons_head a q.parts - private def sigmaPartitionWithPartEquiv (n : ℕ) : (Σ i : Fin n.succ, {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts}) ≃ Σ p : (n + 1).Partition, {a : ℕ // a ∈ p.parts.toFinset} where @@ -282,14 +269,13 @@ theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts. have h1 : 1 ≤ (i + 1 : ℕ) := by lia have h2 : (i + 1 : ℕ) ≤ n + 1 := by lia have hsub : n + 1 - (i + 1 : ℕ) = n - i := by lia - exact hsub ▸ (Fintype.sum_equiv (partitionWithPartEquiv h1 h2) _ _ (fun _ ↦ rfl)).symm + exact hsub ▸ (Fintype.sum_equiv (Partition.partitionWithPartEquiv h1 h2) _ _ (fun _ ↦ rfl)).symm _ = ∑ x : Σ p : (n + 1).Partition, p.parts.toFinset, choose n (x.2.1 - 1) * (x.1.parts.erase x.2.1).bell := by rw [← Nat.range_succ_eq_Iic, Finset.sum_range, ← Fintype.sum_sigma'] refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_ simp [sigmaPartitionWithPartEquiv] - _ = ∑ p : (n + 1).Partition, ∑ a : p.parts.toFinset, - choose n (a - 1) * (p.parts.erase a).bell := + _ = ∑ p : (n + 1).Partition, ∑ a : p.parts.toFinset, choose n (a - 1) * (p.parts.erase a).bell := Fintype.sum_sigma' fun (p : (n + 1).Partition) (a : p.parts.toFinset) ↦ choose n (a - 1) * (p.parts.erase a.1).bell _ = _ := by diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean index 4bb7639e6fa7b9..c28ee24412265f 100644 --- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean +++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean @@ -138,6 +138,22 @@ def toFinsuppAntidiag {n : ℕ} (p : Partition n) : ℕ →₀ ℕ where suffices m ∈ p.parts → m ≠ 0 by simpa grind +/-- If `1 ≤ a` and `a ≤ n`, partitions of `n` containing `a` as a part are equivalent to +partitions of `n - a`. The forward map removes one occurrence of `a`, and the inverse adds `a` as +a part. -/ +def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) : + {p : n.Partition // a ∈ p.parts} ≃ (n - a).Partition where + toFun p := by + refine ⟨p.1.parts.erase a, ?_, ?_⟩ + · intro _ hi + exact p.1.parts_pos (p.1.parts.erase_subset a hi) + · have hs : a + (p.1.parts.erase a).sum = n := by + simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) + lia + invFun q := ⟨⟨a ::ₘ q.parts, by grind, by simp [q.parts_sum, ha]⟩, by simp⟩ + left_inv p := Subtype.ext <| Partition.ext <| cons_erase p.property + right_inv q := Partition.ext <| erase_cons_head a q.parts + theorem toFinsuppAntidiag_injective (n : ℕ) : Function.Injective (toFinsuppAntidiag (n := n)) := by unfold toFinsuppAntidiag intro p q h From 1c94f31a337e68c55c0a8bfc61e8c34b386cd1f7 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sun, 28 Jun 2026 22:30:08 +0800 Subject: [PATCH 39/39] fix --- .../Enumerative/Partition/Basic.lean | 43 ++++++++++++------- 1 file changed, 27 insertions(+), 16 deletions(-) diff --git a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean index c28ee24412265f..935de73ea4c4a9 100644 --- a/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean +++ b/Mathlib/Combinatorics/Enumerative/Partition/Basic.lean @@ -138,22 +138,6 @@ def toFinsuppAntidiag {n : ℕ} (p : Partition n) : ℕ →₀ ℕ where suffices m ∈ p.parts → m ≠ 0 by simpa grind -/-- If `1 ≤ a` and `a ≤ n`, partitions of `n` containing `a` as a part are equivalent to -partitions of `n - a`. The forward map removes one occurrence of `a`, and the inverse adds `a` as -a part. -/ -def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) : - {p : n.Partition // a ∈ p.parts} ≃ (n - a).Partition where - toFun p := by - refine ⟨p.1.parts.erase a, ?_, ?_⟩ - · intro _ hi - exact p.1.parts_pos (p.1.parts.erase_subset a hi) - · have hs : a + (p.1.parts.erase a).sum = n := by - simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) - lia - invFun q := ⟨⟨a ::ₘ q.parts, by grind, by simp [q.parts_sum, ha]⟩, by simp⟩ - left_inv p := Subtype.ext <| Partition.ext <| cons_erase p.property - right_inv q := Partition.ext <| erase_cons_head a q.parts - theorem toFinsuppAntidiag_injective (n : ℕ) : Function.Injective (toFinsuppAntidiag (n := n)) := by unfold toFinsuppAntidiag intro p q h @@ -245,6 +229,33 @@ theorem countRestricted_two (n : ℕ) : countRestricted n 2 = distincts n := by def oddDistincts (n : ℕ) : Finset n.Partition := odds n ∩ distincts n +/-- If `1 ≤ a` and `a ≤ n`, partitions of `n` containing `a` as a part are equivalent to +partitions of `n - a`. The forward map removes one occurrence of `a`, and the inverse adds `a` as +a part. -/ +def partitionWithPartEquiv {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) : + {p : n.Partition // a ∈ p.parts} ≃ (n - a).Partition where + toFun p := by + refine ⟨p.1.parts.erase a, ?_, ?_⟩ + · intro _ hi + exact p.1.parts_pos (p.1.parts.erase_subset a hi) + · have hs : a + (p.1.parts.erase a).sum = n := by + simpa [p.1.parts_sum] using congrArg Multiset.sum (Multiset.cons_erase p.2) + lia + invFun q := ⟨⟨a ::ₘ q.parts, by grind, by simp [q.parts_sum, ha]⟩, by simp⟩ + left_inv p := Subtype.ext <| Partition.ext <| cons_erase p.property + right_inv q := Partition.ext <| erase_cons_head a q.parts + +@[simp] +theorem partitionWithPartEquiv_apply_parts {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) + (p : {p : n.Partition // a ∈ p.parts}) : + (partitionWithPartEquiv ha1 ha p).parts = p.1.parts.erase a := by + dsimp [partitionWithPartEquiv] + +@[simp] +theorem partitionWithPartEquiv_symm_apply_parts {n a : ℕ} (ha1 : 1 ≤ a) (ha : a ≤ n) + (p : (n - a).Partition) : ((partitionWithPartEquiv ha1 ha).symm p).1.parts = a ::ₘ p.parts := by + dsimp [partitionWithPartEquiv] + end Partition end Nat