OAI/Analysis/IntegralMeans/Degree.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.orientedDifference line 21
  2. lemma OAI.Brennan.norm_orientedDifference line 24
  3. lemma OAI.Brennan.orientedDifference_eq_zero line 27
  4. lemma OAI.Brennan.continuous_orientedDifference line 31
  5. def OAI.Brennan.radialCutoff line 36
  6. lemma OAI.Brennan.continuous_radialCutoff line 39
  7. lemma OAI.Brennan.radialCutoff_one line 43
  8. lemma OAI.Brennan.radialCutoff_zero line 48
  9. def OAI.Brennan.surgeryLog line 55
  10. lemma OAI.Brennan.continuousAt_surgeryLog line 58
  11. lemma OAI.Brennan.surgeryLog_eq_zero_eventually line 77
  12. def OAI.Brennan.removeZero line 83
  13. lemma OAI.Brennan.removeZero_eq_const_near line 88
  14. lemma OAI.Brennan.continuous_removeZero line 106
  15. lemma OAI.Brennan.removeZero_eq_zero_iff line 130
  16. lemma OAI.Brennan.removeZero_factorization line 138
  17. lemma OAI.Brennan.exists_slit_radius_of_derivative line 146
  18. lemma OAI.Brennan.exists_slit_radius_pos line 183
  19. lemma OAI.Brennan.exists_slit_radius_neg line 196
  20. lemma OAI.Brennan.differentiable_orientedDifference line 209
  21. lemma OAI.Brennan.hasFDerivAt_removeZero_other line 216
  22. lemma OAI.Brennan.det_complex_smul line 238
  23. lemma OAI.Brennan.windingNumber_orientedDifference line 245
  24. lemma OAI.Brennan.windingNumber_removeZero_add line 265
  25. lemma OAI.Brennan.windingNumber_comp_zero_of_nonvanishing line 299
  26. lemma OAI.Brennan.windingNumber_comp_zero_on_convex line 306
  27. def OAI.Brennan.planeIndex line 323
  28. lemma OAI.Brennan.planeIndex_complex_smul line 326
  29. theorem OAI.Brennan.windingNumber_finite_regular_zeros line 331
  30. lemma OAI.Brennan.exists_countable_injective_partition line 404
  31. def OAI.Brennan.fiberMultiplicity line 439
  32. lemma OAI.Brennan.fiber_subsingleton_of_injOn line 442
  33. lemma OAI.Brennan.fiberMultiplicity_of_injOn line 447
  34. lemma OAI.Brennan.fiberMultiplicity_partition line 461
  35. lemma OAI.Brennan.area_formula_regular line 476
  36. lemma OAI.Brennan.lintegral_positive_part_eq line 507
  37. lemma OAI.Brennan.integral_det_nonpos_of_fiberMultiplicity line 521
  38. lemma OAI.Brennan.finite_regular_zeros_on_compact line 549
  39. lemma OAI.Brennan.loopIndex_circle_inside line 573
  40. lemma OAI.Brennan.ae_regular_value line 588
  41. lemma OAI.Brennan.signed_sum_eq_card_sub line 598
  42. lemma OAI.Brennan.integral_jacobian_nonpos_of_boundary_winding line 611