OAI/Analysis/IntegralMeans/Winding.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.HasLogIncrement.path_trans line 21
  2. lemma OAI.Brennan.HasLogIncrement.path_symm line 46
  3. lemma OAI.Brennan.exists_path_logIncrement line 55
  4. lemma OAI.Brennan.HasLogIncrement.of_slit line 63
  5. lemma OAI.Brennan.HasLogIncrement.of_neg_slit line 69
  6. lemma OAI.Brennan.log_neg_of_im_neg line 81
  7. lemma OAI.Brennan.log_neg_of_im_pos line 87
  8. def OAI.Brennan.rectPath line 93
  9. lemma OAI.Brennan.rectPath_logIncrement line 100
  10. lemma OAI.Brennan.rectPath_winding line 149
  11. lemma OAI.Brennan.windingNumber_path_symm line 154
  12. lemma OAI.Brennan.windingNumber_four_paths line 162
  13. lemma OAI.Brennan.windingNumber_rect_map line 180
  14. lemma OAI.Brennan.transverse_hasFDerivAt line 240
  15. lemma OAI.Brennan.det_transverse_pos line 253
  16. lemma OAI.Brennan.periodic_simple_zero line 259
  17. lemma OAI.Brennan.transverse_unique_zero_strip line 268
  18. def OAI.Brennan.rectRegion line 326
  19. lemma OAI.Brennan.convex_rectRegion line 328
  20. lemma OAI.Brennan.rectPath_mem line 337
  21. lemma OAI.Brennan.rectPath_ne_zero line 358
  22. lemma OAI.Brennan.winding_jump_centred line 363