OAI/Combinatorics/TreewidthL1/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundedTreewidthL1.nonempty_tree_decomposition line 11

   Source documentation

   Removing empty bags preserves the exact tree-decomposition hypotheses. The graph is only required to be nonempty and connected; no extra metric hypothesis enters this combinatorial reduction.

   theorem nonempty_tree_decomposition [Fintype V] [DecidableEq V] [Nonempty V]
       (hG : G.Connected) (k : ℕ) (hdec : HasTreeDecomposition G k) :
       ∃ n : ℕ, ∃ T : SimpleGraph (Fin n), ∃ bag : Fin n → Finset V,
         T.IsTree ∧
         (∀ v : V, ∃ t, v ∈ bag t) ∧
         (∀ u v : V, G.Adj u v → ∃ t, u ∈ bag t ∧ v ∈ bag t) ∧
         (∀ v : V, (T.induce {t | v ∈ bag t}).Connected) ∧
         (∀ t, (bag t).card ≤ k) ∧ (∀ t, (bag t).Nonempty) := by
   …

   Mentions: OAI.BoundedTreewidthL1.HasTreeDecomposition

2. def OAI.BoundedTreewidthL1.l1Append line 70

   Source documentation

   Direct sum of two finite real L1 vectors, with the sum norm (not the maximum norm on an ordinary product).

   def l1Append {m n : ℕ} (x : PiLp (1 : ENNReal) (fun _ : Fin m => ℝ))
       (y : PiLp (1 : ENNReal) (fun _ : Fin n => ℝ)) :
       PiLp (1 : ENNReal) (fun _ : Fin (m+n) => ℝ) :=
   …

3. lemma OAI.BoundedTreewidthL1.l1Append_norm_sub line 75
4. lemma OAI.BoundedTreewidthL1.common_bag_comparison line 85

   Source documentation

   The final purely metric bridge: a common-bag bound on both endpoints and co-bag separation imply a global all-pairs lower comparison.

   lemma common_bag_comparison {V : Type*} [Fintype V] [DecidableEq V]
       (G : SimpleGraph V) (hG : G.Connected) (ℓ : G.edgeSet → ℝ) (hℓ : ∀ e, 0 < ℓ e)
       {I : Type*} (B : I → Finset V) (hne : ∀ i, (B i).Nonempty)
       {m n : ℕ} (Φ : V → PiLp (1 : ENNReal) (fun _ : Fin m => ℝ))
       (Ψ : V → PiLp (1 : ENNReal) (fun _ : Fin n => ℝ))
       (U c a : ℝ) (hU : 0 ≤ U) (hc : 0 < c) (ha : 0 < a)
       (hupper : ∀ x y, ‖Ψ x-Ψ y‖ ≤ U*shortestPathDistance G ℓ x y)
       (hcobag : ∀ i x y, x ∈ B i → y ∈ B i →
         c*shortestPathDistance G ℓ x y ≤ ‖Ψ x-Ψ y‖)
       (hanchor : ∀ x y, ∃ i, a*bagDistance G ℓ (B i) (hne i) x ≤ ‖Φ x-Φ y‖ ∧
         a*bagDistance G ℓ (B i) (hne i) y ≤ ‖Φ x-Φ y‖) (x y : V) :
       c*shortestPathDistance G ℓ x y ≤
   …

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

5. theorem OAI.BoundedTreewidthL1.main_theorem line 135

   Distinct definitions of this name: ComparatorChallenges/BoundedTreewidthL1.lean:43 (same statement text; different proof or body). Qualify references as OAI.BoundedTreewidthL1.main_theorem@path.