OAI/Analysis/IntegralMeans/RankPairing.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Brennan.diskClassSecondCountable line 21
  2. lemma OAI.Brennan.continuous_class_deriv line 23
  3. lemma OAI.Brennan.continuous_class_deriv_deriv line 26
  4. lemma OAI.Brennan.continuous_class_criticalMap line 30
  5. lemma OAI.Brennan.continuous_class_fderiv_criticalMap line 36
  6. lemma OAI.Brennan.continuous_class_normalizedJacobian line 57
  7. def OAI.Brennan.criticalHeight line 65
  8. lemma OAI.Brennan.criticalHeight_pos line 68
  9. lemma OAI.Brennan.continuous_class_criticalHeight line 73
  10. lemma OAI.Brennan.continuousOn_prod_of_continuous_subtype line 85
  11. lemma OAI.Brennan.criticalMap_congr line 94
  12. lemma OAI.Brennan.normalizedJacobian_congr line 99
  13. lemma OAI.Brennan.criticalHeight_congr line 107
  14. lemma OAI.Brennan.goodPair_congr line 112
  15. def OAI.Brennan.affineHome line 129
  16. lemma OAI.Brennan.affineHome_apply line 133
  17. lemma OAI.Brennan.affine_mem_iff line 136
  18. def OAI.Brennan.rerootTarget line 143
  19. def OAI.Brennan.heightScaleInverse line 146
  20. lemma OAI.Brennan.heightScaleInverse_pos line 149
  21. lemma OAI.Brennan.reciprocalPotential_reroot line 153
  22. lemma OAI.Brennan.criticalHeight_reroot line 170
  23. lemma OAI.Brennan.criticalMap_reroot_fiber line 181
  24. lemma OAI.Brennan.potential_level_reroot line 187
  25. lemma OAI.Brennan.goodPair_reroot line 203
  26. def OAI.Brennan.orderRank line 229
  27. lemma OAI.Brennan.orderRank_strictMonoOn line 231
  28. lemma OAI.Brennan.orderRank_injOn line 241
  29. lemma OAI.Brennan.orderRank_finset_enum line 245
  30. lemma OAI.Brennan.exists_orderRank_of_finite_initial line 260
  31. def OAI.Brennan.heightKey line 278
  32. lemma OAI.Brennan.heightKey_injective line 281
  33. def OAI.Brennan.heightOrder line 286
  34. def OAI.Brennan.heightRank line 288
  35. def OAI.Brennan.heightPrecedes line 290
  36. lemma OAI.Brennan.heightOrder_lt_iff line 293
  37. lemma OAI.Brennan.heightOrder_height_le line 298
  38. lemma OAI.Brennan.heightRank_pred_finite line 304
  39. lemma OAI.Brennan.heightRank_lt_segment line 309
  40. lemma OAI.Brennan.exists_equal_heightRank line 319
  41. lemma OAI.Brennan.heightRank_injOn line 330
  42. lemma OAI.Brennan.heightRank_eq_ncard line 334
  43. lemma OAI.Brennan.heightRank_transport line 342
  44. def OAI.Brennan.rankPartner line 357
  45. lemma OAI.Brennan.rankPartner_spec line 360
  46. lemma OAI.Brennan.rankPartner_eq line 367
  47. lemma OAI.Brennan.rankPartner_height line 373
  48. lemma OAI.Brennan.rankPartner_injOn line 382
  49. def OAI.Brennan.positiveFiber line 389
  50. def OAI.Brennan.negativeFiber line 392
  51. lemma OAI.Brennan.criticalHeight_count line 395
  52. lemma OAI.Brennan.criticalHeight_rank_inj line 432
  53. lemma OAI.Brennan.exists_critical_equalRank line 442
  54. def OAI.Brennan.criticalPair line 450
  55. lemma OAI.Brennan.criticalPair_spec line 454
  56. lemma OAI.Brennan.criticalPair_injective line 465