OAI/Analysis/IntegralMeans/BorelPairing.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.joint_locally_injective line 21
  2. lemma OAI.Brennan.countable_joint_injective_partition line 62
  3. lemma OAI.Brennan.exists_borel_partial_inverse line 101
  4. lemma OAI.Brennan.fiber_count_eq_tsum_branches line 122
  5. lemma OAI.Brennan.measurable_fiber_count_branches line 162
  6. lemma OAI.Brennan.measurable_branch_selection line 187
  7. structure OAI.Brennan.BorelBranches line 204
  8. lemma OAI.Brennan.exists_borelBranches line 217
  9. lemma OAI.Brennan.BorelBranches.measurable_count line 229
  10. lemma OAI.Brennan.count_product_fiber line 238
  11. lemma OAI.Brennan.count_subtype_set line 255
  12. instance OAI.Brennan.(instance at line 264) line 264
  13. instance OAI.Brennan.(instance at line 268) line 268
  14. instance OAI.Brennan.(instance at line 270) line 270
  15. def OAI.Brennan.identityHalf line 272
  16. lemma OAI.Brennan.identityHalf_schlicht line 274
  17. def OAI.Brennan.identityClass line 279
  18. instance OAI.Brennan.(instance at line 281) line 281
  19. def OAI.Brennan.jointCriticalMap line 283
  20. def OAI.Brennan.nonsingularClass line 286
  21. lemma OAI.Brennan.continuous_jointCriticalMap line 289
  22. lemma OAI.Brennan.exists_class_branches line 292
  23. def OAI.Brennan.classPrecedes line 320
  24. lemma OAI.Brennan.measurableSet_classPrecedes line 325
  25. def OAI.Brennan.classRankCount line 338
  26. lemma OAI.Brennan.measurable_classRankCount line 342
  27. def OAI.Brennan.signedFiber line 349
  28. lemma OAI.Brennan.signedFiber_one line 352
  29. lemma OAI.Brennan.signedFiber_neg_one line 355
  30. lemma OAI.Brennan.classRankCount_eq_count line 358
  31. lemma OAI.Brennan.classRankCount_eq_heightRank line 387
  32. lemma OAI.Brennan.heightRank_transport_on line 405
  33. lemma OAI.Brennan.heightPrecedes_reroot line 419
  34. lemma OAI.Brennan.signedFiber_reroot line 430
  35. lemma OAI.Brennan.heightRank_reroot line 439
  36. lemma OAI.Brennan.criticalPair_reroot line 448
  37. lemma OAI.Brennan.heightRank_congr_on line 483
  38. lemma OAI.Brennan.signedFiber_congr line 493
  39. lemma OAI.Brennan.criticalPair_congr line 501
  40. def OAI.Brennan.halfOne line 525
  41. lemma OAI.Brennan.class_normalizedJacobian_reroot line 527
  42. lemma OAI.Brennan.class_goodPair_reroot line 534
  43. lemma OAI.Brennan.class_criticalPair_reroot line 543
  44. lemma OAI.Brennan.class_normalizedJacobian_root line 556
  45. lemma OAI.Brennan.class_goodPair_root line 561