OAI/Geometry/HyperbolicGroups/PlanarFacePartition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.PictureSwitch.uniform_genusZero_face_partition line 17

   Source documentation

   Dual form of the proved genus-zero partition theorem, with literal selected face classes and the original map's unordered edge-copy cuts.

   theorem uniform_genusZero_face_partition (d : ℕ) (eta : ℝ) (heta : 0 < eta) :
       ∃ K : ℕ, 0 < K ∧ ∀ (D : Type u) [Fintype D] [DecidableEq D] (M : PictureMap D),
         M.GenusZero → ∀ U : Finset (Quotient (SameCycle.setoid M.face)),
         (∀ v ∈ U, Nat.card {x : D // Quotient.mk (SameCycle.setoid M.face) x = v} ≤ d) →
         ∃ (I : Type) (_ : Fintype I) (part : Quotient (SameCycle.setoid M.face) → I),
           (∀ i, (U.filter (fun x => part x = i)).card ≤ K) ∧
           (Fintype.card (RelativeCutContact M
             (fun x => Quotient.mk (SameCycle.setoid M.face) x ∈ U)
             (part ∘ Quotient.mk (SameCycle.setoid M.face))) : ℝ) ≤ eta * U.card := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap, OAI.HyperbolicObstruction.PictureSwitch.RelativeCutContact