OAI/NumberTheory/Ostmann/Tree/ProductFibers.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform product fibers for pairs and quartets

These explicit bijections justify exposing a component product and then using independent coordinates on its fiber in the tree comparison.

  1. def OAI.Ostmann.fixedProductPairEquiv line 21
  2. def OAI.Ostmann.fixedProductQuartetEquiv line 35
  3. theorem OAI.Ostmann.card_fixedProductPair line 57
  4. theorem OAI.Ostmann.card_fixedProductQuartet line 61
  5. theorem OAI.Ostmann.sum_fixedProductPair line 68

    Source documentation

    Uniform sampling of a fixed pair product leaves one free group coordinate.

    theorem sum_fixedProductPair {G R : Type*} [CommGroup G] [Fintype G] [DecidableEq G]
    [AddCommMonoid R] (P : G) (f : G × G → R) :
    (∑ xy : {xy : G × G // xy.1 * xy.2 = P}, f xy.1) = ∑ x : G, f (x, P / x) := by
…
  6. theorem OAI.Ostmann.sum_fixedProductQuartet line 74

    Source documentation

    A fixed quartet product leaves three independent free coordinates.

    theorem sum_fixedProductQuartet {G R : Type*} [CommGroup G] [Fintype G] [DecidableEq G]
    [AddCommMonoid R] (P : G) (f : G × (G × (G × G)) → R) :
    (∑ m : {m : G × (G × (G × G)) // m.1 * m.2.1 * m.2.2.1 * m.2.2.2 = P}, f m.1) =
      ∑ x : G, ∑ y : G, ∑ z : G, f (x, y, z, P / (x * y * z)) := by
…