Charging the moves of a permutation of Fin L across the gaps between points

For a permutation σ of Fin L, a point x with σ x < x crosses the gaps c with σ x < c ≤ x, at depth x - c, and a point with x < σ x crosses the gaps c with x < c ≤ σ x. The points with x < σ x are ranked by decreasing image (Equiv.Perm.upRank). On every set of forward-moved points closed under passing to larger images, the ranks enumerate an initial segment (Equiv.Perm.image_upRank).

The backward moves have the same total length as the forward ones (Equiv.Perm.sum_tsub_comp_eq_sum_comp_tsub). At each gap as many points cross forward as backward. If σ moves the points below N forward and the others backward, then below every threshold there are at most as many backward depths as forward ranks at each gap (Equiv.Perm.card_cross_backward_le). Charging a backward move across j gaps by ρ₀, …, ρⱼ₋₁ and every gap crossed by a forward move by ρ at its rank, the backward charges are therefore dominated by the forward ones for a nonnegative antitone ρ (Equiv.Perm.prod_prod_range_le_prod_pow_upRank). This is the combinatorial core of Coleman's coefficient bound, read off the Leibniz expansion of a Sylvester matrix.

Main results

• Equiv.Perm.prod_upRank: products along the ranks of the forward-moved points are products over an initial segment.
• Equiv.Perm.prod_prod_range_le_prod_pow_upRank: the crossing estimate.

References

• R. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), 417–479, Appendix A3.

def Equiv.Perm.upRank {L : ℕ} (σ : Perm (Fin L)) (x : Fin L) : ℕ

The rank of x among the points moved forward by σ, ordered by decreasing image.

theorem Equiv.Perm.upRank_def {L : ℕ} (σ : Perm (Fin L)) (x : Fin L) : σ.upRank x = {y : Fin L | ↑y < ↑(σ y) ∧ ↑(σ x) < ↑(σ y)}.card

The rank of x counts the forward-moved points whose image exceeds that of x.

theorem Equiv.Perm.upRank_injOn {L : ℕ} (σ : Perm (Fin L)) : Set.InjOn σ.upRank {x : Fin L | ↑x < ↑(σ x)}

Distinct forward-moved points have distinct ranks, since their images are distinct.

theorem Equiv.Perm.image_upRank {L : ℕ} (σ : Perm (Fin L)) {S : Finset (Fin L)} (hS : ∀ x ∈ S, ↑x < ↑(σ x)) (hclosed : ∀ x ∈ S, ∀ (y : Fin L), ↑y < ↑(σ y) → ↑(σ x) < ↑(σ y) → y ∈ S) : Finset.image σ.upRank S = Finset.range S.card

On a set of forward-moved points closed under passing to larger images, the ranks enumerate range of its size.

theorem Equiv.Perm.card_filter_upRank_lt {L : ℕ} (σ : Perm (Fin L)) {S : Finset (Fin L)} (hS : ∀ x ∈ S, ↑x < ↑(σ x)) (hclosed : ∀ x ∈ S, ∀ (y : Fin L), ↑y < ↑(σ y) → ↑(σ x) < ↑(σ y) → y ∈ S) {t : ℕ} (ht : t ≤ S.card) : {x ∈ S | σ.upRank x < t}.card = t

On a set of forward-moved points closed under passing to larger images, exactly t points have rank below t, for t at most its size.

theorem Equiv.Perm.upRank_lt_card {L : ℕ} (σ : Perm (Fin L)) {x : Fin L} (hx : ↑x < ↑(σ x)) : σ.upRank x < {y : Fin L | ↑y < ↑(σ y)}.card

The rank of a forward-moved point is less than the number of forward-moved points.

theorem Equiv.Perm.prod_upRank {L : ℕ} (σ : Perm (Fin L)) {M : Type u_1} [CommMonoid M] (β : ℕ → M) : ∏ x : Fin L with ↑x < ↑(σ x), β (σ.upRank x) = ∏ t ∈ Finset.range {x : Fin L | ↑x < ↑(σ x)}.card, β t

The products of a sequence along the ranks of the forward-moved points are its products over an initial segment.

theorem Equiv.Perm.card_cross_backward_le_sub_max {L : ℕ} (σ : Perm (Fin L)) {N : ℕ} (hfwd : ∀ (x : Fin L), ↑x < N → ↑x ≤ ↑(σ x)) (c t : ℕ) : {x : Fin L | (↑(σ x) < c ∧ c ≤ ↑x) ∧ ↑x - c < t}.card ≤ c + t - max c N

Backward crossings at depth below t. If σ moves the points below N forward, then the points that cross the gap c backward at depth below t number at most c + t - max c N.

theorem Equiv.Perm.card_cross_backward_le {L : ℕ} (σ : Perm (Fin L)) {N : ℕ} (hfwd : ∀ (x : Fin L), ↑x < N → ↑x ≤ ↑(σ x)) (hbwd : ∀ (x : Fin L), N ≤ ↑x → ↑(σ x) ≤ ↑x) (c t : ℕ) : {x : Fin L | (↑(σ x) < c ∧ c ≤ ↑x) ∧ ↑x - c < t}.card ≤ {x : Fin L | (↑x < c ∧ c ≤ ↑(σ x)) ∧ σ.upRank x < t}.card

Charges at one gap. If σ moves the points below N forward and the others backward, then for every t, at most as many backward moves cross the gap c at depth below t as forward moves of rank below t.

theorem Equiv.Perm.prod_prod_range_le_prod_pow_upRank {L : ℕ} (σ : Perm (Fin L)) {N : ℕ} (hfwd : ∀ (x : Fin L), ↑x < N → ↑x ≤ ↑(σ x)) (hbwd : ∀ (x : Fin L), N ≤ ↑x → ↑(σ x) ≤ ↑x) {R : Type u_1} [CommMonoidWithZero R] [Preorder R] [ZeroLEOneClass R] [PosMulMono R] {ρ : ℕ → R} (hρ₀ : ∀ (i : ℕ), 0 ≤ ρ i) (hρ : Antitone ρ) : ∏ x : Fin L, ∏ i ∈ Finset.range (↑x - ↑(σ x)), ρ i ≤ ∏ x : Fin L, ρ (σ.upRank x) ^ (↑(σ x) - ↑x)

Crossing estimate. If σ moves the points below N forward and the others backward, and ρ is a nonnegative antitone sequence, then the product over the backward moves of ∏ i < x - σ x, ρ i is at most the product over the forward moves of ρ (rank x) ^ (σ x - x).