OAI/Geometry/TamingCompatibility/DifferentialForms/JAction.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TamingCompatibility.Tames.isNondegenerate line 13
  2. lemma OAI.TamingCompatibility.eval_swap line 20
  3. lemma OAI.TamingCompatibility.eval_neg_left line 29
  4. lemma OAI.TamingCompatibility.eval_neg_right line 35
  5. lemma OAI.TamingCompatibility.eval_neg_neg line 40
  6. def OAI.TamingCompatibility.jAction line 44
  7. lemma OAI.TamingCompatibility.eval_jAction line 47
  8. def OAI.TamingCompatibility.invariantPart line 56
  9. def OAI.TamingCompatibility.antiInvariantPart line 59
  10. lemma OAI.TamingCompatibility.eval_invariantPart line 62
  11. lemma OAI.TamingCompatibility.invariantPart_isInvariant line 70
  12. lemma OAI.TamingCompatibility.eval_invariantPart_complexLine line 75
  13. lemma OAI.TamingCompatibility.tames_invariantPart line 83
  14. lemma OAI.TamingCompatibility.compatible_invariantPart line 89
  15. lemma OAI.TamingCompatibility.TwoForm.ext_eval line 93
  16. lemma OAI.TamingCompatibility.jAction_involutive line 102
  17. lemma OAI.TamingCompatibility.jAction_add line 109
  18. lemma OAI.TamingCompatibility.jAction_smul line 112
  19. lemma OAI.TamingCompatibility.invariantPart_add_antiInvariantPart line 115
  20. lemma OAI.TamingCompatibility.invariantPart_idempotent line 120
  21. lemma OAI.TamingCompatibility.antiInvariantPart_idempotent line 126
  22. lemma OAI.TamingCompatibility.AlmostComplexStructure.injective line 133
  23. lemma OAI.TamingCompatibility.AlmostComplexStructure.surjective line 139
  24. lemma OAI.TamingCompatibility.pullback_add line 146
  25. lemma OAI.TamingCompatibility.pullback_smul line 150
  26. lemma OAI.TamingCompatibility.IsSmooth.zero line 154
  27. lemma OAI.TamingCompatibility.IsSmooth.add line 160
  28. lemma OAI.TamingCompatibility.IsSmooth.smul line 167
  29. lemma OAI.TamingCompatibility.IsClosed.zero line 174
  30. lemma OAI.TamingCompatibility.IsClosed.add line 182
  31. lemma OAI.TamingCompatibility.IsClosed.smul line 191
  32. def OAI.TamingCompatibility.smoothClosedInvariantForms line 197
  33. lemma OAI.TamingCompatibility.convex_taming_forms line 216
  34. def OAI.TamingCompatibility.associatedBilinear line 229
  35. lemma OAI.TamingCompatibility.associatedBilinear_apply line 238
  36. lemma OAI.TamingCompatibility.IsInvariant.shift_J line 247
  37. lemma OAI.TamingCompatibility.IsInvariant.associatedBilinear_symm line 254
  38. lemma OAI.TamingCompatibility.IsInvariant.associatedBilinear_hermitian line 263
  39. lemma OAI.TamingCompatibility.Tames.associatedBilinear_pos line 270
  40. lemma OAI.TamingCompatibility.associatedBilinear_invariantPart_fundamental line 276