OAI/Combinatorics/TreewidthL1/AnchorEmbedding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreewidthL1.AnchorExperiment.graphPath line 18
2. def OAI.BoundedTreewidthL1.AnchorExperiment.PathGeometry.track line 74
3. lemma OAI.BoundedTreewidthL1.AnchorExperiment.PathGeometry.lower_of_track line 115
4. theorem OAI.BoundedTreewidthL1.AnchorExperiment.test_parameters_exist line 136
5. lemma OAI.BoundedTreewidthL1.AnchorExperiment.Model.join_lower line 196
6. theorem OAI.BoundedTreewidthL1.AnchorExperiment.anchor_common_bag_embedding line 241

   Source documentation

   The constructed anchor ensemble controls BOTH distances to one actual common bag. This is enough for all-pairs lower comparison when combined with co-bag separation, and involves no assumed contraction/Markov-flow theorem.

   theorem anchor_common_bag_embedding (k : ℕ) (hk : 2 ≤ k) :
       ∃ U c : ℝ, 0 < U ∧ 0 < c ∧
       ∀ (V : Type) [Fintype V] [DecidableEq V] [Nontrivial V]
         (G : SimpleGraph V) (_ : G.Connected) (ℓ : G.edgeSet → ℝ) (_ : ∀ e, 0 < ℓ e)
         (n : ℕ) (T : SimpleGraph (Fin (n+1))) (_ : T.IsTree) (_ : Fin (n+1))
         (B : Fin (n+1) → Finset V) (hne : ∀ i, (B i).Nonempty)
         (_ : ∀ v, ∃ i, v ∈ B i)
         (_ : ∀ u v, G.Adj u v → ∃ i, u ∈ B i ∧ v ∈ B i)
         (_ : ∀ v, (T.induce {i | v ∈ B i}).Connected)
         (_ : ∀ i, (B i).card ≤ k),
         ∃ m : ℕ, ∃ Φ : V → PiLp (1 : ENNReal) (fun _ : Fin m => ℝ),
           (∀ x y, ‖Φ x-Φ y‖ ≤ U*shortestPathDistance G ℓ x y) ∧
   …

   Mentions: OAI.BoundedTreewidthL1.shortestPathDistance