Model.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite families, containment covers, and exceptional sets

All families are ordinary finite sets: repeated generators carry no extra cost. In contrast, the members of a union tuple may repeat. The exceptional family uses containment in a union, without any monotonicity assumption on the input.

abbrev OAI.TalagrandDiscreteConvexity.Family line 20
Also declared: ComparatorChallenges/TalagrandDiscreteConvexity.lean:12 (same declaration text).
def OAI.TalagrandDiscreteConvexity.bernoulliMass line 27
Source documentation
The mass of a subset under independent Bernoulli coordinates.
Also declared: ComparatorChallenges/TalagrandDiscreteConvexity.lean:19 (same declaration text).
```
def bernoulliMass (p : ℝ) (s : Finset α) : ℝ :=
…
```
def OAI.TalagrandDiscreteConvexity.familyMeasure line 31
Source documentation
The Bernoulli measure of an arbitrary finite family.
Also declared: ComparatorChallenges/TalagrandDiscreteConvexity.lean:23 (same declaration text).
```
def familyMeasure (p : ℝ) (D : Family α) : ℝ :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.cost line 35
Source documentation
Cost at the specified density, counting each generator once.
Also declared: ComparatorChallenges/TalagrandDiscreteConvexity.lean:27 (same declaration text).
```
def cost (p : ℝ) (G : Family α) : ℝ := ∑ I ∈ G, p ^ I.card
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.Covers line 38
Source documentation
A cover supplies a contained generator for every target set.
Also declared: ComparatorChallenges/TalagrandDiscreteConvexity.lean:30 (same declaration text).
```
def Covers (G A : Family α) : Prop := ∀ S ∈ A, ∃ I ∈ G, I ⊆ S
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.Small line 41
Source documentation
Smallness is witnessed by an actual containment cover of cost at most one half.
Also declared: ComparatorChallenges/TalagrandDiscreteConvexity.lean:33 (same declaration text).
```
def Small (p : ℝ) (A : Family α) : Prop :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.unionTuple line 45
Source documentation
A union of exactly k entries; repetitions are allowed.
Also declared: ComparatorChallenges/TalagrandDiscreteConvexity.lean:37 (same declaration text).
```
def unionTuple {k : ℕ} (f : Fin k → Finset α) : Finset α :=
…
```
def OAI.TalagrandDiscreteConvexity.unionFamily line 49
Source documentation
All unions of k members of a family.
```
def unionFamily (k : ℕ) (D : Family α) : Family α := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.exceptional line 55
Source documentation
Sets contained in no union of k members of D.
Also declared: ComparatorChallenges/TalagrandDiscreteConvexity.lean:41 (same declaration text).
```
def exceptional (k : ℕ) (D : Family α) : Family α := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.cubeSet line 61
Source documentation
The subset represented by a Boolean coordinate vector.
```
def cubeSet (x : α → Bool) : Finset α :=
…
```
def OAI.TalagrandDiscreteConvexity.familyIndicator line 65
Source documentation
The indicator of a family on the Boolean cube.
```
def familyIndicator (D : Family α) (x : α → Bool) : ℝ :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family