OAI/Probability/LatticeSurface/Dynamics/MatrixJacobi.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TangentialJacobian.asMatrix line 13
  2. lemma OAI.TangentialJacobian.asMatrix_apply line 16
  3. lemma OAI.TangentialJacobian.asMatrix_one line 19
  4. lemma OAI.TangentialJacobian.asMatrix_add line 22
  5. lemma OAI.TangentialJacobian.asMatrix_sub line 25
  6. lemma OAI.TangentialJacobian.asMatrix_smul line 28
  7. lemma OAI.TangentialJacobian.asMatrix_mul line 31
  8. lemma OAI.TangentialJacobian.asMatrix_det line 35
  9. def OAI.TangentialJacobian.detPoly line 38
  10. lemma OAI.TangentialJacobian.detPoly_eval line 41
  11. lemma OAI.TangentialJacobian.detPoly_coeff_one line 50
  12. lemma OAI.TangentialJacobian.det_line_deriv_zero line 54
  13. lemma OAI.TangentialJacobian.det_add_line_deriv_zero line 61
  14. lemma OAI.TangentialJacobian.det_line_deriv line 72
  15. def OAI.TangentialJacobian.traceCLM line 83
  16. lemma OAI.TangentialJacobian.traceCLM_apply line 87
  17. lemma OAI.TangentialJacobian.asMatrix_neg line 91
  18. lemma OAI.TangentialJacobian.inverse_line_deriv_zero line 95
  19. lemma OAI.TangentialJacobian.trace_inverse_line_deriv_zero line 106
  20. lemma OAI.TangentialJacobian.detPoly_second_derivative line 115
  21. lemma OAI.TangentialJacobian.detPoly_coeff_two line 137
  22. lemma OAI.TangentialJacobian.continuous_asMatrix_entry line 144
  23. lemma OAI.TangentialJacobian.detPoly_coeff_continuous line 148
  24. lemma OAI.TangentialJacobian.detPoly_degree_le line 160
  25. lemma OAI.TangentialJacobian.detPoly_eval_sum line 171
  26. lemma OAI.TangentialJacobian.continuous_integrable_of_bounded line 181
  27. lemma OAI.TangentialJacobian.detPoly_coeff_integrable line 190
  28. def OAI.TangentialJacobian.integratedDetPoly line 198
  29. lemma OAI.TangentialJacobian.integratedDetPoly_coeff line 203
  30. lemma OAI.TangentialJacobian.integratedDetPoly_eval line 209
  31. lemma OAI.TangentialJacobian.integratedDetPoly_eq_const line 218
  32. lemma OAI.TangentialJacobian.trace_integral_zero_of_det_identity line 229
  33. lemma OAI.TangentialJacobian.trace_square_integral_of_det_identity line 239