MandatoryCoupling.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The mandatory-row coupling at high density

The auxiliary inclusion probability is valid throughout the closed high-density regime 1 ≤ L * p, including equality, when it is zero.

At each coordinate the mandatory label is uniform and independent of the independent Bernoulli marks. Taking a product of these laws across coordinates gives each row its full Bernoulli subset law. The union is full in every outcome; only marginal probabilities are used to obtain simultaneous family membership.

def OAI.TalagrandDiscreteConvexity.mandatoryParameter line 27
Source documentation
The extra inclusion probability after the uniformly chosen mandatory row.
```
def mandatoryParameter (L : ℕ) (p : ℝ) : ℝ :=
…
```
theorem OAI.TalagrandDiscreteConvexity.mandatoryParameter_den_pos line 30
theorem OAI.TalagrandDiscreteConvexity.mandatoryParameter_nonneg line 36
theorem OAI.TalagrandDiscreteConvexity.mandatoryParameter_lt_one line 45
theorem OAI.TalagrandDiscreteConvexity.mandatoryParameter_marginal line 50
theorem OAI.TalagrandDiscreteConvexity.mandatoryParameter_boundary line 56
abbrev OAI.TalagrandDiscreteConvexity.MandatoryColumn line 67
Source documentation
A coordinate chooses one compulsory row, together with independent marks. The mark in the compulsory row may be sampled and then ignored.
```
abbrev MandatoryColumn (L : ℕ) := Fin L × (Fin L → Bool)
```
def OAI.TalagrandDiscreteConvexity.mandatoryBit line 69
theorem OAI.TalagrandDiscreteConvexity.mandatoryBit_mandatory line 72
theorem OAI.TalagrandDiscreteConvexity.mandatory_prob_prod_or line 76
def OAI.TalagrandDiscreteConvexity.mandatoryColumnLaw line 88
Source documentation
Uniform mandatory label, independent of all the extra row marks.
```
def mandatoryColumnLaw {L : ℕ} (hL : 1 < L) (p : ℝ) (hp : p < 1)
    (hLp : 1 ≤ (L : ℝ) * p) : FiniteLaw (MandatoryColumn L) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.MandatoryColumn
theorem OAI.TalagrandDiscreteConvexity.mandatoryColumnLaw_marginal line 95
def OAI.TalagrandDiscreteConvexity.mandatoryRows line 132
Source documentation
Read the sets in all rows of a coordinate array.
```
def mandatoryRows {L : ℕ} (ω : α → MandatoryColumn L) (j : Fin L) : Finset α :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.MandatoryColumn
def OAI.TalagrandDiscreteConvexity.mandatoryArrayLaw line 136
Source documentation
The coordinate choices are independent; the rows need not be independent.
```
def mandatoryArrayLaw {L : ℕ} (hL : 1 < L) (p : ℝ) (hp : p < 1)
    (hLp : 1 ≤ (L : ℝ) * p) : FiniteLaw (α → MandatoryColumn L) :=
…
```
Mentions: OAI.TalagrandDiscreteConvexity.FiniteLaw, OAI.TalagrandDiscreteConvexity.MandatoryColumn
theorem OAI.TalagrandDiscreteConvexity.mandatoryRows_prob_eq_mass line 141
Source documentation
Every atom of each row has its exact Bernoulli subset mass.
```
theorem mandatoryRows_prob_eq_mass {L : ℕ} (hL : 1 < L) (p : ℝ)
    (hp : p < 1) (hLp : 1 ≤ (L : ℝ) * p) (j : Fin L) (s : Finset α) :
    (mandatoryArrayLaw (α := α) hL p hp hLp).prob
…
```
Mentions: OAI.TalagrandDiscreteConvexity.mandatoryArrayLaw
theorem OAI.TalagrandDiscreteConvexity.mandatoryRows_prob_mem_family line 149
Source documentation
The row distribution agrees on arbitrary, potentially nonmonotone families.
```
theorem mandatoryRows_prob_mem_family {L : ℕ} (hL : 1 < L) (p : ℝ)
    (hp : p < 1) (hLp : 1 ≤ (L : ℝ) * p) (j : Fin L) (D : Family α) :
    (mandatoryArrayLaw (α := α) hL p hp hLp).prob
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.mandatoryArrayLaw
theorem OAI.TalagrandDiscreteConvexity.mandatoryRows_union line 157
Source documentation
The selected mandatory row contains each coordinate in every outcome.
```
theorem mandatoryRows_union {L : ℕ} (ω : α → MandatoryColumn L) :
    unionTuple (mandatoryRows ω) = Finset.univ := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.MandatoryColumn, OAI.TalagrandDiscreteConvexity.unionTuple, OAI.TalagrandDiscreteConvexity.mandatoryRows
theorem OAI.TalagrandDiscreteConvexity.exists_mandatory_cover line 167
Source documentation
Marginal success probabilities and the union bound give a covering tuple. There is no independence assumption between the rows.
```
theorem exists_mandatory_cover {L : ℕ} (hL : 1 < L) (p : ℝ)
    (hp : p < 1) (hLp : 1 ≤ (L : ℝ) * p) (D : Family α)
    (hbudget : (L : ℝ) * (1 - familyMeasure p D) < 1) :
    ∃ rows : Fin L → Finset α,
      (∀ j, rows j ∈ D) ∧ unionTuple rows = Finset.univ := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family, OAI.TalagrandDiscreteConvexity.familyMeasure, OAI.TalagrandDiscreteConvexity.unionTuple