ThresholdAttainment.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Attainment of the integral and fractional thresholds

There are finitely many integral covers, so integral feasibility is closed in the density interval. Fractional feasibility is a compact projection. The actual suprema therefore belong to their respective feasible sets as soon as those sets contain density zero.

theorem OAI.TalagrandThreshold.continuous_cost line 22
theorem OAI.TalagrandThreshold.isClosed_small line 28
Source documentation
Smallness is a finite union of closed conditions, one per actual cover.
```
theorem isClosed_small (F : Family α) : IsClosed {p : ℝ | Small p F} := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Small
theorem OAI.TalagrandThreshold.isCompact_integralFeasible line 45
theorem OAI.TalagrandThreshold.q_mem_integralFeasible line 58
Source documentation
The integral supremum is an actual feasible density.
```
theorem q_mem_integralFeasible (F : Family α) (hF : ∅ ∉ F) :
    q F ∈ integralFeasible F := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.q, OAI.TalagrandThreshold.integralFeasible
theorem OAI.TalagrandThreshold.qf_mem_fractionalFeasible line 63
Source documentation
The fractional supremum is an actual feasible density.
```
theorem qf_mem_fractionalFeasible (F : Family α) (hF : ∅ ∉ F) :
    qf F ∈ fractionalFeasible F := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.fractionalFeasible
theorem OAI.TalagrandThreshold.small_q line 68
theorem OAI.TalagrandThreshold.fractionalSmall_qf line 71