OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Tent.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryLogIntegral.tent line 12
  2. lemma OAI.OrdinaryLogIntegral.tent_nonneg line 14
  3. lemma OAI.OrdinaryLogIntegral.tent_le_one line 16
  4. lemma OAI.OrdinaryLogIntegral.tent_zero_left line 20
  5. lemma OAI.OrdinaryLogIntegral.tent_zero_right line 27
  6. lemma OAI.OrdinaryLogIntegral.tent_rising line 34
  7. lemma OAI.OrdinaryLogIntegral.tent_falling line 41
  8. lemma OAI.OrdinaryLogIntegral.tent_lipschitz line 48
  9. lemma OAI.OrdinaryLogIntegral.logPhase_lipschitz line 61
  10. def OAI.OrdinaryLogIntegral.tentPhase line 74
  11. lemma OAI.OrdinaryLogIntegral.tentPhase_norm line 77
  12. lemma OAI.OrdinaryLogIntegral.tentPhase_zero_left line 81
  13. lemma OAI.OrdinaryLogIntegral.tentPhase_zero_right line 84
  14. lemma OAI.OrdinaryLogIntegral.tentPhase_lipschitz line 87
  15. lemma OAI.OrdinaryLogIntegral.tentPhase_continuous line 112