OAI/NumberTheory/Ostmann/Tree/CrossQuartetFiber.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.pairOrient line 14
2. def OAI.Ostmann.quartetOrient line 17
3. theorem OAI.Ostmann.pairOrient_product line 20
4. def OAI.Ostmann.quartetOrientFiberEquiv line 24
5. theorem OAI.Ostmann.fourth_of_product line 43
6. def OAI.Ostmann.friendlyQuartetFiberEquiv line 53

   Source documentation

   The held coordinates and the inverse first free coordinate parametrize one quartet product fiber without changing its uniform measure.

   noncomputable def friendlyQuartetFiberEquiv {U : Type*} [CommGroup U] (P : U) :
       TreeLeafFiber U 2 P ≃ U × (U × U) where
   …

   Mentions: OAI.Ostmann.TreeLeafFiber

7. def OAI.Ostmann.crossQuartetFiberEquiv line 69
8. theorem OAI.Ostmann.crossQuartetFiberEquiv_symm line 73
9. theorem OAI.Ostmann.sum_crossQuartetFiber line 80

   Source documentation

   This is the actual uniform product-fiber measure used by the cycle proof.

   theorem sum_crossQuartetFiber {U R : Type*} [CommGroup U] [Fintype U] [DecidableEq U]
       [AddCommMonoid R] (left right : Bool) (P : U) (f : TreeLeafTuple U 2 → R) :
       (∑ m : TreeLeafFiber U 2 P, f m.1) =
         ∑ a : U, ∑ b : U, ∑ r : U, f (crossQuartetLeaves left right P a b r) := by
   …

   Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.crossQuartetLeaves

10. theorem OAI.Ostmann.mean_crossQuartetFiber line 89