OAI/Analysis/SymmetricDomains/FieldSecondJet.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.Biholomorph.rotationScalar line 38
  2. theorem OAI.Release061.Biholomorph.rotationScalar_zero line 39
  3. theorem OAI.Release061.Biholomorph.rotationScalar_add line 40
  4. theorem OAI.Release061.Biholomorph.rotationScalar_mul_neg line 42
  5. theorem OAI.Release061.Biholomorph.rotationScalar_norm line 44
  6. def OAI.Release061.Biholomorph.tangentialRotation line 46
  7. def OAI.Release061.Biholomorph.flatTangentialRotation line 56
  8. theorem OAI.Release061.Biholomorph.flatTangentialRotation_apply line 60
  9. def OAI.Release061.Biholomorph.flatTangentialInfinitesimal line 65
  10. theorem OAI.Release061.Biholomorph.hasDerivAt_rotationScalar line 70
  11. theorem OAI.Release061.Biholomorph.hasDerivAt_flatTangentialRotation line 75
  12. theorem OAI.Release061.Biholomorph.flatTangentialRotation_mem line 84
  13. theorem OAI.Release061.Biholomorph.exists_actual_model_rotation line 99
  14. theorem OAI.hasFDerivAt_centeredLinear line 136
  15. theorem OAI.lieBracket_centeredLinear_eq line 141
  16. theorem OAI.fderiv_lieBracket_centeredLinear line 147
  17. theorem OAI.lieBracket_centeredLinear_zeroJet line 159
  18. theorem OAI.lieBracket_centeredLinear_firstJet line 164
  19. theorem OAI.lieBracket_centeredLinear_secondJet line 171
  20. def OAI.ZeroSecondJet line 208
  21. theorem OAI.ZeroSecondJet.comp line 212
  22. theorem OAI.ZeroSecondJet.clm_apply line 231
  23. theorem OAI.ZeroSecondJet.congr line 260
  24. theorem OAI.fderiv_fderiv_add_of_analytic line 270
  25. theorem OAI.fderiv_fderiv_smul_of_analytic line 279
  26. def OAI.fieldFirstJet line 291
  27. def OAI.fieldSecondJet line 300