Prove2Me

Nonzero-row count γ(I,J)\gamma(I,J)

Definition
DiscreteConvex_MixedMatrices_GammaFun

by Shuze Chen · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdiscrete-convex-analysis

γ(I,J)=∣{i∈I∣∃j∈J, Tij≠0}∣\gamma(I,J) = |\{i \in I \mid \exists j \in J,\ T_{ij} \ne 0\}|: the number of nonzero rows of the submatrix T[I,J]T[I,J].

(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.357.)

Definition code
import Mathlib

/-!
Murota, *Discrete Convex Analysis*, SIAM 2003, p.357: the function γ counting the nonzero rows of
a submatrix of `T`, in `DiscreteConvex.MixedMatrices`.
-/

namespace DiscreteConvex.MixedMatrices

open Classical in
/-- `γ(I,J) = |{i ∈ I | ∃ j ∈ J, Tᵢⱼ ≠ 0}|`: the number of nonzero rows of the submatrix
`T[I,J]`. -/
noncomputable def GammaFun {R C F : Type*} [Zero F] (T : Matrix R C F) (I : Finset R)
    (J : Finset C) : ℕ :=
  (I.filter (fun i => ∃ j ∈ J, T i j ≠ 0)).card

end DiscreteConvex.MixedMatrices
Source
Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.357

View graph