SelectorTruncationSlope.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The right-hand slope at a maximal admissible cutoff

A finite minimum provides an actual larger cutoff below every currently heavy weight. Between these cutoffs the truncated excess has the exact affine increment contributed by the heavy coordinates. Weights equal to the original cutoff remain saturated, including when the cutoff is zero.

theorem OAI.TalagrandThreshold.Selector.exists_short_right_cutoff line 27
Source documentation
There is a strictly larger cutoff, at most one, that does not pass any weight strictly above the current cutoff.
```
theorem exists_short_right_cutoff (w : α → ℝ) {ε : ℝ} (hε : ε < 1) :
    ∃ u : ℝ, ε < u ∧ u ≤ 1 ∧ ∀ x, ε < w x → u ≤ w x := by
…
```
theorem OAI.TalagrandThreshold.Selector.truncatedExcess_sub_eq_heavy_increment line 46
Source documentation
On the first interval to the right of a cutoff, precisely the strictly heavy coordinates vary. The inclusion in A makes their coefficient d.
```
theorem truncatedExcess_sub_eq_heavy_increment (w : α → ℝ) (A : Finset α)
    (d ε u : ℝ) (hεu : ε ≤ u)
    (hupper : ∀ x, ε < w x → u ≤ w x)
    (hheavy : ∀ x, ε < w x → x ∈ A) :
    truncatedExcess w A d u - truncatedExcess w A d ε =
      (u - ε) * d * ((heavySet w ε).card : ℝ) := by
…
```
Mentions: OAI.TalagrandThreshold.Selector.truncatedExcess, OAI.TalagrandThreshold.Selector.heavySet

theorem OAI.TalagrandThreshold.Selector.maximal_admissible_card_bound line 76

Source documentation

The cardinality conclusion of maximal truncation. Existence of a maximal admissible cutoff is supplied separately by compactness.

theorem maximal_admissible_card_bound (w : α → ℝ) (A : Finset α) (m d ε : ℝ)
    (hwnonneg : ∀ x, 0 ≤ w x) (hwsum : ∑ x, w x = 1)
    (hm0 : 0 ≤ m) (_hd0 : 0 < d) (_hd1 : d < 1)
    (hε : Admissible w A m d ε)
    (hmax : ∀ u : ℝ, Admissible w A m d u → u ≤ ε) :
    d * ((heavySet w ε).card : ℝ) ≤ m := by
…

Mentions: OAI.TalagrandThreshold.Selector.Admissible, OAI.TalagrandThreshold.Selector.heavySet