OAI/Geometry/HyperbolicGroups/Normalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.FiniteLaw.ext line 17
2. def OAI.HyperbolicObstruction.FiniteLaw.normalize line 25

   Source documentation

   Normalization of nonnegative counts. Positivity is proved before this construction is used to form the uniform present-star law.

   def normalize (f : α → ℝ) (hf : ∀ a, 0 ≤ f a) (hz : 0 < ∑ a, f a) : FiniteLaw α where
   …

   Mentions: OAI.HyperbolicObstruction.FiniteLaw

3. lemma OAI.HyperbolicObstruction.FiniteLaw.abs_sum_sub_const line 30
4. theorem OAI.HyperbolicObstruction.FiniteLaw.normalize_uniform_bound line 36

   Source documentation

   The exact deterministic normalization estimate for branch fibers and for ordered-distinct leaf fibers.

   theorem normalize_uniform_bound [Nonempty α] (f : α → ℝ) (hf : ∀ a, 0 ≤ f a)
       (hz : 0 < ∑ a, f a) (c : ℝ) :
       (normalize f hf hz).totalVariation uniform ≤ (∑ a, |f a - c|) / ∑ a, f a := by
   …

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

5. lemma OAI.HyperbolicObstruction.FiniteLaw.totalVariation_triangle line 63
6. lemma OAI.HyperbolicObstruction.FiniteLaw.totalVariation_map_le line 70
7. lemma OAI.HyperbolicObstruction.FiniteLaw.map_map line 88
8. lemma OAI.HyperbolicObstruction.FiniteLaw.expect_abs_sub_le_relative line 110