OAI/Analysis/IntegralMeans/InverseDensity.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.affineInverse line 25
  2. lemma OAI.Brennan.affineInverse_re line 27
  3. lemma OAI.Brennan.affineInverse_im line 30
  4. lemma OAI.Brennan.affineInverse_mem line 33
  5. lemma OAI.Brennan.affineInverse_invol line 36
  6. lemma OAI.Brennan.affineInverse_injOn line 43
  7. lemma OAI.Brennan.affineInverse_affine line 47
  8. lemma OAI.Brennan.hasFDerivAt_affineInverse line 52
  9. lemma OAI.Brennan.differentiableAt_affineInverse line 68
  10. lemma OAI.Brennan.fderiv_affineInverse_apply line 71
  11. lemma OAI.Brennan.det_affineInverse line 82
  12. lemma OAI.Brennan.affineInverse_change_variables line 97
  13. lemma OAI.Brennan.diskCayley_affineInverse line 107
  14. lemma OAI.Brennan.diskCayley_affineInverse_norm line 120
  15. lemma OAI.Brennan.affineInverse_mem_outsideCore line 124
  16. lemma OAI.Brennan.affineInverse_image_outsideCore line 127
  17. lemma OAI.Brennan.reroot_at_affineInverse line 135
  18. lemma OAI.Brennan.classWeight_inverse_value line 141
  19. lemma OAI.Brennan.inverse_area_bound line 152
  20. def OAI.Brennan.planeClassDeriv line 208
  21. lemma OAI.Brennan.measurable_planeClassDeriv line 211
  22. lemma OAI.Brennan.planeClassDeriv_eq line 224
  23. def OAI.Brennan.inverseDensity line 227
  24. def OAI.Brennan.inverseJacDensity line 230
  25. def OAI.Brennan.weightedInverseArea line 233
  26. lemma OAI.Brennan.measurable_inverseDensity line 236
  27. lemma OAI.Brennan.measurable_inverseJacDensity line 239
  28. lemma OAI.Brennan.measurable_weightedInverseArea line 243
  29. lemma OAI.Brennan.inverseJacDensity_integral_le line 248
  30. def OAI.Brennan.HasWeightedLaw line 261
  31. lemma OAI.Brennan.weighted_inverse_identity line 268
  32. lemma OAI.Brennan.weightedInverseArea_expectation_le line 297
  33. lemma OAI.Brennan.weightedInverseArea_ae_finite line 342