OAI/Analysis/IntegralMeans/LogIncrement.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.HasLogIncrement line 21
  2. lemma OAI.Brennan.HasLogIncrement.perturb line 24
  3. def OAI.Brennan.circleLoop line 48
  4. lemma OAI.Brennan.circleLoop_zero line 51
  5. lemma OAI.Brennan.circleLoop_one line 53
  6. lemma OAI.Brennan.norm_circleLoop line 56
  7. lemma OAI.Brennan.circleLoop_logIncrement line 59
  8. lemma OAI.Brennan.conj_circleLoop_logIncrement line 66
  9. def OAI.Brennan.linearPart line 78
  10. def OAI.Brennan.antiLinearPart line 80
  11. lemma OAI.Brennan.realLinear_decomposition line 82
  12. lemma OAI.Brennan.determinant_complex_real line 93
  13. lemma OAI.Brennan.det_eq_linearParts line 98
  14. lemma OAI.Brennan.linear_circle_logIncrement_pos line 108
  15. lemma OAI.Brennan.linear_circle_logIncrement_neg line 124
  16. lemma OAI.Brennan.HasLogIncrement.smul line 139
  17. lemma OAI.Brennan.norm_linear_lower_pos line 150
  18. lemma OAI.Brennan.norm_linear_lower_neg line 157
  19. lemma OAI.Brennan.local_logIncrement_of_derivative line 164
  20. lemma OAI.Brennan.local_logIncrement_pos line 188
  21. lemma OAI.Brennan.local_logIncrement_neg line 199
  22. lemma OAI.Brennan.exists_log_lift line 210
  23. lemma OAI.Brennan.log_lifts_difference_constant line 218
  24. lemma OAI.Brennan.HasLogIncrement.unique line 232
  25. lemma OAI.Brennan.HasLogIncrement.mul line 240
  26. lemma OAI.Brennan.HasLogIncrement.inv line 252
  27. lemma OAI.Brennan.HasLogIncrement.conj line 266
  28. lemma OAI.Brennan.HasLogIncrement.of_global_log line 276
  29. lemma OAI.Brennan.HasLogIncrement.integer line 284
  30. lemma OAI.Brennan.period_ne_zero line 292
  31. lemma OAI.Brennan.integer_period_injective line 296
  32. lemma OAI.Brennan.exists_integer_logIncrement line 301
  33. def OAI.Brennan.windingNumber line 309
  34. lemma OAI.Brennan.windingNumber_spec line 315
  35. lemma OAI.Brennan.windingNumber_eq_of_logIncrement line 321
  36. lemma OAI.Brennan.windingNumber_mul line 329
  37. lemma OAI.Brennan.windingNumber_perturb line 338
  38. lemma OAI.Brennan.exists_log_lift_of_simplyConnected line 344
  39. lemma OAI.Brennan.HasLogIncrement.homotopy line 352
  40. lemma OAI.Brennan.windingNumber_homotopy line 370
  41. def OAI.Brennan.loopIndex line 378
  42. lemma OAI.Brennan.loopIndex_eventually_eq line 381
  43. lemma OAI.Brennan.continuousOn_loopIndex line 394
  44. lemma OAI.Brennan.hasLogIncrement_constant line 402
  45. lemma OAI.Brennan.loopIndex_eq_zero_of_norm_lt line 407
  46. lemma OAI.Brennan.loopIndex_zero_outside_ball line 416
  47. def OAI.Brennan.windingInterior line 425
  48. lemma OAI.Brennan.isOpen_windingInterior line 428
  49. lemma OAI.Brennan.isBounded_windingInterior line 436
  50. lemma OAI.Brennan.frontier_windingInterior_subset line 445