CoveringResidualProbability.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact survival probability of a tuple of distinct edges

The sampling coordinates are ordered pairs of edges, not their unions. Every ordered pair of positions contributes a distinct coordinate, including each diagonal position. The product Bernoulli law therefore assigns exactly (1 - p) ^ (m * m) to the event that all these coordinates are absent.

theorem OAI.TalagrandDiscreteConvexity.Covering.orderedPairMap_injective line 18

Source documentation

Applying an injection in both coordinates preserves ordered pairs.

theorem orderedPairMap_injective {I E : Type*} {e : I → E}
    (he : Function.Injective e) :
    Function.Injective (fun ij : I × I => (e ij.1, e ij.2)) := by
…

theorem OAI.TalagrandDiscreteConvexity.Covering.tuplePairs_card line 31
Source documentation
The tuple uses all m * m ordered pair coordinates, including the diagonal.
```
theorem tuplePairs_card {H : Family X} {m : ℕ} (f : EdgeTuple H m) :
    (tuplePairs f).card = m * m := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.EdgeTuple, OAI.TalagrandDiscreteConvexity.Covering.tuplePairs
theorem OAI.TalagrandDiscreteConvexity.Covering.diagonal_mem_tuplePairs line 39
Source documentation
A diagonal edge pair is one of the sampled coordinates used by the tuple.
```
theorem diagonal_mem_tuplePairs {H : Family X} {m : ℕ}
    (f : EdgeTuple H m) (i : Fin m) : (f.val i, f.val i) ∈ tuplePairs f := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.EdgeTuple, OAI.TalagrandDiscreteConvexity.Covering.tuplePairs
theorem OAI.TalagrandDiscreteConvexity.Covering.disjoint_tuplePairs_iff line 44
Source documentation
Avoiding the pair set means that none of the ordered tuple pairs was sampled.
```
theorem disjoint_tuplePairs_iff {H : Family X} {m : ℕ}
    (f : EdgeTuple H m) (sample : Sample H) :
    Disjoint sample (tuplePairs f) ↔ ∀ i j, (f.val i, f.val j) ∉ sample := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.EdgeTuple, OAI.TalagrandDiscreteConvexity.Covering.Sample, OAI.TalagrandDiscreteConvexity.Covering.tuplePairs
theorem OAI.TalagrandDiscreteConvexity.Covering.tuple_survival_probability line 57
Source documentation
Exact residual probability under the actual finite product Bernoulli law.
```
theorem tuple_survival_probability {H : Family X} {m : ℕ}
    (f : EdgeTuple H m) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    (bernoulliLaw (α := ↥H × ↥H) p hp0 hp1).prob
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.Covering.EdgeTuple, OAI.TalagrandDiscreteConvexity.bernoulliLaw