OAI/Geometry/HyperbolicGroups/FiberLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.FiniteLaw.uniform_map_mass line 16
2. lemma OAI.HyperbolicObstruction.FiniteLaw.card_fibers line 28
3. lemma OAI.HyperbolicObstruction.FiniteLaw.uniform_map_eq_normalize line 33
4. lemma OAI.HyperbolicObstruction.FiniteLaw.uniform_map_bound line 41
5. lemma OAI.HyperbolicObstruction.FiniteLaw.uniform_subtype_tv line 51

   Source documentation

   The uniform law on a subset, included in the ambient finite set, differs from the ambient uniform law by exactly the proportion excluded.

   lemma uniform_subtype_tv [Nonempty α] (P : α → Prop) [DecidablePred P] [Nonempty {a // P a}] :
       ((uniform : FiniteLaw {a // P a}).map Subtype.val).totalVariation (uniform : FiniteLaw α) =
         1 - (Fintype.card {a // P a} : ℝ) / Fintype.card α := by
   …

   Mentions: OAI.HyperbolicObstruction.FiniteLaw.uniform, OAI.HyperbolicObstruction.FiniteLaw, OAI.HyperbolicObstruction.FiniteLaw.map, OAI.HyperbolicObstruction.FiniteLaw.totalVariation