OAI/Analysis/StrictMeans/ReciprocalMoments.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.StrictInverseFirstPower.HalfPlaneSet line 59
  2. def OAI.StrictInverseFirstPower.reciprocalFunction line 61
  3. lemma OAI.StrictInverseFirstPower.reciprocalFunction_I line 64
  4. lemma OAI.StrictInverseFirstPower.reciprocalFunction_ne_zero line 67
  5. lemma OAI.StrictInverseFirstPower.reciprocalFunction_differentiableOn line 71
  6. lemma OAI.StrictInverseFirstPower.continuous_reciprocalFunction line 76
  7. lemma OAI.StrictInverseFirstPower.continuous_reciprocalFunction_deriv line 87
  8. lemma OAI.StrictInverseFirstPower.continuous_reciprocalFunction_deriv₂ line 92
  9. abbrev OAI.StrictInverseFirstPower.MomentInterval line 97
  10. def OAI.StrictInverseFirstPower.sourcePath line 99
  11. lemma OAI.StrictInverseFirstPower.sourcePath_zero line 101
  12. lemma OAI.StrictInverseFirstPower.sourcePath_mem line 103
  13. lemma OAI.StrictInverseFirstPower.sourcePath_hasDerivAt line 114
  14. lemma OAI.StrictInverseFirstPower.continuous_sourcePath line 120
  15. lemma OAI.StrictInverseFirstPower.reciprocalPath_hasDerivAt line 124
  16. lemma OAI.StrictInverseFirstPower.reciprocalPath_deriv_hasDerivAt line 132
  17. def OAI.StrictInverseFirstPower.normPathFirst line 153
  18. def OAI.StrictInverseFirstPower.normPathSecond line 158
  19. lemma OAI.StrictInverseFirstPower.normPath_hasDerivAt line 168
  20. lemma OAI.StrictInverseFirstPower.normPathFirst_hasDerivAt line 174
  21. lemma OAI.StrictInverseFirstPower.continuous_normPath_on_interval line 180
  22. lemma OAI.StrictInverseFirstPower.normPathFirst_zero line 200
  23. lemma OAI.StrictInverseFirstPower.normPathSecond_zero line 204
  24. lemma OAI.StrictInverseFirstPower.normPathSecond_add_axes line 211
  25. lemma OAI.StrictInverseFirstPower.normPath_integral_hasDerivAt line 217
  26. lemma OAI.StrictInverseFirstPower.normPathFirst_integral_hasDerivAt line 225
  27. def OAI.StrictInverseFirstPower.ReciprocalMeanLaw line 242
  28. lemma OAI.StrictInverseFirstPower.affine_real_law_mean_law line 245
  29. lemma OAI.StrictInverseFirstPower.normPath_integral_eq_rpow line 254
  30. lemma OAI.StrictInverseFirstPower.normPathFirst_integral_eq line 261
  31. lemma OAI.StrictInverseFirstPower.normPathFirst_integral_zero line 278
  32. lemma OAI.StrictInverseFirstPower.normPathSecond_integral_zero line 283
  33. lemma OAI.StrictInverseFirstPower.normPathSecond_integrable_zero line 301
  34. lemma OAI.StrictInverseFirstPower.reciprocal_deriv_norm_sq_moment line 307