OAI/NumberTheory/Ostmann/Characters/DiagonalEstimateSourceDefs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Characters.DiagonalEstimate.sourceScheduledShells line 23
  2. theorem OAI.Ostmann.Characters.DiagonalEstimate.sourceScheduledShells_pos line 27
  3. abbrev OAI.Ostmann.Characters.DiagonalEstimate.sourceScheduledUnits line 32
  4. abbrev OAI.Ostmann.Characters.DiagonalEstimate.sourceScheduledCharacters line 37
  5. abbrev OAI.Ostmann.Characters.DiagonalEstimate.sourceScheduledCenters line 42
  6. def OAI.Ostmann.Characters.DiagonalEstimate.sourcePivotRanges line 47
  7. def OAI.Ostmann.Characters.DiagonalEstimate.sourceMatchingAverage line 50
  8. def OAI.Ostmann.Characters.DiagonalEstimate.sourcePreservingAverage line 63
  9. def OAI.Ostmann.Characters.DiagonalEstimate.sourceChangingAverage line 66
  10. abbrev OAI.Ostmann.Characters.DiagonalEstimate.sourceUnitDiagonal line 69
  11. theorem OAI.Ostmann.Characters.DiagonalEstimate.sourceUnitDiagonal_partition line 80