OAI/Geometry/HyperbolicGroups/StarCoupling.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.StarModel.toConditional line 21

   Source documentation

   Forgetting the auxiliary injectivity retains an actual conditional star of master matches. Its common tuple is named by I.

   def toConditional (support : R → Finset F) (U I : Finset F) (hI : I ⊆ U)
       (w : TableModel.Entry (A := A) support → Bool) (z : Stars (B := Fin (k+1)) support U w) :
   …

   Mentions: OAI.HyperbolicObstruction.TableModel.Entry, OAI.HyperbolicObstruction.StarModel.Stars

2. def OAI.HyperbolicObstruction.StarModel.coupling line 29
3. lemma OAI.HyperbolicObstruction.StarModel.coupling_branch line 35
4. lemma OAI.HyperbolicObstruction.StarModel.coupling_branch_bound line 43
5. lemma OAI.HyperbolicObstruction.StarModel.coupling_leaves line 53
6. lemma OAI.HyperbolicObstruction.StarModel.leaf_distribution_bound line 62
7. lemma OAI.HyperbolicObstruction.StarModel.coupling_leaves_bound line 81

   Source documentation

   Both quantitative conclusions of the deterministic normalization lemma. The last term is solely the distinct-versus-iid error; no conditional independence from the common tuple has been assumed.

   lemma coupling_leaves_bound (support : R → Finset F) (U I : Finset F) (hI : I ⊆ U)
       (e : F) (he : e ∉ U) (w : TableModel.Entry (A := A) support → Bool)
   …

   Mentions: OAI.HyperbolicObstruction.TableModel.Entry