SignedArrays.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Signed arrays force weight on every exceptional set

The arrays have one common set of rows. Each column in S receives the Bernoulli product mass minus the product of the alternating corrections. All-zero columns in S have zero signed mass. This gives pointwise vanishing for exceptional sets, without any nonnegativity assumption on these masses. Expanding the column products and summing independently over the rows gives the exact signed coefficient identity.

def OAI.TalagrandDiscreteConvexity.signedArrayMass line 27
theorem OAI.TalagrandDiscreteConvexity.columnKernel_eq_rowKernel line 34
Source documentation
Choosing the correction columns factors into the same coefficient kernel in every row.
```
theorem columnKernel_eq_rowKernel (q : ℝ) {k : ℕ} (U : Finset V)
    (X : Fin k → V → Bool) :
    (∏ i, if i ∈ U then ∏ j, correction q (X j i)
      else ∏ j, bitWeight q (X j i)) =
      ∏ j, rowKernel q U (X j) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.correction, OAI.TalagrandDiscreteConvexity.bitWeight, OAI.TalagrandDiscreteConvexity.rowKernel
theorem OAI.TalagrandDiscreteConvexity.signed_array_identity line 47
Source documentation
The finite product expansion, followed by exact row factorization. It is valid for every real q and every real-valued row function.
```
theorem signed_array_identity (q : ℝ) (k : ℕ)
    (f : (V → Bool) → ℝ) (S : Finset V) :
    (∑ X : Fin k → V → Bool, (∏ j, f (X j)) * signedArrayMass q S X) =
      ∑ U ∈ S.powerset, (-1 : ℝ) ^ U.card * b q f U ^ k := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.signedArrayMass, OAI.TalagrandDiscreteConvexity.b
theorem OAI.TalagrandDiscreteConvexity.signedArrayMass_eq_zero_of_zero_column line 78
Source documentation
An all-zero column in S cancels exactly; the masses may be signed.
```
theorem signedArrayMass_eq_zero_of_zero_column (q : ℝ) {k : ℕ}
    {S : Finset V} {X : Fin k → V → Bool} {i : V}
    (hi : i ∈ S) (hzero : ∀ j, X j i = false) :
    signedArrayMass q S X = 0 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.signedArrayMass
theorem OAI.TalagrandDiscreteConvexity.exceptional_signed_summand_eq_zero line 87
Source documentation
On an exceptional set, either one row leaves the family or some column of S is all zero. In either case the signed summand vanishes.
```
theorem exceptional_signed_summand_eq_zero (q : ℝ) {k : ℕ}
    {D : Family V} {S : Finset V} (hS : S ∈ exceptional k D)
    (X : Fin k → V → Bool) :
    (∏ j, familyIndicator D (X j)) * signedArrayMass q S X = 0 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.exceptional, OAI.TalagrandDiscreteConvexity.familyIndicator, OAI.TalagrandDiscreteConvexity.signedArrayMass
theorem OAI.TalagrandDiscreteConvexity.exceptional_signed_sum_eq_zero line 108
Source documentation
The exact vanishing signed expansion on an exceptional set.
```
theorem exceptional_signed_sum_eq_zero (q : ℝ) {k : ℕ}
    {D : Family V} {S : Finset V} (hS : S ∈ exceptional k D) :
    (∑ U ∈ S.powerset, (-1 : ℝ) ^ U.card * b q (familyIndicator D) U ^ k) = 0 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.exceptional, OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.familyIndicator
theorem OAI.TalagrandDiscreteConvexity.exceptional_signed_identity line 116
theorem OAI.TalagrandDiscreteConvexity.exceptional_weight_lower_bound line 122
Source documentation
The actual exceptional-weight bound, at the original family density.
```
theorem exceptional_weight_lower_bound (q : ℝ)
    {D : Family V} (hD : (1 / 2 : ℝ) ≤ familyMeasure q D)
    {S : Finset V} (hS : S ∈ exceptional 32 D) :
    (1 / 2 : ℝ) ^ 32 ≤
      ∑ U ∈ S.powerset.erase ∅, w q (familyIndicator D) U ^ 16 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.familyMeasure, OAI.TalagrandDiscreteConvexity.exceptional, OAI.TalagrandDiscreteConvexity.w, OAI.TalagrandDiscreteConvexity.familyIndicator
theorem OAI.TalagrandDiscreteConvexity.exceptional_weight_lower_bound_filter line 132
Source documentation
The filter form used to combine the exceptional bound with weight bins.
```
theorem exceptional_weight_lower_bound_filter (q : ℝ)
    {D : Family V} (hD : (1 / 2 : ℝ) ≤ familyMeasure q D)
    {S : Finset V} (hS : S ∈ exceptional 32 D) :
    (1 / 2 : ℝ) ^ 32 ≤
      ∑ U ∈ S.powerset.filter (fun U => U ≠ ∅), w q (familyIndicator D) U ^ 16 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.familyMeasure, OAI.TalagrandDiscreteConvexity.exceptional, OAI.TalagrandDiscreteConvexity.w, OAI.TalagrandDiscreteConvexity.familyIndicator