ThresholdBounds.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Elementary bounds for the actual expectation thresholds

When the empty set is absent from the family, zero is feasible for both thresholds. Their feasible sets are bounded by one, and indicator covers give the integral-to-fractional comparison.

theorem OAI.TalagrandThreshold.integralFeasible_subset_Icc line 21
theorem OAI.TalagrandThreshold.fractionalFeasible_subset_Icc line 26
theorem OAI.TalagrandThreshold.integralFeasible_bddAbove line 31
theorem OAI.TalagrandThreshold.fractionalFeasible_bddAbove line 35
theorem OAI.TalagrandThreshold.zero_mem_integralFeasible line 39
theorem OAI.TalagrandThreshold.zero_mem_fractionalFeasible line 43
theorem OAI.TalagrandThreshold.integralFeasible_nonempty line 48
theorem OAI.TalagrandThreshold.fractionalFeasible_nonempty line 52
theorem OAI.TalagrandThreshold.integralFeasible_mono line 58
Source documentation
Integral feasibility is preserved by lowering the nonnegative density.
```
theorem integralFeasible_mono {F : Family α} {p r : ℝ}
    (hr : r ∈ integralFeasible F) (hp : 0 ≤ p) (hpr : p ≤ r) :
    p ∈ integralFeasible F :=
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.integralFeasible
theorem OAI.TalagrandThreshold.fractionalFeasible_mono line 65
Source documentation
Fractional feasibility is preserved by lowering the nonnegative density.
```
theorem fractionalFeasible_mono {F : Family α} {p r : ℝ}
    (hr : r ∈ fractionalFeasible F) (hp : 0 ≤ p) (hpr : p ≤ r) :
    p ∈ fractionalFeasible F :=
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.fractionalFeasible
theorem OAI.TalagrandThreshold.integralFeasible_subset_fractionalFeasible line 70
theorem OAI.TalagrandThreshold.le_q_of_mem line 75
theorem OAI.TalagrandThreshold.le_qf_of_mem line 80
theorem OAI.TalagrandThreshold.le_q_of_small line 85
theorem OAI.TalagrandThreshold.le_qf_of_fractionalSmall line 90
theorem OAI.TalagrandThreshold.q_nonneg line 95
theorem OAI.TalagrandThreshold.qf_nonneg line 98
theorem OAI.TalagrandThreshold.q_le_one line 102
theorem OAI.TalagrandThreshold.qf_le_one line 105
theorem OAI.TalagrandThreshold.q_le_qf line 108