SelectorTruncation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Maximal weighted truncation

This is the maximal truncation lemma used by the multiscale selector. The cutoff is obtained from the actual compact admissible set. Its heavy-set bound follows from the exact affine increase on the next interval between weights, rather than an assumed slope or regularity certificate.

theorem OAI.TalagrandThreshold.Selector.exists_maximal_truncation line 23

Source documentation

A nonempty admissible set has a greatest cutoff, whose heavy set satisfies the multiplied cardinality bound.

theorem exists_maximal_truncation (w : α → ℝ) (A : Finset α) (m d : ℝ)
    (hw : ∀ x, 0 ≤ w x) (hsum : ∑ x, w x = 1)
    (hm : 0 ≤ m) (hd0 : 0 < d) (hd1 : d < 1)
    (hne : ∃ u, Admissible w A m d u) :
    ∃ ε, Admissible w A m d ε ∧
      (∀ u, Admissible w A m d u → u ≤ ε) ∧
      d * ((heavySet w ε).card : ℝ) ≤ m := by
…

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

theorem OAI.TalagrandThreshold.Selector.exists_maximal_truncation_div line 35

Source documentation

The division form of the maximal truncation lemma.

theorem exists_maximal_truncation_div (w : α → ℝ) (A : Finset α) (m d : ℝ)
    (hw : ∀ x, 0 ≤ w x) (hsum : ∑ x, w x = 1)
    (hm : 0 ≤ m) (hd0 : 0 < d) (hd1 : d < 1)
    (hne : ∃ u, Admissible w A m d u) :
    ∃ ε, Admissible w A m d ε ∧
      (∀ u, Admissible w A m d u → u ≤ ε) ∧
      ((heavySet w ε).card : ℝ) ≤ m / d := by
…

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