OAI/Analysis/DiamondDistortion/DiamondGraph.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DiamondDistortion.Diamond.Edge line 16

   Source documentation

   Stage edges, retaining their parent, child number, and side.

   Also declared: ComparatorChallenges/DiamondDistortion.lean:276 (same declaration text).

   @[reducible] def Edge : ℕ → Type
     | 0 => Unit
     | n + 1 => Edge n × ℕ × Bool
   
   /-- At every replacement every parent edge receives countably many distinct new vertices. -/

2. def OAI.DiamondDistortion.Diamond.Vertex line 21

   Source documentation

   At every replacement every parent edge receives countably many distinct new vertices.

   Also declared: ComparatorChallenges/DiamondDistortion.lean:281 (same declaration text).

   @[reducible] def Vertex : ℕ → Type
     | 0 => Bool
     | n + 1 => Vertex n ⊕ (Edge n × ℕ)

   Mentions: OAI.DiamondDistortion.Diamond.Edge

3. def OAI.DiamondDistortion.Diamond.endpoint line 25

   Also declared: ComparatorChallenges/DiamondDistortion.lean:285 (same declaration text).

4. def OAI.DiamondDistortion.Diamond.graph line 33

   Source documentation

   The undirected replacement graph.

   Also declared: ComparatorChallenges/DiamondDistortion.lean:293 (same declaration text).

   def graph (n : ℕ) : SimpleGraph (Vertex n) :=
   …

   Mentions: OAI.DiamondDistortion.Diamond.Vertex

5. def OAI.DiamondDistortion.Diamond.baseEdge line 36
6. lemma OAI.DiamondDistortion.Diamond.endpoint_ne line 40
7. lemma OAI.DiamondDistortion.Diamond.adj_iff line 47
8. lemma OAI.DiamondDistortion.Diamond.adj_endpoint line 59
9. lemma OAI.DiamondDistortion.Diamond.adj_old_mid line 63
10. lemma OAI.DiamondDistortion.Diamond.not_adj_old line 80
11. lemma OAI.DiamondDistortion.Diamond.not_adj_new line 86
12. lemma OAI.DiamondDistortion.Diamond.replace_adj line 92
13. lemma OAI.DiamondDistortion.Diamond.replace_walk line 100
14. lemma OAI.DiamondDistortion.Diamond.connected line 111
15. lemma OAI.DiamondDistortion.Diamond.potential_walk line 137
16. lemma OAI.DiamondDistortion.Diamond.distance_potential line 148
17. def OAI.DiamondDistortion.Diamond.extendPotential line 160
18. lemma OAI.DiamondDistortion.Diamond.extendPotential_adj line 164
19. lemma OAI.DiamondDistortion.Diamond.dist_old line 178

    Source documentation

    One subdivision doubles unweighted old-vertex distances.

    lemma dist_old (n : ℕ) (u v : Vertex n) :
        (graph (n+1)).dist (Sum.inl u) (Sum.inl v)=2*(graph n).dist u v := by
    …

    Mentions: OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.graph

20. lemma OAI.DiamondDistortion.Diamond.dist_siblings line 192
21. theorem OAI.DiamondDistortion.Diamond.two_atLeastTwo line 203
22. def OAI.DiamondDistortion.Diamond.distance line 206

    Source documentation

    Final edges have length 2⁻ᵏ: this is the shortest-path metric of the normalized graph.

    Also declared: ComparatorChallenges/DiamondDistortion.lean:297 (same declaration text).

    def distance (k : ℕ) (u v : Vertex k) : ℝ :=
    …

    Mentions: OAI.DiamondDistortion.Diamond.Vertex

23. def OAI.DiamondDistortion.Diamond.HasDistortion line 210

    Source documentation

    The standing all-pairs distortion hypothesis, with its positive arbitrary scale.

    def HasDistortion {X : Type*} [NormedAddCommGroup X]
        (k : ℕ) (f : Vertex k → X) (D s : ℝ) : Prop :=
    …

    Mentions: OAI.DiamondDistortion.Diamond.Vertex

24. lemma OAI.DiamondDistortion.Diamond.distance_old line 216
25. lemma OAI.DiamondDistortion.Diamond.distance_edge line 221
26. lemma OAI.DiamondDistortion.Diamond.distance_siblings line 225
27. def OAI.DiamondDistortion.Diamond.slope line 232

    Source documentation

    The oriented slope of a stage edge in the normalized metric.

    def slope {n : ℕ} (f : Vertex n → X) (e : Edge n) : X :=
    …

    Mentions: OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.Edge

28. def OAI.DiamondDistortion.Diamond.deviation line 236

    Source documentation

    Midpoint deviations normalized by the lengths of the parent edges.

    def deviation {n : ℕ} (f : Vertex (n+1) → X) (e : Edge n) (i : ℕ) : X :=
    …

    Mentions: OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.Edge

29. lemma OAI.DiamondDistortion.Diamond.slope_plus_deviation line 240
30. lemma OAI.DiamondDistortion.Diamond.slope_minus_deviation line 246
31. lemma OAI.DiamondDistortion.Diamond.deviation_sub line 252
32. lemma OAI.DiamondDistortion.Diamond.deviation_separated line 259
33. def OAI.DiamondDistortion.Diamond.QuadraticLens line 270

    Source documentation

    An infinite separated symmetric lens with the exact quadratic constant.

    def QuadraticLens (X : Type*) [NormedAddCommGroup X] : Prop :=
    …

34. lemma OAI.DiamondDistortion.Diamond.squared_stretch_loss line 277

    Source documentation

    Supremum-free squared stretch-loss induction. The bound on all final-edge slopes loses s²/4 at each backward step. No maximum child is used.

    lemma squared_stretch_loss (hX : QuadraticLens X) (k : ℕ) (f : Vertex k → X)
        {s B : ℝ} (hs : 0 < s)
        (hl : ∀ u v,s*distance k u v ≤ ‖f u-f v‖)
        (hb : ∀ e,‖slope f e‖^2 ≤ B) : s^2*(1+(k:ℝ)/4) ≤ B := by
    …

    Mentions: OAI.DiamondDistortion.Diamond.QuadraticLens, OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.distance, OAI.DiamondDistortion.Diamond.slope

35. lemma OAI.DiamondDistortion.Diamond.distortion_bound line 313
36. def OAI.DiamondDistortion.Headline line 334

    Source documentation

    The exact two-model unconditional headline; neither intrinsic estimate is a hypothesis.

    def Headline : Prop :=
    …

37. theorem OAI.DiamondDistortion.forest_quadratic_lens line 342

    Source documentation

    The finite forest lens property follows from the proved pooled estimate and the proved approximation of its full dual.

    theorem forest_quadratic_lens : Diamond.QuadraticLens ForestDual := by
    …

    Mentions: OAI.DiamondDistortion.Diamond.QuadraticLens, OAI.DiamondDistortion.ForestDual

38. theorem OAI.DiamondDistortion.infinite_quadratic_lens line 349

    Source documentation

    The infinite-height assertion is only for its closed coordinate span, not for the full infinite-height dual.

    theorem infinite_quadratic_lens : Diamond.QuadraticLens InfinitePredual := by
    …

    Mentions: OAI.DiamondDistortion.Diamond.QuadraticLens, OAI.DiamondDistortion.InfinitePredual

39. theorem OAI.DiamondDistortion.headline line 355