OAI/NumberTheory/PiExponent/Analysis/FlintSine.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.sin_nat_ne_zero line 12
  2. def OAI.PiExponent.sineGroup line 19
  3. theorem OAI.PiExponent.round_div_pi_nonneg line 21
  4. theorem OAI.PiExponent.sineGroup_cast line 28
  5. theorem OAI.PiExponent.sineGroup_distance line 32
  6. theorem OAI.PiExponent.sineGroup_pos line 46
  7. theorem OAI.PiExponent.sineGroup_lower line 56
  8. theorem OAI.PiExponent.abs_sin_lower_integerDistance line 62
  9. theorem OAI.PiExponent.sineGroup_residue_injective line 74
  10. theorem OAI.PiExponent.flint_term_le_distance_term line 88
  11. theorem OAI.PiExponent.summable_sineGroup_comp line 128
  12. theorem OAI.PiExponent.flintHills_summable_of_distance_summable line 138
  13. theorem OAI.PiExponent.flintHills_positive_summable_of_distance_summable line 151