CoveringBasic.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Finite objects in the elementary covering argument

Sampling is indexed by ordered pairs of edges, including diagonal pairs. Different pairs remain different indices even if their unions coincide. Residual generators are indexed by injective ordered tuples.

def OAI.TalagrandDiscreteConvexity.Covering.EdgeTuple line 22
Source documentation
An ordered tuple of distinct members of a finite edge family.
```
def EdgeTuple (H : Family V) (t : ℕ) :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
instance OAI.TalagrandDiscreteConvexity.Covering.edgeTupleFintype line 25
abbrev OAI.TalagrandDiscreteConvexity.Covering.PairIndex line 31
Source documentation
All independent ordered-pair sampling indices.
```
abbrev PairIndex (H : Family V) := ↥H × ↥H
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
abbrev OAI.TalagrandDiscreteConvexity.Covering.Sample line 34
Source documentation
A sampling outcome specifies precisely the pairs selected.
```
abbrev Sample (H : Family V) := Finset (PairIndex H)
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.PairIndex
def OAI.TalagrandDiscreteConvexity.Covering.tupleUnion line 36
def OAI.TalagrandDiscreteConvexity.Covering.tuplePairs line 39
theorem OAI.TalagrandDiscreteConvexity.Covering.mem_tupleUnion line 44
theorem OAI.TalagrandDiscreteConvexity.Covering.mem_tuplePairs line 49
def OAI.TalagrandDiscreteConvexity.Covering.weightedDegree line 56
Source documentation
The weighted number of edges containing a prescribed vertex set.
```
noncomputable def weightedDegree (H : Family V) (rho : ℝ) (r : ℕ)
    (I : Finset V) : ℝ := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.Covering.regularFamily line 62
Source documentation
Edges avoiding all prescribed initial generators.
```
noncomputable def regularFamily (H C0 : Family V) : Family V := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
theorem OAI.TalagrandDiscreteConvexity.Covering.mem_regularFamily line 66
theorem OAI.TalagrandDiscreteConvexity.Covering.regularFamily_subset line 71
def OAI.TalagrandDiscreteConvexity.Covering.initialFamily line 80
Source documentation
The high weighted-degree sets used as the initial generators.
```
noncomputable def initialFamily (H : Family V) (rho : ℝ) (r : ℕ)
    (T : ℝ) : Family V := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.Covering.regularEdges line 86
Source documentation
The regular edges for the actual high-degree initial family.
```
noncomputable def regularEdges (H : Family V) (rho : ℝ) (r : ℕ)
    (T : ℝ) : Family V := regularFamily H (initialFamily H rho r T)
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.regularFamily, OAI.TalagrandDiscreteConvexity.Covering.initialFamily
def OAI.TalagrandDiscreteConvexity.Covering.denseFamily line 90
Source documentation
Sets containing at least m distinct edges of the original family.
```
noncomputable def denseFamily (H : Family V) (m : ℕ) : Family V := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
theorem OAI.TalagrandDiscreteConvexity.Covering.mem_initialFamily line 94
theorem OAI.TalagrandDiscreteConvexity.Covering.mem_regularEdges line 100
theorem OAI.TalagrandDiscreteConvexity.Covering.mem_denseFamily line 106
theorem OAI.TalagrandDiscreteConvexity.Covering.regularEdges_subset line 111