OAI/Combinatorics/TreewidthL1/Anchors.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreewidthL1.AnchorTreeParticles.retained line 12
2. def OAI.BoundedTreewidthL1.AnchorTreeParticles.fresh line 14
3. def OAI.BoundedTreewidthL1.AnchorTreeParticles.seed line 16
4. def OAI.BoundedTreewidthL1.AnchorTreeParticles.step line 18
5. def OAI.BoundedTreewidthL1.AnchorTreeParticles.state line 21
6. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.retained_subset line 25
7. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.batch_data line 32
8. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.state_eq line 44
9. theorem OAI.BoundedTreewidthL1.AnchorTreeParticles.forest_particle_realization line 53

   Source documentation

   Actual branching preparation for anchor keys, launched at their own bag. Children use their own copies of the parent's list; no consistency assumption on sampled bag laws.

   theorem forest_particle_realization (R : RootedForest I) (bag : I → Finset V)
       (A : I → Finset J) (k q : ℕ) (hbag : ∀ i, (bag i).card ≤ k)
       (hA : ∀ i, (A i).card ≤ q) (hN : Fintype.card ι = 2*q + k.factorial + 2)
       (d : V → V → ℝ) (L H Δ : ℝ) (hH : 0 < H) (hΔ : 0 < Δ)
       (g : I → J → V → ℝ)
       (hLip : ∀ i a, ∀ u v, |g i a u - g i a v| ≤ L*d u v)
       (hHeight : ∀ i a v, |g i a v| ≤ H)
       (hzero : ∀ i a, ∀ v ∈ bag i, g i a v = 0) :
       let M := H*((Fintype.card ι : ℝ)-1)+2*Δ
   …

   Mentions: OAI.BoundedTreewidthL1.RootedForest

10. theorem OAI.BoundedTreewidthL1.AnchorTreeParticles.measurable_state line 135

    Source documentation

    Measurability of the actual branching preparation, with all randomness sampled beforehand. No measurable-choice assumption about the particle lists.

    theorem measurable_state (R : RootedForest I) (bag : I → Finset V) (A : I → Finset J)
        (g : Ω → I → J → V → ℝ)
        (hg : ∀ i a v, Measurable (fun ω => g ω i a v)) (i : I) :
        Measurable (fun ω => state (ι := ι) R bag A (g ω) i) := by
    …

    Mentions: OAI.BoundedTreewidthL1.RootedForest, OAI.BoundedTreewidthL1.AnchorTreeParticles.state

11. def OAI.BoundedTreewidthL1.AnchorTreeParticles.origin line 155

    Source documentation

    The discrete launch location depends only on the rooted decomposition and active keys. In particular it does not consult any preparatory randomness.

    noncomputable def origin (R : RootedForest I) (A : I → Finset J) (root : I) : I → J → I :=
    …

    Mentions: OAI.BoundedTreewidthL1.RootedForest

12. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.origin_eq line 158
13. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.origin_fresh line 164
14. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.origin_transport line 180
15. lemma OAI.BoundedTreewidthL1.AnchorTreeParticles.two_particle_difference line 205
16. theorem OAI.BoundedTreewidthL1.AnchorTreeParticles.origin_particle_gap line 224

    Source documentation

    The actual active pair at any descendant supplies the original launch separation. The origin is deterministic, so no conditioning on the particle scheduler or sampled coefficients is required.

    theorem origin_particle_gap (R : RootedForest I) (root : I) (bag : I → Finset V)
        (A : I → Finset J) (k q : ℕ) (hbag : ∀ i, (bag i).card ≤ k)
        (hA : ∀ i, (A i).card ≤ q) (hN : Fintype.card ι = 2*q + k.factorial + 2)
        (d : V → V → ℝ) (L H Δ : ℝ) (hH : 0 < H) (hΔ : 0 < Δ)
        (g : I → J → V → ℝ)
        (hLip : ∀ i a, ∀ u v, |g i a u - g i a v| ≤ L*d u v)
        (hHeight : ∀ i a v, |g i a v| ≤ H)
        (hzero : ∀ i a, ∀ v ∈ bag i, g i a v = 0)
        (i : I) (a : J) (ha : a ∈ A i) (u v : V) :
        2*|g (origin R A root i a) a u - g (origin R A root i a) a v| ≤
          ∑ t, |(state (ι := ι) R bag A g i).1 t u -
    …

    Mentions: OAI.BoundedTreewidthL1.RootedForest, OAI.BoundedTreewidthL1.AnchorTreeParticles.origin, OAI.BoundedTreewidthL1.AnchorTreeParticles.state

17. theorem OAI.BoundedTreewidthL1.AnchorTreeParticles.averaged_origin_realization line 264

    Source documentation

    Actual global averaged L1 realization of the branching preparation, with an unconditional integral lower bound from each deterministic active origin.

    theorem averaged_origin_realization
        (G : SimpleGraph V) (hG : G.Connected) (ℓ : G.edgeSet → ℝ) (hℓ : ∀ e, 0 < ℓ e)
        (T : SimpleGraph I) (hT : T.IsTree) (root : I) (B : I → Finset V)
        (hcover : ∀ v, ∃ i, v ∈ B i)
        (hedge : ∀ u v, G.Adj u v → ∃ i, u ∈ B i ∧ v ∈ B i)
        (hrun : ∀ v, (T.induce {i | v ∈ B i}).Preconnected)
        (A : I → Finset J) (k q : ℕ) (hbag : ∀ i, (B i).card ≤ k)
        (hA : ∀ i, (A i).card ≤ q) (hN : Fintype.card ι = 2*q + k.factorial + 2)
        (ν : Measure Ω) [IsProbabilityMeasure ν]
        (L H Δ : ℝ) (hL : 0 < L) (hH : 0 < H) (hΔ : 0 < Δ)
        (g : Ω → I → J → V → ℝ) (hmeas : ∀ i a v, Measurable (fun ω => g ω i a v))
        (hLip : ∀ ω i a, ∀ u v, |g ω i a u - g ω i a v| ≤ L*shortestPathDistance G ℓ u v)
    …

    Mentions: OAI.BoundedTreewidthL1.shortestPathDistance

18. lemma OAI.BoundedTreewidthL1.tree_path_mem_connected line 342
19. lemma OAI.BoundedTreewidthL1.touched_bags_connected line 358

    Source documentation

    The bags touched by the vertices of a graph walk form a connected subtree. No bounded-width assumption is needed for this purely combinatorial fact.

    lemma touched_bags_connected {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)
        {u v : V} (p : G.Walk u v) :
        (T.induce {t | ∃ z ∈ p.support, z ∈ bag t}).Connected := by
    …

20. theorem OAI.BoundedTreewidthL1.bag_separator line 390
21. def OAI.BoundedTreewidthL1.bagDistance line 406

    Source documentation

    Exact finite minimum distance to a nonempty bag in the original weighted metric.

    noncomputable def bagDistance {V : Type*} (G : SimpleGraph V) (ℓ : G.edgeSet → ℝ)
        (A : Finset V) (hA : A.Nonempty) (x : V) : ℝ :=
    …

22. lemma OAI.BoundedTreewidthL1.bagDistance_attained line 410
23. lemma OAI.BoundedTreewidthL1.bagDistance_le line 415
24. lemma OAI.BoundedTreewidthL1.bagDistance_nonneg line 420
25. lemma OAI.BoundedTreewidthL1.bagDistance_triangle line 425
26. lemma OAI.BoundedTreewidthL1.bagDistance_lipschitz line 433
27. lemma OAI.BoundedTreewidthL1.geodesic_split line 442
28. theorem OAI.BoundedTreewidthL1.separator_bag_geometry line 455
29. def OAI.BoundedTreewidthL1.AnchorCache.Drop line 490

    Source documentation

    Immediately follows a strict-to-weak threshold drop in the age-ordered list.

    def Drop (C : Finset ℕ) (v : ℕ → ℝ) (τ : ℝ) (a : ℕ) : Prop :=
    …

30. def OAI.BoundedTreewidthL1.AnchorCache.protectedEntries line 494
31. def OAI.BoundedTreewidthL1.AnchorCache.cacheBound line 501
32. def OAI.BoundedTreewidthL1.AnchorCache.eligible line 503
33. def OAI.BoundedTreewidthL1.AnchorCache.trim line 510

    Source documentation

    Retain the inclusive list if space remains; otherwise evict its oldest unprotected nonroot entry. The fallback is unreachable on admissible input.

    noncomputable def trim (k : ℕ) (P : Finset V) (C : Finset ℕ)
        (d : V → V → ℝ) (v : V → ℕ → ℝ) (J : ℝ) : Finset ℕ := by
    …

34. lemma OAI.BoundedTreewidthL1.AnchorCache.drop_unique line 518
35. lemma OAI.BoundedTreewidthL1.AnchorCache.drop_card_le line 530
36. lemma OAI.BoundedTreewidthL1.AnchorCache.protected_subset line 539
37. lemma OAI.BoundedTreewidthL1.AnchorCache.protected_card line 552
38. lemma OAI.BoundedTreewidthL1.AnchorCache.eligible_nonempty line 577
39. theorem OAI.BoundedTreewidthL1.AnchorCache.deterministic_cache_step line 600
40. def OAI.BoundedTreewidthL1.AnchorCache.memory line 637
41. def OAI.BoundedTreewidthL1.AnchorCache.inclusiveCache line 643

    Source documentation

    Incoming cache plus current proposal, before the release at this bag.

    noncomputable def inclusiveCache (k : ℕ) (P : ℕ → Finset V) (d : V → V → ℝ)
        (v : ℕ → V → ℕ → ℝ) (J : ℝ) : ℕ → Finset ℕ
      | 0 => {0}
      | t+1 => insert (t+1) (memory k P d v J t)

    Mentions: OAI.BoundedTreewidthL1.AnchorCache.memory

42. def OAI.BoundedTreewidthL1.AnchorCache.ValidInput line 648
43. lemma OAI.BoundedTreewidthL1.AnchorCache.trim_subset line 654
44. lemma OAI.BoundedTreewidthL1.AnchorCache.trim_removed_unique line 660
45. lemma OAI.BoundedTreewidthL1.AnchorCache.memory_subset line 674
46. lemma OAI.BoundedTreewidthL1.AnchorCache.inclusive_self line 681
47. lemma OAI.BoundedTreewidthL1.AnchorCache.inclusive_age line 685
48. lemma OAI.BoundedTreewidthL1.AnchorCache.inclusive_backwards line 697
49. lemma OAI.BoundedTreewidthL1.AnchorCache.memory_invariant line 714
50. lemma OAI.BoundedTreewidthL1.AnchorCache.inclusive_invariant line 730
51. lemma OAI.BoundedTreewidthL1.AnchorCache.memory_protected line 742
52. def OAI.BoundedTreewidthL1.AnchorCache.activeTimes line 754
53. def OAI.BoundedTreewidthL1.AnchorCache.lastActive line 759
54. lemma OAI.BoundedTreewidthL1.AnchorCache.active_self line 765
55. lemma OAI.BoundedTreewidthL1.AnchorCache.lastActive_mem line 771
56. lemma OAI.BoundedTreewidthL1.AnchorCache.le_lastActive line 779
57. lemma OAI.BoundedTreewidthL1.AnchorCache.inclusive_iff_interval line 787
58. theorem OAI.BoundedTreewidthL1.AnchorCache.cache_program_realizes line 801

    Source documentation

    Realizes the deterministic cache as the inclusive reservation path needed by the youngest-crossing argument.

    theorem cache_program_realizes (k : ℕ) (P : ℕ → Finset V) (d : V → V → ℝ)
        (v : ℕ → V → ℕ → ℝ) (J : ℝ) (last : ℕ)
        (hvalid : ValidInput k P d v J last) :
        ∃ R : BoundedTreewidthL1.ReservationPath, R.last = last ∧
          (∀ t ≤ last, R.inclusive t = inclusiveCache k P d v J t) ∧
          (∀ t, (R.inclusive t).card ≤ cacheBound k + 1) ∧
          (∀ t < last, ∀ a ∈ protectedEntries (P t) (inclusiveCache k P d v J t) d (v t) J,
            t < R.finish a)
     := by
    …

    Mentions: OAI.BoundedTreewidthL1.AnchorCache.ValidInput, OAI.BoundedTreewidthL1.ReservationPath, OAI.BoundedTreewidthL1.AnchorCache.inclusiveCache, OAI.BoundedTreewidthL1.AnchorCache.cacheBound, OAI.BoundedTreewidthL1.AnchorCache.protectedEntries

59. theorem OAI.BoundedTreewidthL1.AnchorCache.graph_cache_realizes line 863
60. lemma OAI.BoundedTreewidthL1.AnchorCache.drop_congr_on line 899
61. lemma OAI.BoundedTreewidthL1.AnchorCache.protected_congr_on line 909
62. lemma OAI.BoundedTreewidthL1.AnchorCache.trim_congr_on line 925
63. lemma OAI.BoundedTreewidthL1.AnchorCache.memory_prefix line 933
64. lemma OAI.BoundedTreewidthL1.AnchorCache.inclusiveCache_prefix line 948
65. def OAI.BoundedTreewidthL1.RootedTree.downPath line 965
66. lemma OAI.BoundedTreewidthL1.RootedTree.downPath_isPath line 966
67. lemma OAI.BoundedTreewidthL1.RootedTree.downPath_length line 968
68. lemma OAI.BoundedTreewidthL1.RootedTree.depth_parent line 971
69. lemma OAI.BoundedTreewidthL1.RootedTree.path_parent line 981
70. lemma OAI.BoundedTreewidthL1.RootedTree.downPath_parent_getVert line 989
71. def OAI.BoundedTreewidthL1.TreeCache.bags line 1005
72. def OAI.BoundedTreewidthL1.TreeCache.heights line 1007
73. def OAI.BoundedTreewidthL1.TreeCache.inclusive line 1009
74. def OAI.BoundedTreewidthL1.TreeCache.released line 1012
75. def OAI.BoundedTreewidthL1.TreeCache.active line 1015
76. def OAI.BoundedTreewidthL1.TreeCache.retained line 1018
77. lemma OAI.BoundedTreewidthL1.TreeCache.inclusive_parent line 1022
78. lemma OAI.BoundedTreewidthL1.TreeCache.active_parent line 1039
79. lemma OAI.BoundedTreewidthL1.TreeCache.retained_subset line 1055
80. lemma OAI.BoundedTreewidthL1.TreeCache.child_not_active line 1060
81. lemma OAI.BoundedTreewidthL1.TreeCache.active_root line 1086
82. lemma OAI.BoundedTreewidthL1.TreeCache.active_inter_parent line 1092
83. lemma OAI.BoundedTreewidthL1.TreeCache.active_sdiff_parent line 1107
84. theorem OAI.BoundedTreewidthL1.TreeCache.graph_active_bound line 1122

    Source documentation

    Width-only cache capacity on the actual root-to-node paths.

    theorem graph_active_bound [Fintype V] [DecidableEq V]
        (G : SimpleGraph V) (ℓ : G.edgeSet → ℝ) (hG : G.Connected) (hℓ : ∀ e, 0 < ℓ e)
        (T : SimpleGraph I) (B : I → Finset V) (hne : ∀ i, (B i).Nonempty)
        (hT : T.IsTree) (root : I)
        (hedge : ∀ u v, G.Adj u v → ∃ t, u ∈ B t ∧ v ∈ B t)
        (hocc : ∀ v, (T.induce {t | v ∈ B t}).Connected)
        (k : ℕ) (hcard : ∀ i, (B i).card ≤ k) (J : ℝ) (i : I) :
        (active T hT root B (fun a => bagDistance G ℓ (B a) (hne a)) k
          (shortestPathDistance G ℓ) J i).card ≤ cacheBound k + 1 := by
    …

    Mentions: OAI.BoundedTreewidthL1.TreeCache.active, OAI.BoundedTreewidthL1.bagDistance, OAI.BoundedTreewidthL1.shortestPathDistance