OAI/Geometry/QuadricBundles/MatrixDynamics.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuadricCounterexample.source_A_det line 11
  2. lemma OAI.QuadricCounterexample.source_B_det line 14
  3. lemma OAI.QuadricCounterexample.source_A_trace line 17
  4. lemma OAI.QuadricCounterexample.source_B_trace line 20
  5. lemma OAI.QuadricCounterexample.matrix_sq_of_det_trace_one line 23
  6. lemma OAI.QuadricCounterexample.matrix_cube_of_det_trace_one line 34
  7. lemma OAI.QuadricCounterexample.source_A_cube line 44
  8. lemma OAI.QuadricCounterexample.source_B_cube line 46
  9. lemma OAI.QuadricCounterexample.source_A_six line 49
  10. lemma OAI.QuadricCounterexample.source_B_six line 52
  11. lemma OAI.QuadricCounterexample.source_A_inv line 56
  12. lemma OAI.QuadricCounterexample.source_relative_trace line 62
  13. lemma OAI.QuadricCounterexample.source_product_trace line 74
  14. lemma OAI.QuadricCounterexample.source_abs_product_trace_gt_two line 83
  15. def OAI.QuadricCounterexample.projectiveCoord line 96
  16. lemma OAI.QuadricCounterexample.projectiveCoord_eq line 99
  17. lemma OAI.QuadricCounterexample.projectiveCoord_smul line 105
  18. lemma OAI.QuadricCounterexample.projectiveCoord_action line 111
  19. lemma OAI.QuadricCounterexample.tendsto_projectiveCoord line 120
  20. theorem OAI.QuadricCounterexample.projective_orbit_converges_in_eigenbasis line 133
  21. theorem OAI.QuadricCounterexample.projective_north_south_of_eigenbasis line 188
  22. def OAI.QuadricCounterexample.expandingRoot line 222
  23. def OAI.QuadricCounterexample.contractingRoot line 223
  24. lemma OAI.QuadricCounterexample.hyperbolic_roots line 225
  25. lemma OAI.QuadricCounterexample.hyperbolic_norm_ratio line 244
  26. def OAI.QuadricCounterexample.hyperbolicBasis line 251
  27. lemma OAI.QuadricCounterexample.hyperbolicBasis_det_ne_zero line 256
  28. lemma OAI.QuadricCounterexample.hyperbolicBasis_diagonalizes line 269
  29. theorem OAI.QuadricCounterexample.invariant_measure_ae_endpoints line 295
  30. lemma OAI.QuadricCounterexample.fixed_of_period_three_in_pair line 313
  31. theorem OAI.QuadricCounterexample.no_invariant_measure_of_period_three_north_south line 327
  32. def OAI.QuadricCounterexample.source_A_gl line 355
  33. def OAI.QuadricCounterexample.source_B_gl line 357
  34. lemma OAI.QuadricCounterexample.source_A_gl_val line 360
  35. lemma OAI.QuadricCounterexample.source_B_gl_val line 361
  36. lemma OAI.QuadricCounterexample.projective_cube_identity line 363
  37. lemma OAI.QuadricCounterexample.source_no_common_fixed_point line 376
  38. lemma OAI.QuadricCounterexample.source_product_lower_left_ne_zero line 400
  39. def OAI.QuadricCounterexample.source_eigenbasis line 405
  40. lemma OAI.QuadricCounterexample.source_north_south line 413
  41. theorem OAI.QuadricCounterexample.source_no_invariant_finite_measure line 443