OAI/Analysis/ForestSpace/Diamonds.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ForestSpace.Diamond.Network line 18

    Source documentation

    An oriented edge enumeration; only the associated undirected unit-edge simple graph is used for distances.

    Also declared: ComparatorChallenges/ForestSpace.lean:388 (same declaration text).

    structure Network where
…
  2. def OAI.ForestSpace.Diamond.Network.graph line 28

    Also declared: ComparatorChallenges/ForestSpace.lean:399 (same declaration text).

  3. theorem OAI.ForestSpace.Diamond.Network.edge_adj line 40
  4. def OAI.ForestSpace.Diamond.Network.refine line 45

    Source documentation

    Every edge is replaced by countably many internally disjoint two-edge paths. All old vertices remain, and each pair (edge,index) is a new midpoint.

    Also declared: ComparatorChallenges/ForestSpace.lean:413 (same declaration text).

    @[reducible] def refine : Network where
…

    Mentions: OAI.ForestSpace.Diamond.Network

  5. theorem OAI.ForestSpace.Diamond.Network.refine_adj_left line 52
  6. theorem OAI.ForestSpace.Diamond.Network.refine_adj_right line 56
  7. theorem OAI.ForestSpace.Diamond.Network.refine_no_adj_middle line 60
  8. theorem OAI.ForestSpace.Diamond.Network.refine_no_adj_old line 65
  9. theorem OAI.ForestSpace.Diamond.Network.refine_adj_lift line 70
  10. theorem OAI.ForestSpace.Diamond.Network.refine_walk_lift line 79
  11. theorem OAI.ForestSpace.Diamond.Network.refine_connected line 91
  12. theorem OAI.ForestSpace.Diamond.potential_bound line 114
  13. theorem OAI.ForestSpace.Diamond.Network.adj_dist_potential line 131
  14. def OAI.ForestSpace.Diamond.Network.refinePotential line 143
  15. theorem OAI.ForestSpace.Diamond.Network.refinePotential_adj line 147
  16. theorem OAI.ForestSpace.Diamond.Network.refine_dist_old line 158
  17. theorem OAI.ForestSpace.Diamond.Network.refine_dist_middle line 172
  18. def OAI.ForestSpace.Diamond.Network.iterate line 186

    Source documentation

    Iterating the very same edge replacement, starting from an arbitrary network. This recursion groups the first replacement before the remaining ones.

    Also declared: ComparatorChallenges/ForestSpace.lean:422 (same declaration text).

    @[reducible] def iterate : Network → ℕ → Network
  | A,0 => A
  | A,n+1 => iterate A.refine n

/-- The canonical inclusion of all old vertices through finitely many refinements. -/

    Mentions: OAI.ForestSpace.Diamond.Network, OAI.ForestSpace.Diamond.Network.old

  19. def OAI.ForestSpace.Diamond.Network.old line 191

    Source documentation

    The canonical inclusion of all old vertices through finitely many refinements.

    def old : (A : Network) → (n : ℕ) → A.V → (A.iterate n).V
  | _,0 => id
  | A,n+1 => fun u => A.refine.old n (Sum.inl u)

    Mentions: OAI.ForestSpace.Diamond.Network

  20. theorem OAI.ForestSpace.Diamond.Network.old_zero line 195
  21. theorem OAI.ForestSpace.Diamond.Network.old_succ line 196
  22. theorem OAI.ForestSpace.Diamond.Network.old_injective line 199
  23. theorem OAI.ForestSpace.Diamond.Network.iterate_connected line 204
  24. theorem OAI.ForestSpace.Diamond.Network.old_dist line 210
  25. theorem OAI.ForestSpace.Diamond.Network.old_edge_dist line 220
  26. theorem OAI.ForestSpace.Diamond.Network.old_middle_dist line 224
  27. def OAI.ForestSpace.Diamond.base line 234

    Source documentation

    D₀ is precisely one edge.

    Also declared: ComparatorChallenges/ForestSpace.lean:429 (same declaration text).

    @[reducible] def base : Network where
…

    Mentions: OAI.ForestSpace.Diamond.Network

  28. theorem OAI.ForestSpace.Diamond.base_connected line 241
  29. def OAI.ForestSpace.Diamond.diamond line 251

    Source documentation

    Countably branching diamonds, all current edges of length one.

    Also declared: ComparatorChallenges/ForestSpace.lean:437 (same declaration text).

    @[reducible] def diamond (k : ℕ) := base.iterate k
  30. def OAI.ForestSpace.Diamond.distance line 254

    Source documentation

    The shortest-path distance, via Mathlib's actual graph distance.

    Distinct definitions of this name: ComparatorChallenges/ForestSpace.lean:440 (same statement text; different proof or body). Qualify references as OAI.ForestSpace.Diamond.distance@path.

    def distance (k : ℕ) (u v : (diamond k).V) : ℝ := ((diamond k).graph.dist u v : ℝ)

    Mentions: OAI.ForestSpace.Diamond.diamond

  31. theorem OAI.ForestSpace.Diamond.diamond_connected line 256
  32. theorem OAI.ForestSpace.Diamond.Network.iterate_succ_refine line 260

    Source documentation

    Our tail-recursive presentation is exactly successive edge replacement.

    theorem Network.iterate_succ_refine (A : Network) (n : ℕ) :
    A.iterate (n+1) = (A.iterate n).refine := by
…

    Mentions: OAI.ForestSpace.Diamond.Network, OAI.ForestSpace.Diamond.Network.refine

  33. theorem OAI.ForestSpace.Diamond.diamond_zero line 266
  34. theorem OAI.ForestSpace.Diamond.diamond_succ line 268
  35. theorem OAI.ForestSpace.Diamond.Network.iterate_countable line 271
  36. theorem OAI.ForestSpace.Diamond.diamond_countable line 278

    Source documentation

    Vertices and edges really are countable at each finite diamond stage.

    theorem diamond_countable (k : ℕ) : Countable (diamond k).V ∧ Countable (diamond k).E :=
…

    Mentions: OAI.ForestSpace.Diamond.diamond

  37. theorem OAI.ForestSpace.Diamond.distance_nonneg line 281
  38. theorem OAI.ForestSpace.Diamond.distance_eq_zero_iff line 285
  39. theorem OAI.ForestSpace.Diamond.distance_comm line 290
  40. theorem OAI.ForestSpace.Diamond.distance_triangle line 295
  41. def OAI.ForestSpace.Diamond.Network.UniqueEdges line 304

    Source documentation

    Every undirected edge has exactly one entry in the oriented enumeration. Thus refinement replaces genuine graph edges, not a multiset of edges.

    def Network.UniqueEdges (A : Network) : Prop :=
…

    Mentions: OAI.ForestSpace.Diamond.Network

  42. theorem OAI.ForestSpace.Diamond.Network.refine_uniqueEdges line 308
  43. theorem OAI.ForestSpace.Diamond.Network.iterate_uniqueEdges line 316
  44. theorem OAI.ForestSpace.Diamond.diamond_uniqueEdges line 322