LabelCoupling.lean`

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TalagrandDiscreteConvexity.labelLaw line 18
Source documentation
One coordinate receives label zero with the residual mass, and each of the L row labels with mass p. This does not assert independence of the rows.
```
def labelLaw (L : ℕ) (p : ℝ) (hp : 0 ≤ p) (hLp : (L : ℝ) * p ≤ 1) :
    FiniteLaw (Fin (L + 1)) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.FiniteLaw
theorem OAI.TalagrandDiscreteConvexity.labelLaw_weight_zero line 31
theorem OAI.TalagrandDiscreteConvexity.labelLaw_weight_succ line 36
theorem OAI.TalagrandDiscreteConvexity.labelLaw_prob_zero line 41
theorem OAI.TalagrandDiscreteConvexity.labelLaw_prob_succ line 52
theorem OAI.TalagrandDiscreteConvexity.labelLaw_prob_nonzero line 63
def OAI.TalagrandDiscreteConvexity.labelSamples line 72
Source documentation
Independent coordinate labels; the row membership events may be dependent.
```
def labelSamples (L : ℕ) (p : ℝ) (hp : 0 ≤ p) (hLp : (L : ℝ) * p ≤ 1) :
    FiniteLaw (α → Fin (L + 1)) :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.FiniteLaw
def OAI.TalagrandDiscreteConvexity.labelRow line 77
Source documentation
Row j contains exactly the coordinates labeled by its successor label.
```
def labelRow {L : ℕ} (ω : α → Fin (L + 1)) (j : Fin L) : Finset α := by
…
```
theorem OAI.TalagrandDiscreteConvexity.mem_labelRow line 82
theorem OAI.TalagrandDiscreteConvexity.labelUnion_eq_cubeSet_nonzero line 87
theorem OAI.TalagrandDiscreteConvexity.labelRow_prob_eq_mass line 100
Source documentation
Every row has the full Bernoulli law, proved from independent coordinates.
```
theorem labelRow_prob_eq_mass (L : ℕ) (p : ℝ) (hp : 0 ≤ p)
    (hLp : (L : ℝ) * p ≤ 1) (j : Fin L) (s : Finset α) :
    (labelSamples L p hp hLp).prob (fun ω => labelRow ω j = s) =
      bernoulliMass p s := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.labelSamples, OAI.TalagrandDiscreteConvexity.labelRow, OAI.TalagrandDiscreteConvexity.bernoulliMass
theorem OAI.TalagrandDiscreteConvexity.labelRow_prob_mem_family line 112
theorem OAI.TalagrandDiscreteConvexity.labelUnion_prob_eq_mass line 125
Source documentation
The row union has the full Bernoulli law at the amplified density L * p.
```
theorem labelUnion_prob_eq_mass (L : ℕ) (p : ℝ) (hp : 0 ≤ p)
    (hLp : (L : ℝ) * p ≤ 1) (s : Finset α) :
    (labelSamples L p hp hLp).prob (fun ω => unionTuple (labelRow ω) = s) =
      bernoulliMass ((L : ℝ) * p) s := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.labelSamples, OAI.TalagrandDiscreteConvexity.unionTuple, OAI.TalagrandDiscreteConvexity.labelRow, OAI.TalagrandDiscreteConvexity.bernoulliMass
theorem OAI.TalagrandDiscreteConvexity.labelUnion_prob_mem_family line 137
theorem OAI.TalagrandDiscreteConvexity.familyMeasure_unionFamily_label_lower line 151
Source documentation
Dependent rows give the density bound using only a union bound on failures. The law of the rows and of their union is supplied by the explicit label coupling.
```
theorem familyMeasure_unionFamily_label_lower (L : ℕ) (p : ℝ) (hp : 0 ≤ p)
    (hLp : (L : ℝ) * p ≤ 1) (D : Family α) :
    1 - (L : ℝ) * (1 - familyMeasure p D) ≤
      familyMeasure ((L : ℝ) * p) (unionFamily L D) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.familyMeasure, OAI.TalagrandDiscreteConvexity.unionFamily