OAI/Combinatorics/TreewidthL1/Padding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoundedTreewidthL1.PaddedPartitions.Partition line 11

   Source documentation

   A partition is represented by its block-label map. The fibers are the blocks; using vertices as labels represents every partition of a finite nonempty vertex set. Unused labels impose no extra block condition.

   abbrev Partition (V : Type*) := V → V

2. def OAI.BoundedTreewidthL1.PaddedPartitions.BoundedDiameter line 14

   Source documentation

   Weak diameter, measured in the original weighted graph metric.

   def BoundedDiameter {V : Type*} (G : SimpleGraph V) (ℓ : G.edgeSet → ℝ)
       (r : ℝ) (P : Partition V) : Prop :=
   …

   Mentions: OAI.BoundedTreewidthL1.PaddedPartitions.Partition

3. def OAI.BoundedTreewidthL1.PaddedPartitions.PaddedAt line 19

   Source documentation

   The closed metric ball is contained in the block containing x.

   def PaddedAt {V : Type*} (G : SimpleGraph V) (ℓ : G.edgeSet → ℝ)
       (s : ℝ) (P : Partition V) (x : V) : Prop :=
   …

   Mentions: OAI.BoundedTreewidthL1.PaddedPartitions.Partition

4. def OAI.BoundedTreewidthL1.PaddedPartitions.paddingProbability line 23
5. def OAI.BoundedTreewidthL1.PaddedPartitions.UniformPaddedPartitions line 29
6. theorem OAI.BoundedTreewidthL1.PaddedPartitions.uniform_padded_partitions line 46