OAI/Geometry/HyperbolicGroups/Distinct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.FiniteLaw.map_uniform_equiv line 18
  2. def OAI.HyperbolicObstruction.FiniteLaw.embeddingSubtypeEquiv line 31
  3. lemma OAI.HyperbolicObstruction.FiniteLaw.distinct_tv line 37
  4. theorem OAI.HyperbolicObstruction.FiniteLaw.distinct_error_tendsto line 58

    Source documentation

    Distinct sampling and iid sampling have vanishing TV distance at each fixed number of leaves. This uses the exact falling-factorial ratio.

    theorem distinct_error_tendsto (t : ℕ) :
    Tendsto (fun N : ℕ => 1 - ((N.descFactorial t : ℕ) : ℝ) / (N : ℝ) ^ t) atTop (𝓝 0) := by
…