Up/Down operators and Theorem 4.7 for the Boolean algebra

This file formalizes Theorem 4.7 from Stanley's Algebraic Combinatorics.

Main results

• adjointness — ⟨up v, w⟩ = ⟨v, down w⟩ (key technical lemma)
• DU_form_eq_inner_up — DU_form(v,v) = ‖U(v)‖²
• UD_form_succ_eq_inner_down — UD_form(v,v) = ‖D(v)‖²
• DU_minus_UD — Lemma 4.6: DU − UD = (n − 2i)·I (bilinear form version)
• up_ker_trivial — kernel of Uᵢ is trivial when 2i < n (quadratic form argument)
• up_injective — Theorem 4.7: Uᵢ is injective when 2i < n
• up_surjective — Theorem 4.7: Uᵢ is surjective when n ≤ 2i

@[reducible, inline]

abbrev BooleanUpDown.Level (n i : ℕ) : Type

The i-th level of the boolean algebra B_n: subsets of {0,…,n−1} of cardinality i.

def BooleanUpDown.up {n : ℕ} (i : ℕ) (v : Level n i → ℝ) : Level n (i + 1) → ℝ

The up operator Uᵢ: (up i v)(y) = ∑_{x ⊆ y, |x|=i} v(x).

def BooleanUpDown.down {n : ℕ} (i : ℕ) (w : Level n (i + 1) → ℝ) : Level n i → ℝ

The down operator D_{i+1}: (down i w)(x) = ∑_{y ⊇ x, |y|=i+1} w(y).

def BooleanUpDown.innerProd {α : Type u_1} [Fintype α] (f g : α → ℝ) : ℝ

Inner product on real-valued functions on a finite type.

theorem BooleanUpDown.innerProd_comm {α : Type u_1} [Fintype α] (f g : α → ℝ) : innerProd f g = innerProd g f

def BooleanUpDown.DU_form {n : ℕ} (i : ℕ) (v w : Level n i → ℝ) : ℝ

Bilinear form from DU coefficients: ∑_x ∑_z DU_coeff(x,z) · v(x) · w(z).

def BooleanUpDown.UD_form {n : ℕ} (i : ℕ) (v w : Level n i → ℝ) : ℝ

Bilinear form from UD coefficients: ∑_x ∑_z UD_coeff(x,z) · v(x) · w(z).

def BooleanUpDown.upLM {n : ℕ} (i : ℕ) : (Level n i → ℝ) →ₗ[ℝ] Level n (i + 1) → ℝ

The up operator as a linear map.

def BooleanUpDown.downLM {n : ℕ} (i : ℕ) : (Level n (i + 1) → ℝ) →ₗ[ℝ] Level n i → ℝ

The down operator as a linear map.

def BooleanUpDown.upDownLM {n : ℕ} (i : ℕ) : (Level n (i + 1) → ℝ) →ₗ[ℝ] Level n (i + 1) → ℝ

The composition up ∘ down as a linear endomorphism on level i+1.

theorem BooleanUpDown.adjointness {n : ℕ} (i : ℕ) (v : Level n i → ℝ) (w : Level n (i + 1) → ℝ) : innerProd (up i v) w = innerProd v (down i w)

Adjointness: ⟨up v, w⟩ = ⟨v, down w⟩.

theorem BooleanUpDown.level_filter_card_eq_DU {n : ℕ} (i : ℕ) (x z : Level n i) : {y : Level n (i + 1) | ↑x ⊆ ↑y ∧ ↑z ⊆ ↑y}.card = BooleanCommutator.DU_coeff i ↑x ↑z

theorem BooleanUpDown.down_up_apply {n : ℕ} (i : ℕ) (v : Level n i → ℝ) (x : Level n i) : down i (up i v) x = ∑ z : Level n i, ↑(BooleanCommutator.DU_coeff i ↑x ↑z) * v z

theorem BooleanUpDown.level_filter_card_eq_UD {n : ℕ} (k : ℕ) (x z : Level n (k + 1)) : {w : Level n k | ↑w ⊆ ↑x ∧ ↑w ⊆ ↑z}.card = BooleanCommutator.UD_coeff (k + 1) ↑x ↑z

theorem BooleanUpDown.up_down_apply {n : ℕ} (k : ℕ) (v : Level n (k + 1) → ℝ) (x : Level n (k + 1)) : up k (down k v) x = ∑ z : Level n (k + 1), ↑(BooleanCommutator.UD_coeff (k + 1) ↑x ↑z) * v z

theorem BooleanUpDown.DU_form_eq_inner_up {n : ℕ} (i : ℕ) (v : Level n i → ℝ) : DU_form i v v = innerProd (up i v) (up i v)

DU_form(v,v) = ⟨up v, up v⟩, the squared norm of the up image.

theorem BooleanUpDown.DU_form_nonneg {n : ℕ} (i : ℕ) (v : Level n i → ℝ) : 0 ≤ DU_form i v v

theorem BooleanUpDown.UD_form_succ_eq_inner_down {n : ℕ} (k : ℕ) (v : Level n (k + 1) → ℝ) : UD_form (k + 1) v v = innerProd (down k v) (down k v)

UD_form at level k+1 equals ⟨down k v, down k v⟩, via adjointness.

theorem BooleanUpDown.UD_form_nonneg {n : ℕ} (i : ℕ) (v : Level n i → ℝ) : 0 ≤ UD_form i v v

theorem BooleanUpDown.DU_minus_UD {n : ℕ} (i : ℕ) (v : Level n i → ℝ) (hi : i ≤ n) : DU_form i v v - UD_form i v v = (↑n - 2 * ↑i) * ∑ x : Level n i, v x * v x

Lemma 4.6 (bilinear form version). DU_form(v,v) − UD_form(v,v) = (n − 2i) · ∑_x v(x)².

theorem BooleanUpDown.up_ker_trivial {n : ℕ} (i : ℕ) (hi : 2 * i < n) (v : Level n i → ℝ) (hv : up i v = 0) : v = 0

theorem BooleanUpDown.up_injective {n : ℕ} (i : ℕ) (hi : 2 * i < n) : Function.Injective (up i)

Theorem 4.7 (injectivity). When 2i < n, the up operator Uᵢ is injective.

theorem BooleanUpDown.updown_ker_trivial {n : ℕ} (i : ℕ) (hi : n ≤ 2 * i) (w : Level n (i + 1) → ℝ) (hw : up i (down i w) = 0) : w = 0

theorem BooleanUpDown.up_surjective {n : ℕ} (i : ℕ) (hi : n ≤ 2 * i) : Function.Surjective (up i)

Theorem 4.7 (surjectivity). When n ≤ 2i, the up operator Uᵢ is surjective.