TailOrder.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The upper-tail order used in the finite-spectrum upper comparison.

def OAI.InvariantIsing.pathTail line 13
lemma OAI.InvariantIsing.posPart_integral_eq_interval line 15
lemma OAI.InvariantIsing.pathTail_sub_le_posPart line 20
lemma OAI.InvariantIsing.exists_path_level_cutoff line 43
Source documentation
A monotone quantile crosses any horizontal level at a cutoff, allowing a jump or a nontrivial atom at that level. Endpoint values play no role.
```
lemma exists_path_level_cutoff (p : OverlapPath) (r : ℝ) :
    ∃ s ∈ Icc (0 : ℝ) 1,
      (∀ u ∈ Ioo 0 s, p u ≤ r) ∧ (∀ u ∈ Ioo s 1, r ≤ p u) := by
…
```
Mentions: OAI.InvariantIsing.OverlapPath
lemma OAI.InvariantIsing.exists_posPart_eq_pathTail line 73
Source documentation
The positive-part integral is attained by a tail of the quantile.
```
lemma exists_posPart_eq_pathTail (p : OverlapPath) (r : ℝ) :
    ∃ s ∈ Icc (0 : ℝ) 1,
      (∫ u, max (p u - r) 0 ∂pathMeasure) = pathTail p s - (1 - s) * r := by
…
```
Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.pathTail
theorem OAI.InvariantIsing.deficit_le_of_pathTail_le line 106
Source documentation
Manuscript up:tail-order: ordering every upper tail reverses the entire deficit function, including at jumps and atoms of either overlap quantile.
```
theorem deficit_le_of_pathTail_le (p q : OverlapPath)
    (htail : ∀ s ∈ Icc (0 : ℝ) 1, pathTail q s ≤ pathTail p s) (r : ℝ) :
    deficit p r ≤ deficit q r := by
…
```
Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.pathTail