CoveringResidualCost.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Expected cost of the actual residual generators

Repeated unions are first counted with multiplicity. Each injective tuple avoids exactly its distinct ordered-pair indices under the product Bernoulli law. Finite linearity then separates this common survival probability from the weighted tuple sum.

theorem OAI.TalagrandDiscreteConvexity.Covering.expectation_residualFamily_le line 25
Source documentation
The expected residual cost is bounded by the actual weighted tuple sum times the exact probability of avoiding all ordered pairs of one tuple.
```
theorem expectation_residualFamily_le (H : Family V) (rho : ℝ)
    (hrho : 0 ≤ rho) (m : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    (bernoulliLaw (α := PairIndex H) p hp0 hp1).expectation
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.bernoulliLaw, OAI.TalagrandDiscreteConvexity.Covering.PairIndex

theorem OAI.TalagrandDiscreteConvexity.Covering.expectation_residualFamily_le_extension line 63

Source documentation

Applying the proved tuple recurrence bounds the expected residual cost using only the actual extension estimate for the edge family.

theorem expectation_residualFamily_le_extension (H : Family V)
    {rho T : ℝ} {r m : ℕ} (hrho : 0 ≤ rho) (hT : 0 ≤ T)
    (uniform : ∀ e ∈ H, (e : Finset V).card = r)
    (extension : ∀ B : Finset V,
      (∑ e ∈ H, rho ^ (e \ B).card) ≤ T * (1 + (B.card : ℝ)) ^ r)
    (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    (bernoulliLaw (α := PairIndex H) p hp0 hp1).expectation
…

Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.bernoulliLaw, OAI.TalagrandDiscreteConvexity.Covering.PairIndex

theorem OAI.TalagrandDiscreteConvexity.Covering.expectation_residualFamily_le_inv_pow line 78