Statistic values on an inserted Boolean chain

This file connects the concrete inserted Boolean chain to the abstract A/B statistic sequences used in the mass-transport proof of Theorem 2.1.

noncomputable def Feige.insertionLowerK {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (r : ℕ) : ℝ

The Bᵣ value at the lifted lower state Cᵣ, extended by zero after the old chain's sentinel.

Equations

• Feige.insertionLowerK γ β σ r = if hr : r < n + 1 then Feige.twoPointKFinset γ β (Feige.liftChainState (Feige.chainState σ ⟨r, hr⟩)) else 0

noncomputable def Feige.insertionUpperK {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (r : ℕ) : ℝ

The Aᵣ value at the lifted upper state Hᵣ, extended by zero after the old chain's sentinel.

Equations

• Feige.insertionUpperK γ β σ r = if hr : r < n + 1 then Feige.twoPointKFinset γ β (insert (Fin.last n) (Feige.liftChainState (Feige.chainState σ ⟨r, hr⟩))) else 0

noncomputable def Feige.insertionOldK {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (r : ℕ) : ℝ

The old n-coordinate statistic sequence Fᵣ, including its zero sentinel.

Equations

• Feige.insertionOldK γ β σ r = Feige.booleanChainK (fun (i : Fin n) => γ i.castSucc) (fun (i : Fin n) => β i.castSucc) σ r

noncomputable def Feige.insertionWidth {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (r : ℕ) : ℝ

Band width wᵣ = Bᵣ - Aᵣ.

Equations

• Feige.insertionWidth γ β σ r = Feige.insertionLowerK γ β σ r - Feige.insertionUpperK γ β σ r

noncomputable def Feige.insertionTheta {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (r : ℕ) : ℝ

Conditional interpolation parameter θᵣ = (Fᵣ - Aᵣ) / (Bᵣ - Aᵣ).

Equations

• Feige.insertionTheta γ β σ r = (Feige.insertionOldK γ β σ r - Feige.insertionUpperK γ β σ r) / Feige.insertionWidth γ β σ r

theorem Feige.insertionWidth_nonneg {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (hγ : ∀ (i : Fin (n + 1)), 0 ≤ γ i) (hβ : ∀ (i : Fin (n + 1)), 0 ≤ β i) (r : ℕ) : 0 ≤ insertionWidth γ β σ r

Monotonicity of K makes every insertion band width nonnegative.

theorem Feige.insertionOldK_eq_upper_add_theta_mul_width {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (r : ℕ) (hw : insertionWidth γ β σ r ≠ 0) : insertionOldK γ β σ r = insertionUpperK γ β σ r + insertionTheta γ β σ r * insertionWidth γ β σ r

The defining interpolation identity, whenever the band has positive width (nonzero is algebraically sufficient).

theorem Feige.insertionOldK_eq_upper_add_theta_mul_width_all {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (hw : ∀ r < n + 1, insertionWidth γ β σ r ≠ 0) (r : ℕ) : insertionOldK γ β σ r = insertionUpperK γ β σ r + insertionTheta γ β σ r * insertionWidth γ β σ r

The interpolation identity on the whole zero-extended sequence, given nondegeneracy of every genuine insertion band.

@[simp]

theorem Feige.insertionTheta_sentinel {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) : insertionTheta γ β σ (n + 1) = 0

theorem Feige.insertionOldK_zero_eq_lowerK_zero {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (hγ : ∀ (i : Fin (n + 1)), 0 ≤ γ i) : insertionOldK γ β σ 0 = 1 ∧ insertionLowerK γ β σ 0 = 1

The initial old and lower statistic values both equal one.

theorem Feige.insertionTheta_zero {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (hγ : ∀ (i : Fin (n + 1)), 0 ≤ γ i) (hw : insertionWidth γ β σ 0 ≠ 0) : insertionTheta γ β σ 0 = 1

The initial interpolation parameter is one when its band is nondegenerate.

theorem Feige.booleanChainK_insertChainPerm_eq {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (r : Fin (n + 2)) : booleanChainK γ β (insertChainPerm σ J) ↑r = insertionStatisticSequence (insertionUpperK γ β σ) (insertionLowerK γ β σ) ↑J ↑r

At every genuine level, the statistic along the inserted permutation is exactly Bᵣ before insertion and Aᵣ₋₁ afterwards.

theorem Feige.booleanChainK_insertChainPerm_eq_nat {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (r : ℕ) : booleanChainK γ β (insertChainPerm σ J) r = insertionStatisticSequence (insertionUpperK γ β σ) (insertionLowerK γ β σ) (↑J) r

The preceding identity, including the zero sentinel and the zero extension beyond it.

theorem Feige.chainMass_booleanChainK_insert_lower {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (J j : Fin (n + 1)) (hjJ : j ≤ J) : chainMass (booleanChainK γ β (insertChainPerm σ J)) ↑j = lowerMassForInsertion (insertionLowerK γ β σ) (fun (r : ℕ) => insertionLowerK γ β σ r - insertionUpperK γ β σ r) ↑J ↑j

The actual chain mass at a present lower state Cⱼ is its lower rank contribution.

theorem Feige.chainMass_booleanChainK_insert_upper {n : ℕ} (γ β : Fin (n + 1) → ℝ) (σ : Equiv.Perm (Fin n)) (J j : Fin (n + 1)) (hJj : J ≤ j) : chainMass (booleanChainK γ β (insertChainPerm σ J)) (↑j + 1) = upperMassForInsertion (insertionUpperK γ β σ) ↑J ↑j

The actual chain mass at a present upper state Hⱼ is its upper rank contribution, including the terminal edge to the zero sentinel.