OAI/Analysis/StrictMeans/MeasurableGeometry.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.isClosed_exists_mem_compact line 109
  2. lemma OAI.StrictInverseFirstPower.measurableSet_exists_of_closed_sigmaCompact line 122
  3. lemma OAI.StrictInverseFirstPower.measurableSet_compact_positive_sublevels line 141
  4. lemma OAI.StrictInverseFirstPower.reciprocalFunction_deriv line 185
  5. lemma OAI.StrictInverseFirstPower.logarithmicDerivative_eq_reciprocal line 193
  6. lemma OAI.StrictInverseFirstPower.continuous_logarithmicDerivative line 200
  7. lemma OAI.StrictInverseFirstPower.continuous_jacobianExpression line 212
  8. lemma OAI.StrictInverseFirstPower.reciprocalFunction_rebase line 218
  9. lemma OAI.StrictInverseFirstPower.reciprocalFunction_rebase_deriv line 223
  10. lemma OAI.StrictInverseFirstPower.logarithmicDerivative_rebase line 235
  11. lemma OAI.StrictInverseFirstPower.jacobianExpression_rebase line 247
  12. lemma OAI.StrictInverseFirstPower.jacobianExpression_rebase_I line 252
  13. def OAI.StrictInverseFirstPower.reciprocalPotential line 265
  14. lemma OAI.StrictInverseFirstPower.continuous_reciprocalPotential line 268
  15. lemma OAI.StrictInverseFirstPower.reciprocalPotential_sublevel_image line 276
  16. lemma OAI.StrictInverseFirstPower.compactPotential_iff line 295
  17. def OAI.StrictInverseFirstPower.GoodPair line 309
  18. lemma OAI.StrictInverseFirstPower.continuous_jacobianExpression_upper line 317
  19. lemma OAI.StrictInverseFirstPower.measurableSet_regular_pairs line 325
  20. lemma OAI.StrictInverseFirstPower.measurableSet_untied_pairs line 339
  21. lemma OAI.StrictInverseFirstPower.measurableSet_goodPairs line 390