ThresholdCompactness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness of the fractional feasible densities

The cover coefficients and the density range over closed unit intervals. The coverage inequalities and the polynomial cost bound cut out a closed subset of their compact product. Its projection is exactly the set of fractionally feasible densities, including when that set is empty.

theorem OAI.TalagrandThreshold.continuous_fracCost line 26
Source documentation
The fractional cost is jointly continuous in the density and coefficients.
```
theorem continuous_fracCost :
    Continuous (fun z : ℝ × (Finset α → ℝ) => fracCost z.1 z.2) := by
…
```
Mentions: OAI.TalagrandThreshold.fracCost
theorem OAI.TalagrandThreshold.isCompact_fractionalFeasible line 34
Source documentation
Fractional feasibility is the projection of the actual compact set of covers.
```
theorem isCompact_fractionalFeasible (F : Family α) :
    IsCompact (fractionalFeasible F) := by
…
```
Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.fractionalFeasible