OAI/NumberTheory/Ostmann/Quadratic/QuadraticGrowthCorrectionBands.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Original low and high correction bands from the actual growth matrices

  1. def OAI.Ostmann.quadraticLowCorrectionBand line 13
  2. def OAI.Ostmann.quadraticHighCorrectionBand line 20
  3. def OAI.Ostmann.quadraticCorrectionGrowthScale line 27
  4. theorem OAI.Ostmann.quadratic_low_band_growth line 34