CoveringSampledFamilies.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Deterministic covers from a pair-sampling outcome

Every sampling outcome gives a cover. The cost bounds count generators with multiplicity, indexed by ordered pairs or injective ordered tuples. No independence or probability estimate is needed for these pointwise statements.

def OAI.TalagrandDiscreteConvexity.Covering.pairUnion line 23
Source documentation
The generator produced by a sampled ordered pair.
```
def pairUnion {H : Family V} (p : PairIndex H) : Finset V := p.1.val ∪ p.2.val
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.PairIndex
def OAI.TalagrandDiscreteConvexity.Covering.sampledFamily line 26
Source documentation
Duplicate unions are identified in the family of sampled generators.
```
noncomputable def sampledFamily (H : Family V) (sample : Sample H) : Family V :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.Sample
def OAI.TalagrandDiscreteConvexity.Covering.residualFamily line 31
Source documentation
An injective tuple contributes a residual generator exactly when all of its ordered pair indices were avoided.
```
noncomputable def residualFamily (H : Family V) (m : ℕ) (sample : Sample H) :
    Family V := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.Sample
theorem OAI.TalagrandDiscreteConvexity.Covering.mem_sampledFamily line 37
theorem OAI.TalagrandDiscreteConvexity.Covering.mem_residualFamily line 42
theorem OAI.TalagrandDiscreteConvexity.Covering.cost_sampledFamily_le line 50
Source documentation
Counting each sampled ordered pair separately bounds the family cost.
```
theorem cost_sampledFamily_le (H : Family V) (sample : Sample H)
    {rho : ℝ} (hrho : 0 ≤ rho) :
    cost rho (sampledFamily H sample) ≤
      ∑ p ∈ sample, rho ^ (pairUnion p).card := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.Sample, OAI.TalagrandDiscreteConvexity.cost, OAI.TalagrandDiscreteConvexity.Covering.sampledFamily, OAI.TalagrandDiscreteConvexity.Covering.pairUnion
theorem OAI.TalagrandDiscreteConvexity.Covering.cost_residualFamily_le line 61
Source documentation
Counting each avoiding tuple separately bounds the residual cost. The indicator has the same argument order as the sampling law.
```
theorem cost_residualFamily_le (H : Family V) (m : ℕ) (sample : Sample H)
    {rho : ℝ} (hrho : 0 ≤ rho) :
    cost rho (residualFamily H m sample) ≤
      ∑ f : EdgeTuple H m,
        if Disjoint sample (tuplePairs f) then rho ^ (tupleUnion f).card else 0 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.Sample, OAI.TalagrandDiscreteConvexity.cost, OAI.TalagrandDiscreteConvexity.Covering.residualFamily, OAI.TalagrandDiscreteConvexity.Covering.EdgeTuple, OAI.TalagrandDiscreteConvexity.Covering.tuplePairs, OAI.TalagrandDiscreteConvexity.Covering.tupleUnion
theorem OAI.TalagrandDiscreteConvexity.Covering.exists_regular_tuple line 79
Source documentation
A large contained-edge family can be enumerated injectively inside the regular edges, provided the set avoids the initial generators.
```
theorem exists_regular_tuple {H C0 : Family V} {m : ℕ} {S : Finset V}
    (hm : m ≤ (H.filter (fun e => e ⊆ S)).card)
    (h0 : ¬∃ I ∈ C0, I ⊆ S) :
    ∃ f : EdgeTuple (regularFamily H C0) m, ∀ i, (f.val i).val ⊆ S := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.EdgeTuple, OAI.TalagrandDiscreteConvexity.Covering.regularFamily
theorem OAI.TalagrandDiscreteConvexity.Covering.covers_sampled_residual line 106
Source documentation
Every pair-sampling outcome covers each set containing sufficiently many original edges. This includes m = 0 and empty edge families.
```
theorem covers_sampled_residual [Fintype V] (H C0 : Family V) (m : ℕ)
    (sample : Sample (regularFamily H C0)) :
    Covers (C0 ∪ sampledFamily (regularFamily H C0) sample ∪
      residualFamily (regularFamily H C0) m sample) (denseFamily H m) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.Sample, OAI.TalagrandDiscreteConvexity.Covering.regularFamily, OAI.TalagrandDiscreteConvexity.Covers, OAI.TalagrandDiscreteConvexity.Covering.sampledFamily, OAI.TalagrandDiscreteConvexity.Covering.residualFamily, OAI.TalagrandDiscreteConvexity.Covering.denseFamily