OAI/Combinatorics/DiscreteConvexity/ColumnExpansion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A product expansion on a prescribed set of coordinates

Only coordinates in S contribute correction terms. Expanding their product therefore gives a sum indexed by S.powerset, with the factors outside S left unchanged.

  1. theorem OAI.TalagrandDiscreteConvexity.prod_ite_split line 20
  2. theorem OAI.TalagrandDiscreteConvexity.prod_sub_ite_eq_sum_powerset line 38

    Source documentation

    Expand a product with correction terms restricted to S.

    theorem prod_sub_ite_eq_sum_powerset (S : Finset V) (P C : V → ℝ) :
    (∏ i, (P i - if i ∈ S then C i else 0)) =
      ∑ U ∈ S.powerset, (-1 : ℝ) ^ U.card * ∏ i, if i ∈ U then C i else P i := by
…