Variational.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Spectral overlap deficit

The deficit D is equation (1.4) of the manuscript. Global bounded monotone representatives are used for paths on (0,1); endpoint values never enter the integrals.

structure OAI.InvariantIsing.OverlapPath line 21
Source documentation
A bounded nondecreasing representative of an admissible overlap quantile.
Also declared: ComparatorChallenges/InvariantIsing.lean:61 (same declaration text).
```
structure OverlapPath where
…
```
instance OAI.InvariantIsing.(instance at line 27) line 27
def OAI.InvariantIsing.pathMeasure line 29
Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:69 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.pathMeasure@path.
lemma OAI.InvariantIsing.pathMeasure_univ line 31
instance OAI.InvariantIsing.(instance at line 34) line 34
lemma OAI.InvariantIsing.OverlapPath.measurable line 36
lemma OAI.InvariantIsing.OverlapPath.integrable line 39
lemma OAI.InvariantIsing.OverlapPath.integrable_posPart line 44
def OAI.InvariantIsing.deficit line 53
Source documentation
Equation (1.4), defined also outside the interval for convenience.
Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:71 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.deficit@path.
```
def deficit (p : OverlapPath) (r : ℝ) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.OverlapPath
lemma OAI.InvariantIsing.deficit_one line 56
lemma OAI.InvariantIsing.deficit_nonneg line 62
lemma OAI.InvariantIsing.deficit_le line 74
lemma OAI.InvariantIsing.deficit_mem_unit line 80
lemma OAI.InvariantIsing.deficit_zero line 84
lemma OAI.InvariantIsing.deficit_antitone_path line 92
Source documentation
Pointwise order of quantiles reverses the order of deficits.
```
lemma deficit_antitone_path (p q : OverlapPath) (hpq : ∀ s, p s ≤ q s) (r : ℝ) :
    deficit q r ≤ deficit p r := by
…
```
Mentions: OAI.InvariantIsing.OverlapPath
def OAI.InvariantIsing.constantPath line 103
Source documentation
A constant quantile has deficit 1 - max q r.
```
def constantPath (q : ℝ) (hq : q ∈ Set.Icc (0 : ℝ) 1) : OverlapPath where
…
```
Mentions: OAI.InvariantIsing.OverlapPath
lemma OAI.InvariantIsing.deficit_constant line 109
lemma OAI.InvariantIsing.complement_max_eq line 119
lemma OAI.InvariantIsing.OverlapPath.integrable_complement_max line 127
lemma OAI.InvariantIsing.deficit_eq_integral line 132
lemma OAI.InvariantIsing.abs_deficit_sub_le line 139
Source documentation
The deficit is 1-Lipschitz in its scalar argument, including at atoms.
```
lemma abs_deficit_sub_le (p : OverlapPath) (r u : ℝ) :
    |deficit p r - deficit p u| ≤ |r - u| := by
…
```
Mentions: OAI.InvariantIsing.OverlapPath
lemma OAI.InvariantIsing.continuous_deficit line 154
lemma OAI.InvariantIsing.abs_deficit_sub_path_le line 162
Source documentation
Equation (4.10): uniform deficit error is bounded by the L¹ path error.
```
lemma abs_deficit_sub_path_le (p q : OverlapPath) (r : ℝ) :
    |deficit p r - deficit q r| ≤ ∫ s, |p s - q s| ∂pathMeasure := by
…
```
Mentions: OAI.InvariantIsing.OverlapPath