ExceptionalWeightBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An exceptional-weight lower bound from a signed identity

Separating the empty subset in a vanishing signed sum bounds its weight by the total unsigned weight of the nonempty subsets. This scalar argument does not depend on how the weights or their signed identity were constructed.

theorem OAI.TalagrandDiscreteConvexity.exceptional_lower_bound_of_signed_sum line 23

Source documentation

A vanishing signed 32nd-power sum and an empty-subset value at least one half force a lower bound on the sum of the nonempty squared weights.

theorem exceptional_lower_bound_of_signed_sum {V : Type*} [DecidableEq V]
    (S : Finset V) (b : Finset V → ℝ)
    (hsum : ∑ U ∈ S.powerset, (-1 : ℝ) ^ U.card * b U ^ 32 = 0)
    (hb0 : (1 / 2 : ℝ) ≤ b ∅) :
    (1 / 2 : ℝ) ^ 32 ≤ ∑ U ∈ S.powerset.erase ∅, (b U ^ 2) ^ 16 := by
…

Mentions: OAI.TalagrandDiscreteConvexity.b