SelectorTruncationDefinitions.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite weighted truncation

The heavy set uses a strict cutoff. Weights equal to the cutoff are already saturated when the cutoff increases, as required by the maximal truncation argument.

def OAI.TalagrandThreshold.Selector.heavySet line 22
Source documentation
The points whose weight is strictly above the cutoff.
```
noncomputable def heavySet (w : α → ℝ) (u : ℝ) : Finset α := by
…
```
def OAI.TalagrandThreshold.Selector.truncatedExcess line 27
Source documentation
The excess mass after every coordinate is truncated at the same cutoff.
```
noncomputable def truncatedExcess (w : α → ℝ) (A : Finset α) (d u : ℝ) : ℝ :=
…
```
def OAI.TalagrandThreshold.Selector.Admissible line 32
Source documentation
An admissible cutoff includes all heavy points and meets the truncated weighted-excess test.
```
def Admissible (w : α → ℝ) (A : Finset α) (m d u : ℝ) : Prop :=
…
```
theorem OAI.TalagrandThreshold.Selector.mem_heavySet line 37
theorem OAI.TalagrandThreshold.Selector.Admissible.heavy_subset line 42
theorem OAI.TalagrandThreshold.Selector.Admissible.outside_le line 47