OAI/Analysis/StrictMeans/JacobianMoments.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.StrictInverseFirstPower.real_det_eq line 66
  2. def OAI.StrictInverseFirstPower.criticalMap line 71
  3. def OAI.StrictInverseFirstPower.normalizedJacobian line 74
  4. theorem OAI.StrictInverseFirstPower.criticalMap_fderiv line 77
  5. def OAI.StrictInverseFirstPower.logarithmicDerivative line 97
  6. def OAI.StrictInverseFirstPower.jacobianExpression line 100
  7. theorem OAI.StrictInverseFirstPower.determinant_columns_factor line 104
  8. theorem OAI.StrictInverseFirstPower.criticalMap_fderiv_one line 112
  9. theorem OAI.StrictInverseFirstPower.criticalMap_fderiv_I line 123
  10. theorem OAI.StrictInverseFirstPower.normalizedJacobian_eq line 134
  11. lemma OAI.StrictInverseFirstPower.reciprocalFunction_deriv_I line 160
  12. lemma OAI.StrictInverseFirstPower.logarithmicDerivative_I_eq line 168
  13. lemma OAI.StrictInverseFirstPower.continuous_logarithmicDerivative_I line 173
  14. lemma OAI.StrictInverseFirstPower.logarithmicDerivative_integrable_I line 179
  15. lemma OAI.StrictInverseFirstPower.logarithmicDerivative_real_moment line 184
  16. lemma OAI.StrictInverseFirstPower.logarithmicDerivative_norm_sq_moment line 190
  17. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_normalizedJacobian_I line 196
  18. lemma OAI.StrictInverseFirstPower.expected_normalizedJacobian line 203
  19. theorem OAI.StrictInverseFirstPower.expected_normalizedJacobian_at_source_k line 226