HeightTree.lean`

73 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.PlanarL1.HeightTree line 15
Source documentation
A rooted incidence tree with a nondecreasing metric height. Unlike the shortest-path tree, added terminal branches are permitted to have zero length. Termination follows the incidence tree, not strict metric height.
```
structure HeightTree (V : Type*) where
…
```
abbrev OAI.PlanarL1.HeightTree.Step line 27
abbrev OAI.PlanarL1.HeightTree.Ancestor line 28
lemma OAI.PlanarL1.HeightTree.ancestor_height line 30
def OAI.PlanarL1.HeightTree.profile line 37
Source documentation
McShane cones over the finite ancestral chain. The recursive minimum is used instead of linear interpolation, so zero-length incidences need no division.
```
noncomputable def profile (q : V → ℝ) (v : V) : ℝ → ℝ :=
…
```
lemma OAI.PlanarL1.HeightTree.profile_eq line 41
lemma OAI.PlanarL1.HeightTree.profile_root line 47
lemma OAI.PlanarL1.HeightTree.profile_child line 51
lemma OAI.PlanarL1.HeightTree.profile_le_cone line 55
lemma OAI.PlanarL1.HeightTree.profile_lipschitz line 61
def OAI.PlanarL1.HeightTree.Compatible line 75
Source documentation
Discrete one-Lipschitz data along the actual tree edges.
```
def Compatible (q : V → ℝ) : Prop :=
…
```
lemma OAI.PlanarL1.HeightTree.profile_above line 78
lemma OAI.PlanarL1.HeightTree.profile_at line 90
lemma OAI.PlanarL1.HeightTree.profile_below_parent line 94

lemma OAI.PlanarL1.HeightTree.profile_ancestor line 106

Source documentation

Common root prefixes receive literally the same potential on every copy.

lemma profile_ancestor {q : V → ℝ} (hq : T.Compatible q) {u v : V}
    (h : T.Ancestor u v) {H : ℝ} (hH : H ≤ T.height u) :
    T.profile q v H = T.profile q u H := by
…

lemma OAI.PlanarL1.HeightTree.root_ancestor line 116
def OAI.PlanarL1.HeightTree.depth line 123
lemma OAI.PlanarL1.HeightTree.depth_eq line 127
lemma OAI.PlanarL1.HeightTree.step_depth line 132
lemma OAI.PlanarL1.HeightTree.ancestor_depth line 136
lemma OAI.PlanarL1.HeightTree.ancestor_antisymm line 141
def OAI.PlanarL1.HeightTree.IsLeaf line 150
lemma OAI.PlanarL1.HeightTree.exists_leaf line 152
def OAI.PlanarL1.HeightTree.leafAbove line 161
lemma OAI.PlanarL1.HeightTree.ancestor_leafAbove line 164
def OAI.PlanarL1.Weighted.ExtraDart line 177
Source documentation
Each orientation is one distinct new branch incidence. Paired incidences are not identified until the column switch is installed.
```
def ExtraDart (hc : G.Connected) (hs : ∀ u v, l u v=l v u)
    (hl : ∀ u v, G.Adj u v → 0<l u v) (o : V) :=
…
```
def OAI.PlanarL1.Weighted.ExtraDart.reverse line 185
lemma OAI.PlanarL1.Weighted.ExtraDart.reverse_reverse line 188
def OAI.PlanarL1.Weighted.ExtraDart.tipHeight line 193
lemma OAI.PlanarL1.Weighted.ExtraDart.tipHeight_reverse line 196
lemma OAI.PlanarL1.Weighted.ExtraDart.height_le_tip line 203
abbrev OAI.PlanarL1.Weighted.EnlargedTree.Node line 215
def OAI.PlanarL1.Weighted.EnlargedTree.parent line 217
def OAI.PlanarL1.Weighted.EnlargedTree.height line 221
lemma OAI.PlanarL1.Weighted.EnlargedTree.parent_wf line 225
def OAI.PlanarL1.Weighted.EnlargedTree.tree line 246
Source documentation
An abstract height tree, including zero-length branches.
```
noncomputable def tree : HeightTree (Node hc hs hl o) where
…
```
Mentions: OAI.PlanarL1.HeightTree, OAI.PlanarL1.Weighted.EnlargedTree.Node
lemma OAI.PlanarL1.Weighted.EnlargedTree.extra_leaf line 264
def OAI.PlanarL1.Weighted.EnlargedTree.potential line 271
Source documentation
Graph-distance potentials extended to the two endpoints of each split edge by their shortest distance through either of that edge's endpoints.
```
noncomputable def potential (z : V) : Node hc hs hl o → ℝ
  | .inl v => graphDistance G l z v
  | .inr d => min
      (graphDistance G l z d.val.fst + ExtraDart.tipHeight hc hs hl o d - graphDistance G l o d.val.fst)
      (graphDistance G l z d.val.snd + ExtraDart.tipHeight hc hs hl o d - graphDistance G l o d.val.snd)
```
Mentions: OAI.PlanarL1.Weighted.EnlargedTree.Node, OAI.PlanarL1.graphDistance, OAI.PlanarL1.Weighted.ExtraDart.tipHeight
lemma OAI.PlanarL1.Weighted.EnlargedTree.potential_reverse line 277
lemma OAI.PlanarL1.Weighted.EnlargedTree.min_split_compatible line 286
lemma OAI.PlanarL1.Weighted.EnlargedTree.potential_compatible line 297
def OAI.PlanarL1.HeightTree.prefixGraph line 335
Source documentation
Adjacent copies in the cyclic contour of an ancestral subtree.
```
def prefixGraph (leaf : Fin n → V) (a : V) : SimpleGraph (Fin n) where
…
```
structure OAI.PlanarL1.HeightTree.Layout line 349
Source documentation
The combinatorial output of a planar tree contour construction. No metric realization or metric estimates are part of this data.
```
structure Layout (n : ℕ) where
…
```
def OAI.PlanarL1.HeightTree.Layout.heights line 364
lemma OAI.PlanarL1.HeightTree.Layout.mem_heights line 370
lemma OAI.PlanarL1.HeightTree.Layout.heights_symm line 377
lemma OAI.PlanarL1.HeightTree.Layout.heights_compact line 388
lemma OAI.PlanarL1.HeightTree.Layout.switch_le_tip line 396
def OAI.PlanarL1.HeightTree.Layout.model line 402

def OAI.PlanarL1.HeightTree.Layout.prefixPath line 442

Source documentation

Constant-height switches connect all copies on a common root prefix.

noncomputable def prefixPath {a : V} {i j : Fin n}
    (p : (T.prefixGraph L.leaf a).Walk i j) {H : ℝ}
    (hlo : T.height T.root ≤ H) (hhi : H ≤ T.height a) :
    L.model.Path univ i j :=
…

lemma OAI.PlanarL1.HeightTree.Layout.prefixPath_length line 451
lemma OAI.PlanarL1.HeightTree.Layout.exists_prefixPath line 459
def OAI.PlanarL1.HeightTree.Layout.column line 466
lemma OAI.PlanarL1.HeightTree.Layout.ancestor_column line 469
def OAI.PlanarL1.HeightTree.Layout.point line 473

lemma OAI.PlanarL1.Columns.Model.Path.potential_le line 491

Source documentation

A scalar potential compatible with every actual switch bounds the length of every switching path, irrespective of excursions into the separate tails.

lemma Path.potential_le {J : Set ℝ} {i j : Fin n} (p : M.Path J i j)
    (q : Fin n → ℝ → ℝ) (hLip : ∀ i, LipschitzWith 1 (q i))
    (hSwitch : ∀ i j H, H ∈ M.heights i j → q i H=q j H) (a b : ℝ) :
    |q i a-q j b| ≤ p.length a b := by
…

lemma OAI.PlanarL1.Columns.Model.Point.potential_le line 504
lemma OAI.PlanarL1.HeightTree.IsLeaf.ancestor_eq line 518
lemma OAI.PlanarL1.HeightTree.Layout.leaf_column line 526
lemma OAI.PlanarL1.HeightTree.Layout.column_leaf line 529
lemma OAI.PlanarL1.HeightTree.Layout.profile_switch line 532
lemma OAI.PlanarL1.HeightTree.Layout.potential_le line 540
lemma OAI.PlanarL1.HeightTree.Layout.parent_distance_le line 551
lemma OAI.PlanarL1.HeightTree.Layout.pair_distance_zero line 565
instance OAI.PlanarL1.Weighted.ExtraDart.fintype line 587
def OAI.PlanarL1.Weighted.EnlargedTree.ExactPairs line 595
Source documentation
The leaf pairs are precisely the two incidences of each original non-tree edge, not extra shortcuts.
```
def ExactPairs : Prop := ∀ i j, L.pair.Adj i j ↔ ∃ d : ExtraDart hc hs hl o,
…
```
Mentions: OAI.PlanarL1.Weighted.ExtraDart
lemma OAI.PlanarL1.Weighted.EnlargedTree.original_distance_lower line 598
lemma OAI.PlanarL1.Weighted.EnlargedTree.tip_pair line 608
lemma OAI.PlanarL1.Weighted.EnlargedTree.tip_distance_zero line 614
lemma OAI.PlanarL1.Weighted.EnlargedTree.original_parent_distance line 620
lemma OAI.PlanarL1.Weighted.EnlargedTree.original_edge_distance line 630
lemma OAI.PlanarL1.Weighted.EnlargedTree.original_walk_distance line 657
lemma OAI.PlanarL1.Weighted.EnlargedTree.original_distance line 668
Source documentation
The original weighted graph embeds isometrically into the actual column path metric. In particular all tails and zero-length branch incidences are accounted for; the lower bound is certified by graph-distance potentials.
```
lemma original_distance (hpair : ExactPairs L) (u v : V) :
    (L.point (.inl u)).distance (L.point (.inl v))=graphDistance G l u v := by
…
```
Mentions: OAI.PlanarL1.Weighted.EnlargedTree.ExactPairs, OAI.PlanarL1.graphDistance