Set-family shadow corollaries

This file exposes thin numeric corollaries of the upstream Kruskal-Katona upper-shadow theorem in the notation used by the Harper proof.

theorem BooleanIsoperimetry.upperShadow_eq_upperShadowVal (N r t : ℕ) : upperShadow N r t = upperShadowVal N r t

The Shadow.lean numeric scaffold upperShadow and the relocated upstream upperShadowVal are definitionally equal.

theorem BooleanIsoperimetry.upperShadow_eq_card_upperLayerShadow {N r t : ℕ} (hr : 1 ≤ r) (ht : t ≤ N.choose r) : upperShadow N r t = (upperLayerShadow N r (layerInitSeg N r t)).card

Shadow.upperShadow form of the partial-layer identity.

theorem BooleanIsoperimetry.upperShadow_numeric_min {N r t : ℕ} (hr : 1 ≤ r) (ht : t ≤ N.choose r) {A : Finset (Cube N)} (hA : ∀ x ∈ A, Finset.card x = r) (hcard : A.card = t) : upperShadow N r t ≤ (upperLayerShadow N r A).card

Shadow.upperShadow form of the Kruskal–Katona numeric minimum.