Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Strong.Weighted.Condenser.Identity.Internal

Identity strong-condensation witnesses #

At every seed the ideal conditional law is the original source. The actual joint law agrees exactly, including the zero-division convention for an empty seed alphabet.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_id {X : Type u_1} {Seed : Type u_2} [Fintype X] [Fintype Seed] {K : ℕ} {ε : ℝ} (nonnegative : 0 ≤ ε) :
WeightedStrongSeededCondenser (fun (x : X) (x_1 : Seed) => x) K K ε