OAI/NumberTheory/Ostmann/Tree/BottomPairCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinates for a bottom pair of the finite-field tree

The change of variables in §6 sends (d,t) to (dt/(t-1),d/(t-1)). On its valid domain this is a bijection with the ordered distinct nonzero pairs. It is the change of variables used in the bottom-pair second moment.

  1. def OAI.Ostmann.ValidPairCoordinates line 19
  2. def OAI.Ostmann.DistinctNonzeroPair line 22
  3. theorem OAI.Ostmann.pair_coordinate_difference line 25
  4. theorem OAI.Ostmann.pair_coordinate_ratio line 30
  5. theorem OAI.Ostmann.pair_coordinates_reconstruct line 35
  6. def OAI.Ostmann.pairCoordinatesEquiv line 48

    Source documentation

    The difference and ratio coordinates parametrize exactly the ordered distinct nonzero pairs.

    noncomputable def pairCoordinatesEquiv (K : Type*) [Field K] :
    ValidPairCoordinates K ≃ DistinctNonzeroPair K where
…

    Mentions: OAI.Ostmann.ValidPairCoordinates, OAI.Ostmann.DistinctNonzeroPair