UnionTuples.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Grouping and repeating union tuples

Grouping a * b entries into a rows of length b preserves exactly the possible unions. Repetition is allowed throughout, as in the definition of the exceptional family. No positivity assumption is needed for grouping.

def OAI.TalagrandDiscreteConvexity.flattenTuple line 19
Source documentation
Flatten a rectangular array using the standard finite product equivalence.
```
def flattenTuple {a b : ℕ} (f : Fin a → Fin b → Finset α) :
    Fin (a * b) → Finset α :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b
theorem OAI.TalagrandDiscreteConvexity.unionTuple_flatten line 24
theorem OAI.TalagrandDiscreteConvexity.unionTuple_rows line 36
theorem OAI.TalagrandDiscreteConvexity.unionFamily_mul line 45
Source documentation
Iterated unions are exactly unions of the product number of entries.
```
theorem unionFamily_mul (a b : ℕ) (D : Family α) :
    unionFamily a (unionFamily b D) = unionFamily (a * b) D := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.unionFamily
theorem OAI.TalagrandDiscreteConvexity.exceptional_unionFamily line 76
Source documentation
Grouping tuples preserves failure of containment in every possible union.
```
theorem exceptional_unionFamily (a b : ℕ) (D : Family α) :
    exceptional a (unionFamily b D) = exceptional (a * b) D := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.exceptional, OAI.TalagrandDiscreteConvexity.unionFamily
def OAI.TalagrandDiscreteConvexity.repeatTuple line 82
Source documentation
Repeat the same row tuple a times.
```
def repeatTuple (a : ℕ) {b : ℕ} (f : Fin b → Finset α) :
    Fin (a * b) → Finset α :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b
theorem OAI.TalagrandDiscreteConvexity.repeatTuple_mem line 87
theorem OAI.TalagrandDiscreteConvexity.unionTuple_repeat line 92
theorem OAI.TalagrandDiscreteConvexity.exists_unionTuple_mul_eq_univ line 103
theorem OAI.TalagrandDiscreteConvexity.exceptional_mul_eq_empty_of_full_union line 110

theorem OAI.TalagrandDiscreteConvexity.exists_unionTuple_thirtytwo_mul_eq_univ line 117

Source documentation

The repetition used in the full-union branch of the density argument.

theorem exists_unionTuple_thirtytwo_mul_eq_univ {L : ℕ} {D : Family α}
    (f : Fin L → Finset α) (hf : ∀ j, f j ∈ D)
    (hfull : unionTuple f = Finset.univ) :
    ∃ g : Fin (32 * L) → Finset α, (∀ j, g j ∈ D) ∧ unionTuple g = Finset.univ :=
…

Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.unionTuple