OAI/Combinatorics/TreewidthL1/Annulus.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

Finite adaptive random iteration. No independence assumptions on an intermediate state: every fresh coordinate is independently enumerated.

  1. lemma OAI.BoundedTreewidthL1.path_length_set_nonempty_of_reachable line 12
  2. lemma OAI.BoundedTreewidthL1.shortestPathDistance_attained_of_reachable line 18
  3. lemma OAI.BoundedTreewidthL1.shortestPathDistance_nonneg_of_reachable line 23
  4. lemma OAI.BoundedTreewidthL1.shortestPathDistance_self_of_nonneg line 29
  5. lemma OAI.BoundedTreewidthL1.shortestPathDistance_comm_of_reachable line 34
  6. lemma OAI.BoundedTreewidthL1.shortestPathDistance_triangle_of_reachable line 44
  7. lemma OAI.BoundedTreewidthL1.walkLength_takeUntil_le line 52
  8. lemma OAI.BoundedTreewidthL1.geodesic_split_of_reachable line 60
  9. lemma OAI.BoundedTreewidthL1.reachable_openBall_connected line 75

    Source documentation

    Intrinsic balls are connected even when the ambient graph is disconnected; reachability is explicit, so the empty-infimum convention never adds vertices.

    lemma reachable_openBall_connected [Fintype V] [DecidableEq V]
    (hℓ : ∀ e, 0 ≤ ℓ e) (u : V) {r : ℝ} (hr : 0 < r) :
    (G.induce {v | G.Reachable u v ∧ shortestPathDistance G ℓ u v < r}).Connected := by
…

    Mentions: OAI.BoundedTreewidthL1.shortestPathDistance

  10. lemma OAI.BoundedTreewidthL1.reachable_closedBall_connected line 94
  11. lemma OAI.BoundedTreewidthL1.shortest_closedBall_connected line 113
  12. def OAI.BoundedTreewidthL1.weightedMetricSpace line 126
  13. abbrev OAI.BoundedTreewidthL1.Annulus.weights line 141
  14. def OAI.BoundedTreewidthL1.Annulus.distance line 143
  15. def OAI.BoundedTreewidthL1.Annulus.root line 146
  16. lemma OAI.BoundedTreewidthL1.Annulus.root_reachable line 149
  17. lemma OAI.BoundedTreewidthL1.Annulus.root_eq line 152
  18. lemma OAI.BoundedTreewidthL1.Annulus.root_idem line 155
  19. def OAI.BoundedTreewidthL1.Annulus.height line 158
  20. lemma OAI.BoundedTreewidthL1.Annulus.walkLength_weights line 161
  21. lemma OAI.BoundedTreewidthL1.Annulus.walkLength_transfer line 169
  22. lemma OAI.BoundedTreewidthL1.Annulus.walkLength_mono_map line 174
  23. lemma OAI.BoundedTreewidthL1.Annulus.distance_mono line 182
  24. lemma OAI.BoundedTreewidthL1.Annulus.distance_edge line 190
  25. lemma OAI.BoundedTreewidthL1.Annulus.height_nonneg line 195
  26. lemma OAI.BoundedTreewidthL1.Annulus.height_root line 200
  27. lemma OAI.BoundedTreewidthL1.Annulus.height_eq_of_reachable line 205
  28. lemma OAI.BoundedTreewidthL1.Annulus.height_le_add_distance line 209
  29. lemma OAI.BoundedTreewidthL1.Annulus.height_edge line 216
  30. lemma OAI.BoundedTreewidthL1.Annulus.walk_crossing_below line 224

    Source documentation

    The predecessor of a first height crossing is strictly inside the ball.

    lemma walk_crossing_below (H : SimpleGraph V) (f : V → ℝ) {ε t : ℝ}
    (hstep : ∀ a b, H.Adj a b → f b ≤ f a + ε)
    {u v : V} (p : H.Walk u v) (hu : f u < t) (hv : t ≤ f v) :
    ∃ z ∈ p.support, t - ε ≤ f z ∧ f z < t := by
…
  31. def OAI.BoundedTreewidthL1.Annulus.inner line 238

    Source documentation

    The strict intrinsic inner ball, with reachability explicitly imposed.

    def inner (H : SimpleGraph V) (w : Sym2 V → ℝ) (x : V) (t : ℝ) : Set V :=
…
  32. lemma OAI.BoundedTreewidthL1.Annulus.inner_connected line 241
  33. lemma OAI.BoundedTreewidthL1.Annulus.inner_reachable line 246
  34. lemma OAI.BoundedTreewidthL1.Annulus.inner_height line 250
  35. lemma OAI.BoundedTreewidthL1.Annulus.inner_dominates line 255
  36. def OAI.BoundedTreewidthL1.Annulus.band line 283
  37. def OAI.BoundedTreewidthL1.Annulus.cut line 286
  38. lemma OAI.BoundedTreewidthL1.Annulus.cut_le line 291
  39. lemma OAI.BoundedTreewidthL1.Annulus.band_eq_of_cut_reachable line 294
  40. lemma OAI.BoundedTreewidthL1.Annulus.band_bounds line 301
  41. lemma OAI.BoundedTreewidthL1.Annulus.band_nonneg line 313
  42. theorem OAI.BoundedTreewidthL1.Annulus.cut_component_alternative line 319

    Source documentation

    A single annulus either is close to its root, or has a connected inner ball deleted from its component and uniformly close to all of that component.

    theorem cut_component_alternative [Fintype V] [DecidableEq V]
    (G H : SimpleGraph V) (hHG : H ≤ G)
    (w : Sym2 V → ℝ) (hw : ∀ e, 0 ≤ w e)
    {R a ε : ℝ} (hR : 0 < R) (ha0 : 0 ≤ a) (haR : a < R)
    (hmesh : ∀ u v, H.Adj u v → w s(u,v) ≤ ε) (x : V) :
    (∀ y z, (cut H w R a).Reachable x y → (cut H w R a).Reachable x z →
      distance G w y z ≤ 2 * R) ∨
    ∃ B : Set V, (G.induce B).Connected ∧
      (∀ z ∈ B, H.Reachable x z) ∧
      (∀ z ∈ B, ¬(cut H w R a).Reachable x z) ∧
      ∀ c, (cut H w R a).Reachable x c → ∃ z ∈ B, distance G w c z ≤ R + ε := by
…

    Mentions: OAI.BoundedTreewidthL1.Annulus.cut, OAI.BoundedTreewidthL1.Annulus.distance

  43. def OAI.BoundedTreewidthL1.Annulus.run line 379

    Source documentation

    Successive annulus cuts, with one finite random choice at each round.

    noncomputable def run (w : Sym2 V → ℝ) (R : ℝ) (offset : A → ℝ) :
    (n : ℕ) → SimpleGraph V → (Fin n → A) → SimpleGraph V
  | 0, H, _ => H
  | n + 1, H, σ => run w R offset n (cut H w R (offset (σ 0))) (fun i => σ i.succ)

    Mentions: OAI.BoundedTreewidthL1.Annulus.cut

  44. lemma OAI.BoundedTreewidthL1.Annulus.run_le line 384
  45. structure OAI.BoundedTreewidthL1.Annulus.BarrierFamily line 392

    Source documentation

    Connected barriers around a final component. The inside/outside fields are what permit nested cuts to add one more disjoint barrier at each round.

    structure BarrierFamily (G H F : SimpleGraph V) (w : Sym2 V → ℝ)
    (ρ : ℝ) (x : V) (n : ℕ) where
…
  46. theorem OAI.BoundedTreewidthL1.Annulus.run_component_alternative line 403

    Source documentation

    Deterministic invariant of the annulus recursion. A large component has one genuinely connected, disjoint nearby barrier for every cut round.

    theorem run_component_alternative [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (w : Sym2 V → ℝ) (hw : ∀ e, 0 ≤ w e)
    {R ε : ℝ} (hR : 0 < R) (offset : A → ℝ)
    (hoff0 : ∀ a, 0 ≤ offset a) (hoffR : ∀ a, offset a < R)
    (n : ℕ) (H : SimpleGraph V) (hHG : H ≤ G)
    (hmesh : ∀ u v, H.Adj u v → w s(u,v) ≤ ε) (σ : Fin n → A) (x : V) :
    (∀ y z, (run w R offset n H σ).Reachable x y →
      (run w R offset n H σ).Reachable x z → distance G w y z ≤ 2 * R) ∨
    Nonempty (BarrierFamily G H (run w R offset n H σ) w (R + ε) x n) := by
…

    Mentions: OAI.BoundedTreewidthL1.Annulus.run, OAI.BoundedTreewidthL1.Annulus.distance, OAI.BoundedTreewidthL1.Annulus.BarrierFamily

  47. lemma OAI.BoundedTreewidthL1.Annulus.reachable_set_connected line 477
  48. def OAI.BoundedTreewidthL1.TreePathClosed line 491

    Source documentation

    Convexity with respect to the unique simple paths in a tree.

    def TreePathClosed {I : Type*} (T : SimpleGraph I) (S : Set I) : Prop :=
…
  49. theorem OAI.BoundedTreewidthL1.tree_helly_aux line 495
  50. theorem OAI.BoundedTreewidthL1.tree_subtree_helly line 571

    Source documentation

    Finite trees have the Helly property for connected vertex sets. The index family need not be finite. This is the exact combinatorial input for the bounded-treewidth padded-partition construction, not a main theorem claim.

    theorem tree_subtree_helly {I J : Type*} [Fintype I]
    (T : SimpleGraph I) (hT : T.IsTree) (S : J → Set I)
    (hS : ∀ j, (T.induce (S j)).Connected)
    (hpair : ∀ i j, (S i ∩ S j).Nonempty) :
    ∃ v, ∀ j, v ∈ S j := by
…
  51. lemma OAI.BoundedTreewidthL1.touched_bags_connected_set line 583

    Source documentation

    An arbitrary nonempty connected vertex set touches a connected set of bags.

    lemma touched_bags_connected_set {V I : Type*} [DecidableEq V]
    (G : SimpleGraph V) (T : SimpleGraph I) (bag : I → Finset V)
    (hedge : ∀ u v, G.Adj u v → ∃ t, u ∈ bag t ∧ v ∈ bag t)
    (hocc : ∀ v, (T.induce {t | v ∈ bag t}).Connected)
    (S : Set V) (hS : (G.induce S).Connected) :
    (T.induce {t | ∃ z ∈ S, z ∈ bag t}).Connected := by
…
  52. lemma OAI.BoundedTreewidthL1.card_le_of_pairwise_disjoint_hits line 607
  53. theorem OAI.BoundedTreewidthL1.tree_decomposition_crossbar line 625

    Source documentation

    A crossbar of two internally disjoint families of connected sets forces a bag meeting every member of one family. Consequently its size is at least the smaller family cardinality. This is the deterministic width obstruction used by iterated annulus partitions.

    theorem tree_decomposition_crossbar {V I A B : Type*} [DecidableEq V]
    [Fintype I] [Fintype A] [Fintype B]
    (G : SimpleGraph V) (T : SimpleGraph I) (bag : I → Finset V)
    (hT : T.IsTree)
    (hedge : ∀ u v, G.Adj u v → ∃ t, u ∈ bag t ∧ v ∈ bag t)
    (hocc : ∀ v, (T.induce {t | v ∈ bag t}).Connected)
    (X : A → Set V) (Y : B → Set V)
    (hX : ∀ i, (G.induce (X i)).Connected)
    (hY : ∀ j, (G.induce (Y j)).Connected)
    (hdisX : Pairwise (fun i j => Disjoint (X i) (X j)))
    (hdisY : Pairwise (fun i j => Disjoint (Y i) (Y j)))
    (hcross : ∀ i j, (X i ∩ Y j).Nonempty) :
…
  54. lemma OAI.BoundedTreewidthL1.walk_crossing_window line 664

    Source documentation

    A discrete intermediate-value bound with an explicit mesh error.

    lemma walk_crossing_window {V : Type*} (H : SimpleGraph V) (f : V → ℝ)
    {ε t : ℝ} (hε : 0 ≤ ε)
    (hstep : ∀ a b, H.Adj a b → f b ≤ f a + ε)
    {u v : V} (p : H.Walk u v) (hu : f u ≤ t) (hv : t ≤ f v) :
    ∃ z ∈ p.support, t ≤ f z ∧ f z ≤ t + ε := by
…
  55. theorem OAI.BoundedTreewidthL1.connected_multidomination_diameter line 683

    Source documentation

    The deterministic diameter obstruction behind the annulus algorithm. The radius balls are in the original metric; only the connectivity walk in C uses the small-edge subgraph H. No intrinsic diameter replaces weak diameter.

    theorem connected_multidomination_diameter {V I : Type*} [MetricSpace V]
    [DecidableEq V] [Fintype I]
    (G H : SimpleGraph V) (hHG : H ≤ G)
    (T : SimpleGraph I) (bag : I → Finset V) (k : ℕ)
    (hT : T.IsTree)
    (hedge : ∀ u v, G.Adj u v → ∃ t, u ∈ bag t ∧ v ∈ bag t)
    (hocc : ∀ v, (T.induce {t | v ∈ bag t}).Connected)
    (hwidth : ∀ t, (bag t).card ≤ k)
    {R ε : ℝ} (hR : 0 ≤ R) (hε : 0 < ε)
    (hmesh : ∀ u v, H.Adj u v → dist u v ≤ ε)
    (hballs : ∀ c, (G.induce {z | dist c z ≤ R}).Connected)
    (C : Set V) (hC : (H.induce C).Connected)
…
  56. theorem OAI.BoundedTreewidthL1.Annulus.run_diameter line 783

    Source documentation

    The finite-round annulus decomposition has weak diameter bounded solely by the width and scale. The metric here remains the original graph metric.

    theorem run_diameter {V I A : Type*} [Fintype V] [DecidableEq V] [MetricSpace V]
    [Fintype I] (G H : SimpleGraph V) (hHG : H ≤ G)
    (w : Sym2 V → ℝ) (hw : ∀ e, 0 ≤ w e)
    (hdist : ∀ u v, dist u v = distance G w u v)
    (T : SimpleGraph I) (bag : I → Finset V) (k : ℕ) (hk : 1 ≤ k)
    (hT : T.IsTree)
    (hedge : ∀ u v, G.Adj u v → ∃ t, u ∈ bag t ∧ v ∈ bag t)
    (hocc : ∀ v, (T.induce {t | v ∈ bag t}).Connected)
    (hwidth : ∀ t, (bag t).card ≤ k)
    {R ε : ℝ} (hR : 0 < R) (hε : 0 < ε)
    (hmesh : ∀ u v, H.Adj u v → w s(u,v) ≤ ε)
    (hballs : ∀ c, (G.induce {z | dist c z ≤ R + ε}).Connected)
…

    Mentions: OAI.BoundedTreewidthL1.Annulus.distance

  57. lemma OAI.BoundedTreewidthL1.Annulus.floor_ne_boundary line 833
  58. theorem OAI.BoundedTreewidthL1.Annulus.grid_bad_subsingleton line 843

    Source documentation

    A random finite grid incurs at most one bad offset at any prescribed height. No minimum positive edge length enters this count.

    theorem grid_bad_subsingleton (M : ℕ) (hM : 0 < M) (t β : ℝ)
    (hβ : 0 ≤ β) (hsep : 2 * (M : ℝ) * β < 1) :
    {j : Fin M | ⌊t + (j.val : ℝ) / M - β⌋ ≠ ⌊t + (j.val : ℝ) / M + β⌋}.Subsingleton := by
…
  59. lemma OAI.BoundedTreewidthL1.Annulus.floor_eq_of_window line 893
  60. lemma OAI.BoundedTreewidthL1.Annulus.walkLength_edge_le line 902
  61. def OAI.BoundedTreewidthL1.Annulus.smallEdges line 918
  62. lemma OAI.BoundedTreewidthL1.Annulus.smallEdges_le line 923
  63. lemma OAI.BoundedTreewidthL1.Annulus.smallEdges_mesh line 926
  64. lemma OAI.BoundedTreewidthL1.Annulus.smallEdges_mem_iff line 929
  65. def OAI.BoundedTreewidthL1.Annulus.PreservesBall line 936

    Source documentation

    The ball is preserved with its actual original shortest paths, not only with unquantified reachability. This is the induction invariant for padding.

    def PreservesBall (G H : SimpleGraph V) (w : Sym2 V → ℝ) (ε : ℝ) (x : V) : Prop :=
…
  66. lemma OAI.BoundedTreewidthL1.Annulus.smallEdges_preserves line 940
  67. lemma OAI.BoundedTreewidthL1.Annulus.walk_height_window line 952
  68. lemma OAI.BoundedTreewidthL1.Annulus.band_eq_of_height_window line 970
  69. lemma OAI.BoundedTreewidthL1.Annulus.preservesBall_cut line 987
  70. def OAI.BoundedTreewidthL1.Annulus.gridOffset line 1010
  71. lemma OAI.BoundedTreewidthL1.Annulus.gridOffset_nonneg line 1012
  72. lemma OAI.BoundedTreewidthL1.Annulus.gridOffset_lt line 1015
  73. lemma OAI.BoundedTreewidthL1.Annulus.grid_window_eq line 1022
  74. def OAI.FiniteRandomIteration.run line 1038
  75. def OAI.FiniteRandomIteration.count line 1042
  76. lemma OAI.FiniteRandomIteration.count_nonneg line 1047
  77. lemma OAI.FiniteRandomIteration.count_succ line 1052
  78. lemma OAI.FiniteRandomIteration.count_lower line 1061
  79. lemma OAI.FiniteRandomIteration.fraction_lower line 1104
  80. lemma OAI.BoundedTreewidthL1.Annulus.run_eq_iteration line 1131
  81. lemma OAI.BoundedTreewidthL1.Annulus.preserves_bad_subsingleton line 1139
  82. lemma OAI.BoundedTreewidthL1.Annulus.preserves_fraction line 1156
  83. def OAI.FiniteLawPush.law line 1179
  84. lemma OAI.FiniteLawPush.nonneg line 1183
  85. lemma OAI.FiniteLawPush.total line 1189
  86. lemma OAI.FiniteLawPush.supported line 1197
  87. lemma OAI.FiniteLawPush.event line 1205