Helper lemmas for Franklin's involution

Helper lemmas about consecutiveTopRun, partition membership, and properties of αOp/βOp.

Main results

• ctr_zero, ctr_succ: defining equations for consecutiveTopRun
• ctr_eq_of: the characterisation of consecutiveTopRun S m as the unique r with m - j ∈ S for all j < r and m - r ∉ S
• mem_DP: membership in distinctPartitions
• sum_Icc_id_mul_two, Icc_sum_id: Gauss' summation formula over Finset.Icc in ℕ
• consecutiveTopRun_Icc, partBase_Icc, partMax_Icc, partSlope_Icc: the structural invariants of an interval, which is the shape both pentagonal families smkSet/spkSet take

@[simp]

theorem ctr_zero (S : Finset ℕ) : consecutiveTopRun S 0 = if 0 ∈ S then 1 else 0

Base case: consecutiveTopRun S 0 = 1 if 0 ∈ S, else 0.

@[simp]

theorem ctr_succ (S : Finset ℕ) (m : ℕ) : consecutiveTopRun S (m + 1) = if m + 1 ∈ S then 1 + consecutiveTopRun S m else 0

Recurrence: consecutiveTopRun S (m+1) is 1 + consecutiveTopRun S m if m+1 ∈ S, else 0.

theorem ctr_not_mem (S : Finset ℕ) (m : ℕ) (h : m ∉ S) : consecutiveTopRun S m = 0

If m ∉ S then consecutiveTopRun S m = 0.

theorem ctr_pos_of_mem (S : Finset ℕ) (m : ℕ) (h : m ∈ S) : 0 < consecutiveTopRun S m

If m ∈ S then consecutiveTopRun S m > 0.

theorem ctr_le (S : Finset ℕ) (m : ℕ) (h : 0 ∉ S) : consecutiveTopRun S m ≤ m

If 0 ∉ S then consecutiveTopRun S m ≤ m.

theorem ctr_mem_of_lt (S : Finset ℕ) (m j : ℕ) (hj : j < consecutiveTopRun S m) : m - j ∈ S

If j < consecutiveTopRun S m then m - j ∈ S.

theorem ctr_ge_of_mem (S : Finset ℕ) (m r : ℕ) (hrm : r ≤ m) (h : ∀ j < r, m - j ∈ S) : r ≤ consecutiveTopRun S m

Lower bound for consecutiveTopRun: a run of length r below m forces r ≤ consecutiveTopRun S m.

theorem ctr_eq_of (S : Finset ℕ) (m r : ℕ) (hrm : r ≤ m) (hmem : ∀ j < r, m - j ∈ S) (hnot : m - r ∉ S) : consecutiveTopRun S m = r

consecutiveTopRun S m is the unique r ≤ m with m - j ∈ S for every j < r and m - r ∉ S.

theorem ctr_not_mem_boundary (S : Finset ℕ) (m : ℕ) (h0 : 0 ∉ S) (hm : m ∈ S) : m - consecutiveTopRun S m ∉ S

If 0 ∉ S and m ∈ S then m - consecutiveTopRun S m ∉ S.

theorem mem_DP (n : ℕ) (S : Finset ℕ) : S ∈ distinctPartitions n ↔ S ⊆ Finset.Icc 1 n ∧ S.sum id = n

S ∈ distinctPartitions n iff S ⊆ Icc 1 n and S.sum id = n.

theorem DP_pos_mem (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitions n) {x : ℕ} (hx : x ∈ S) : 1 ≤ x

Every element of a distinct partition of n is positive.

theorem DP_le_mem (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitions n) {x : ℕ} (hx : x ∈ S) : x ≤ n

Every element of S ∈ distinctPartitions n is at most n.

theorem DP_zero_not_mem (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitions n) : 0 ∉ S

0 is not in any distinct partition.

theorem DP_sum (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitions n) : S.sum id = n

The sum of a distinct partition of n equals n.

theorem DPalpha_mem_DP (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : S ∈ distinctPartitions n

Every α-partition is a distinct partition.

theorem DPbeta_mem_DP (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : S ∈ distinctPartitions n

Every β-partition is a distinct partition.

theorem DPalpha_nonempty (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : S.Nonempty

Every α-partition is nonempty.

theorem DPbeta_nonempty (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : S.Nonempty

Every β-partition is nonempty.

theorem partBase_mem (S : Finset ℕ) (hne : S.Nonempty) : partBase S ∈ S

partBase S ∈ S for nonempty S.

theorem partMax_mem (S : Finset ℕ) (hne : S.Nonempty) : partMax S ∈ S

partMax S ∈ S for nonempty S.

theorem partBase_le (S : Finset ℕ) (hne : S.Nonempty) {x : ℕ} (hx : x ∈ S) : partBase S ≤ x

partBase S ≤ x for any x ∈ S.

theorem le_partMax (S : Finset ℕ) (hne : S.Nonempty) {x : ℕ} (hx : x ∈ S) : x ≤ partMax S

x ≤ partMax S for any x ∈ S.

theorem partBase_le_partMax (S : Finset ℕ) (hne : S.Nonempty) : partBase S ≤ partMax S

partBase S ≤ partMax S for nonempty S.

theorem partSlope_pos (S : Finset ℕ) (hne : S.Nonempty) : 0 < partSlope S

partSlope S > 0 when S is nonempty.

theorem partSlope_le_partMax (S : Finset ℕ) (h0 : 0 ∉ S) : partSlope S ≤ partMax S

partSlope S ≤ partMax S when 0 ∉ S.

theorem DPalpha_base_le_slope (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : partBase S ≤ partSlope S

For S ∈ α(n), partBase S ≤ partSlope S.

theorem DPbeta_slope_lt_base (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : partSlope S < partBase S

For S ∈ β(n), partSlope S < partBase S.

theorem DPalpha_max_ge_2base (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : 2 * partBase S ≤ partMax S

For S ∈ α(n), partMax S ≥ 2 * partBase S.

theorem DPbeta_max_ge_2slope_add_1 (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : 2 * partSlope S + 1 ≤ partMax S

For S ∈ β(n), partMax S ≥ 2 * partSlope S + 1.

Intervals

Both pentagonal families are intervals — smkSet k = Icc k (2 * k - 1) and spkSet k = Icc (k + 1) (2 * k) — and a special partition is an interval too (DPspecial_* in Lemmas.lean). The lemmas below compute the sum and the three structural invariants of an arbitrary Finset.Icc a b once and for all.

theorem sum_Icc_id_mul_two (a b : ℕ) : (∑ i ∈ Finset.Icc a b, i) * 2 = (b + 1 - a) * (a + b)

Gauss' summation formula over Finset.Icc in ℕ, in * 2 form: no division and no truncated subtraction on the left. Unconditional — both sides are 0 when b < a.

theorem sum_Icc_id (a b : ℕ) : ∑ i ∈ Finset.Icc a b, i = (b + 1 - a) * (a + b) / 2

Gauss' summation formula over Finset.Icc in ℕ.

theorem Icc_sum_id_mul_two (a b : ℕ) : (Finset.Icc a b).sum id * 2 = (b + 1 - a) * (a + b)

sum_Icc_id_mul_two in Finset.sum _ id phrasing, which is what distinctPartitions uses. rw cannot see through id, so this restatement is what call sites need.

theorem Icc_sum_id (a b : ℕ) : (Finset.Icc a b).sum id = (b + 1 - a) * (a + b) / 2

sum_Icc_id in Finset.sum _ id phrasing.

theorem consecutiveTopRun_Icc (a b m : ℕ) : consecutiveTopRun (Finset.Icc a b) m = if a ≤ m ∧ m ≤ b then m - a + 1 else 0

The consecutive-run function on an interval: every element of Icc a b continues the run back down to a, and everything outside has run length 0.

theorem partBase_Icc {a b : ℕ} (hab : a ≤ b) : partBase (Finset.Icc a b) = a

The base of a nonempty interval is its left endpoint.

theorem partMax_Icc {a b : ℕ} (hab : a ≤ b) : partMax (Finset.Icc a b) = b

The max of a nonempty interval is its right endpoint.

theorem partSlope_Icc {a b : ℕ} (hab : a ≤ b) : partSlope (Finset.Icc a b) = b - a + 1

A nonempty interval is one single run, so its slope is its whole length.

theorem DPalpha_m_sub_b_add_1_mem (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : partMax S - partBase S + 1 ∈ S

For S ∈ α(n), partMax S - partBase S + 1 ∈ S.

theorem DPalpha_base_ne_m_sub_b_add_1 (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : partBase S ≠ partMax S - partBase S + 1

For S ∈ α(n), partBase S ≠ partMax S - partBase S + 1.

theorem partMax_succ_not_mem (S : Finset ℕ) (hne : S.Nonempty) : partMax S + 1 ∉ S

partMax S + 1 ∉ S for nonempty S.

theorem mem_alphaOp {S : Finset ℕ} {x : ℕ} : x ∈ alphaOp S ↔ x = partMax S + 1 ∨ x ≠ partMax S - partBase S + 1 ∧ x ≠ partBase S ∧ x ∈ S

Membership in αOp S, with the two lets of the definition unfolded.

theorem alphaOp_sum (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : (alphaOp S).sum id = S.sum id

The α-operation preserves the sum of parts.

theorem alphaOp_partMax (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : partMax (alphaOp S) = partMax S + 1

For S ∈ α(n), partMax (αOp S) = partMax S + 1.

theorem alphaOp_partSlope (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsAlpha n) : partSlope (alphaOp S) = partBase S

For S ∈ α(n), partSlope (αOp S) = partBase S.

theorem DPbeta_slope_not_mem (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : partSlope S ∉ S

For S ∈ β(n), partSlope S ∉ S.

theorem DPbeta_m_sub_s_not_mem (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : partMax S - partSlope S ∉ S

For S ∈ β(n), partMax S - partSlope S ∉ S.

theorem DPbeta_slope_ne_m_sub_slope (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : partSlope S ≠ partMax S - partSlope S

For S ∈ β(n), partSlope S ≠ partMax S - partSlope S.

theorem betaOp_eq (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : betaOp S = insert (partSlope S) (insert (partMax S - partSlope S) (S.erase (partMax S)))

For S ∈ β(n), βOp S inserts the slope and partMax S - partSlope S into S, after deleting the maximum.

theorem betaOp_sum (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : (betaOp S).sum id = S.sum id

The β-operation preserves the sum of parts.

theorem betaOp_partMax (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : partMax (betaOp S) = partMax S - 1

For S ∈ β(n), partMax (βOp S) = partMax S - 1.

theorem betaOp_partBase (n : ℕ) (S : Finset ℕ) (hS : S ∈ distinctPartitionsBeta n) : partBase (betaOp S) = partSlope S

For S ∈ β(n), partBase (βOp S) = partSlope S.