SelectorTruncationCompact.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Existence of the maximal admissible truncation

The condition that every heavy point belongs to A is a family of closed lower bounds on the cutoff, one for each point outside A. The excess is a continuous finite sum. Thus the admissible cutoffs form a closed subset of [0, 1], and a nonempty such set has a greatest element.

This existence argument does not use positivity or normalization of the weights, or sign assumptions on the parameters m and d.

theorem OAI.TalagrandThreshold.Selector.continuous_truncatedExcess line 26
Source documentation
Finite truncation gives a continuous excess as the cutoff varies.
```
theorem continuous_truncatedExcess (w : α → ℝ) (A : Finset α) (d : ℝ) :
    Continuous (fun u => truncatedExcess w A d u) := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.truncatedExcess
theorem OAI.TalagrandThreshold.Selector.isClosed_admissible line 34
Source documentation
The heavy-point inclusion and the excess test are closed conditions.
```
theorem isClosed_admissible (w : α → ℝ) (A : Finset α) (m d : ℝ) :
    IsClosed {u : ℝ | Admissible w A m d u} := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.Admissible
theorem OAI.TalagrandThreshold.Selector.isCompact_admissible line 59
Source documentation
Admissible cutoffs are compact because they are closed and lie in [0, 1].
```
theorem isCompact_admissible (w : α → ℝ) (A : Finset α) (m d : ℝ) :
    IsCompact {u : ℝ | Admissible w A m d u} := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.Admissible

theorem OAI.TalagrandThreshold.Selector.exists_greatest_admissible line 67

Source documentation

Every nonempty admissible set has an actual greatest cutoff.

theorem exists_greatest_admissible (w : α → ℝ) (A : Finset α) (m d : ℝ)
    (hne : ∃ u, Admissible w A m d u) :
    ∃ ε, Admissible w A m d ε ∧ ∀ u, Admissible w A m d u → u ≤ ε := by
…

Mentions: OAI.TalagrandThreshold.Selector.Admissible