OAI/Analysis/IntegralMeans/GoodPairs.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.compact_sublevels_iff_exhaustion line 24
  2. lemma OAI.Brennan.measurableSet_compact_sublevels line 42
  3. lemma OAI.Brennan.compact_sublevels_iff_positive line 66
  4. lemma OAI.Brennan.compact_positive_superlevels_iff line 73
  5. lemma OAI.Brennan.measurableSet_compact_positive_superlevels line 107
  6. lemma OAI.Brennan.measurableSet_regular_parameters line 131
  7. lemma OAI.Brennan.ae_regular_values line 162
  8. lemma OAI.Brennan.potential_superlevel_eq_closed line 172
  9. lemma OAI.Brennan.measurableSet_class_goodPairs line 183
  10. lemma OAI.Brennan.class_ae_goodPairs line 205
  11. def OAI.Brennan.pairingDomain line 219
  12. lemma OAI.Brennan.measurableSet_pairingDomain line 223
  13. lemma OAI.Brennan.criticalPair_eq_of_classRanks line 230
  14. lemma OAI.Brennan.measurable_criticalPair line 249