Descent.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DiamondDistortion.PathModel.linear_regular line 19
Source documentation
Ancestral coordinate projections for the literal linear path cost are contractive, jointly cofinal, and nested in both orders.
```
theorem linear_regular : Regular linearHeads where
…
```
Mentions: OAI.DiamondDistortion.PathModel.linearHeads
theorem OAI.DiamondDistortion.PathModel.adaptive_graph line 26
theorem OAI.DiamondDistortion.PathModel.predictable_495_graph line 33
theorem OAI.DiamondDistortion.PathModel.variation_252_graph line 38
theorem OAI.DiamondDistortion.PathModel.leakage_1024_graph line 43
theorem OAI.DiamondDistortion.PathModel.squared_gap_400_graph line 50
theorem OAI.DiamondDistortion.DirectSegmentApplications.deterministic_descent line 63
theorem OAI.DiamondDistortion.DirectSegmentApplications.bin_descent line 68
lemma OAI.DiamondDistortion.Diamond.hasDistortion_iff_all_pairs line 87
Source documentation
The redundant conventional condition D≥1 follows from the all-pairs inequalities alone; thus HasDistortion adds no standing hypothesis.
```
lemma hasDistortion_iff_all_pairs {k : ℕ} (f : Vertex k → X) (D s : ℝ) :
    HasDistortion k f D s ↔ 0 < s ∧ ∀ u v,
      s*distance k u v ≤ ‖f u-f v‖ ∧ ‖f u-f v‖ ≤ D*s*distance k u v := by
…
```
Mentions: OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.HasDistortion, OAI.DiamondDistortion.Diamond.distance
theorem OAI.DiamondDistortion.headline_all_pairs line 104
Distinct definitions of this name: ComparatorChallenges/DiamondDistortion.lean:302 (same statement text; different proof or body). Qualify references as OAI.DiamondDistortion.headline_all_pairs@path.
theorem OAI.DiamondDistortion.direct_atomic_obstruction_positive line 117