OAI/Analysis/PlanarPacking/BarrierProduct.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpPlanar.logSin_hasDeriv line 13
  2. lemma OAI.SharpPlanar.cot_scaled_hasDeriv line 19
  3. lemma OAI.SharpPlanar.logSin_concaveOn line 30
  4. lemma OAI.SharpPlanar.sinc_ne_zero line 44
  5. lemma OAI.SharpPlanar.logSinc_hasDeriv line 51
  6. lemma OAI.SharpPlanar.logSinc_deriv_hasDeriv line 66
  7. lemma OAI.SharpPlanar.logSinc_concaveOn line 77
  8. def OAI.SharpPlanar.dividedP line 108
  9. lemma OAI.SharpPlanar.dividedP_zero line 112
  10. lemma OAI.SharpPlanar.dividedP_factor line 115
  11. lemma OAI.SharpPlanar.sine_twelfth_ne line 127
  12. def OAI.SharpPlanar.leftHalf line 134
  13. def OAI.SharpPlanar.rightHalf line 136
  14. lemma OAI.SharpPlanar.half_pos line 139
  15. lemma OAI.SharpPlanar.half_bounds line 142
  16. lemma OAI.SharpPlanar.other_sine_ne line 147
  17. lemma OAI.SharpPlanar.dividedP_pos line 159
  18. lemma OAI.SharpPlanar.dividedP_log line 171
  19. lemma OAI.SharpPlanar.concaveOn_finset_sum line 200
  20. lemma OAI.SharpPlanar.dividedP_log_concave line 210
  21. lemma OAI.SharpPlanar.lower_of_log_concave line 240