OAI/NumberTheory/Ostmann/Quadratic/QuadraticPhaseContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative continuity of the original quadratic phase parameter

  1. theorem OAI.Ostmann.realAdditivePhase_sub_norm_le line 11
  2. theorem OAI.Ostmann.quadraticDensityTerm_phase_sub_bound line 24
  3. theorem OAI.Ostmann.positiveQuadraticSum_phase_sub_bound line 64