OAI/Analysis/StrictMeans/AreaTails.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.affineInversePlane line 72
  2. lemma OAI.StrictInverseFirstPower.affineInversePlane_re line 74
  3. lemma OAI.StrictInverseFirstPower.affineInversePlane_im line 76
  4. lemma OAI.StrictInverseFirstPower.coe_affineInverse line 79
  5. lemma OAI.StrictInverseFirstPower.affineInversePlane_mapsTo line 82
  6. lemma OAI.StrictInverseFirstPower.affineInversePlane_involution line 89
  7. lemma OAI.StrictInverseFirstPower.affineInversePlane_injOn line 96
  8. lemma OAI.StrictInverseFirstPower.continuous_affineInverse line 102
  9. def OAI.StrictInverseFirstPower.outsideCenter line 107
  10. def OAI.StrictInverseFirstPower.outsideCenterH line 109
  11. lemma OAI.StrictInverseFirstPower.measurableSet_outsideCenter line 111
  12. lemma OAI.StrictInverseFirstPower.measurableSet_outsideCenterH line 117
  13. lemma OAI.StrictInverseFirstPower.norm_cayley_inverse line 122
  14. lemma OAI.StrictInverseFirstPower.affineInversePlane_outside_image line 136
  15. lemma OAI.StrictInverseFirstPower.affineInversePlane_hasFDerivAt line 145
  16. lemma OAI.StrictInverseFirstPower.det_affineInversePlane line 157
  17. lemma OAI.StrictInverseFirstPower.lintegral_affineInverse_outside line 170
  18. lemma OAI.StrictInverseFirstPower.holomorphic_lintegral_image line 194
  19. lemma OAI.StrictInverseFirstPower.integrable_inverse_cube_outside line 202
  20. lemma OAI.StrictInverseFirstPower.inverse_cube_tail_finite line 230
  21. lemma OAI.StrictInverseFirstPower.halfPlane_area_tail_uniform line 235
  22. def OAI.StrictInverseFirstPower.halfPlaneProjection line 256
  23. lemma OAI.StrictInverseFirstPower.measurable_halfPlaneProjection line 259
  24. lemma OAI.StrictInverseFirstPower.halfPlaneProjection_coe line 262
  25. lemma OAI.StrictInverseFirstPower.halfPlaneProjection_of_pos line 265
  26. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_inverse_rebase line 268
  27. def OAI.StrictInverseFirstPower.inverseCubeValue line 274
  28. def OAI.StrictInverseFirstPower.conformalAreaCube line 277
  29. lemma OAI.StrictInverseFirstPower.measurable_inverseCubeValue line 280
  30. lemma OAI.StrictInverseFirstPower.measurable_conformalAreaCube line 284
  31. lemma OAI.StrictInverseFirstPower.weighted_inverse_cube_rebase line 289
  32. lemma OAI.StrictInverseFirstPower.area_cube_expectation line 307
  33. def OAI.StrictInverseFirstPower.weightedAreaTail line 324
  34. lemma OAI.StrictInverseFirstPower.measurable_inverseCube_plane line 327
  35. lemma OAI.StrictInverseFirstPower.measurable_conformalArea_plane line 333
  36. lemma OAI.StrictInverseFirstPower.measurable_areaTail_density line 339
  37. lemma OAI.StrictInverseFirstPower.measurable_weightedAreaTail line 345
  38. lemma OAI.StrictInverseFirstPower.expected_area_tail line 348
  39. theorem OAI.StrictInverseFirstPower.weightedAreaTail_ae_finite line 376