OAI/Geometry/HyperbolicGroups/Deviation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.StarModel.branchDeviation line 19
2. def OAI.HyperbolicObstruction.StarModel.leafDeviation line 24
3. lemma OAI.HyperbolicObstruction.StarModel.branchDeviation_nonneg line 29
4. lemma OAI.HyperbolicObstruction.StarModel.leafDeviation_nonneg line 36
5. theorem OAI.HyperbolicObstruction.StarModel.expect_branchDeviation line 42

   Source documentation

   Summing the conditional first-moment bounds costs the expected number of master matches, not the number of all assignments without its match factor.

   theorem expect_branchDeviation (support : R → Finset F) (U : Finset F) (j : B)
       (p : R → ℝ) (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1) (ξ : Var (B := B) U → A)
   …

   Mentions: OAI.HyperbolicObstruction.StarModel.Var

6. theorem OAI.HyperbolicObstruction.StarModel.expect_leafDeviation line 77

   Source documentation

   The corresponding unconditional L1 bound for ordered-distinct leaf lists.

   theorem expect_leafDeviation (support : R → Finset F) (U : Finset F) (e : F)
       (p : R → ℝ) (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1) (ξ : Var (B := B) U → A)
   …

   Mentions: OAI.HyperbolicObstruction.StarModel.Var