OAI/NumberTheory/Ostmann/Tree/ReciprocalDiagonal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The diagonal average is an affine correlation

The substitution r = lam - 1/d turns the weighted bottom-pair diagonal into the affine averaging operator applied to the reciprocal twist.

  1. theorem OAI.Ostmann.fieldBottomPair_eq_bottomPairValue line 18
  2. theorem OAI.Ostmann.mellinDiagonal_reciprocal line 27