CoveringPairCost.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The cost of sampled ordered pairs

The expectation is bounded by counting pair unions with multiplicity. Its deterministic bound uses the actual regularized edge family and the sharp 2^r extension estimate, rather than the coarser tuple-extension estimate.

theorem OAI.TalagrandDiscreteConvexity.Covering.regular_pair_weight_sum_le line 21
theorem OAI.TalagrandDiscreteConvexity.Covering.expectation_sampledFamily_le line 62
Source documentation
The actual independent pair sample has small expected generator cost. No identification of equal unions is made at the probability-index level.
```
theorem expectation_sampledFamily_le {H : Family V} {rho T p : ℝ} {r : ℕ}
    (hrho : 0 ≤ rho) (hT : 0 ≤ T) (hH : ∀ e ∈ H, e.card = r)
    (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    (bernoulliLaw (α := PairIndex (regularEdges H rho r T)) p hp0 hp1).expectation
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.bernoulliLaw, OAI.TalagrandDiscreteConvexity.Covering.PairIndex, OAI.TalagrandDiscreteConvexity.Covering.regularEdges