OAI/Geometry/HyperbolicGroups/ExtensionConditioning.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.StarModel.residual_ne_branch line 19
2. lemma OAI.HyperbolicObstruction.StarModel.extension_depends line 42
3. theorem OAI.HyperbolicObstruction.StarModel.extension_conditioning line 61

   Source documentation

   The entire law of the residual extension count is unchanged by conditioning on the fixed branch being an actual match.

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

   Mentions: OAI.HyperbolicObstruction.StarModel.Var

4. lemma OAI.HyperbolicObstruction.StarModel.leaf_expect line 79
5. lemma OAI.HyperbolicObstruction.StarModel.extension_expect line 89
6. lemma OAI.HyperbolicObstruction.StarModel.leaf_expect_eq line 99
7. lemma OAI.HyperbolicObstruction.StarModel.extension_expect_eq line 107