OAI/Geometry/HyperbolicGroups/LeafFiber.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.StarModel.leafValues line 19

   Source documentation

   A total extension of the specified distinct leaf values. The filler only occupies other field names and plays no part in the pinned statistic.

   def leafValues (U : Finset F) (b : B ↪ A) (a₀ : A) : Var (B := B) U → A
   …

   Mentions: OAI.HyperbolicObstruction.StarModel.Var

2. lemma OAI.HyperbolicObstruction.StarModel.leafValues_fieldwise line 25
3. lemma OAI.HyperbolicObstruction.StarModel.leaf_pin_fieldwise line 32
4. def OAI.HyperbolicObstruction.StarModel.starLeaves line 37
5. lemma OAI.HyperbolicObstruction.StarModel.leaves_eq_iff line 45
6. theorem OAI.HyperbolicObstruction.StarModel.card_leaf_fiber line 65

   Source documentation

   The leaf count is the exact fiber size of the uniform present-star law, not the count of a surrogate independently resampled star.

   theorem card_leaf_fiber (support : R → Finset F) (U : Finset F) (e : F) (he : e ∉ U)
       (w : TableModel.Entry (A := A) support → Bool) (b : B ↪ A) (a₀ : A) :
   …

   Mentions: OAI.HyperbolicObstruction.TableModel.Entry