OAI/Geometry/TamingCompatibility/Charts/LocalFormalAdjoint.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.LocalFormalAdjoint.multiply line 16
  2. lemma OAI.TamingCompatibility.LocalFormalAdjoint.multiply_apply line 21
  3. def OAI.TamingCompatibility.LocalFormalAdjoint.adjointCoefficient line 24
  4. lemma OAI.TamingCompatibility.LocalFormalAdjoint.adjointCoefficient_apply line 28
  5. lemma OAI.TamingCompatibility.LocalFormalAdjoint.multiply_pairing line 32
  6. lemma OAI.TamingCompatibility.LocalFormalAdjoint.directional_formal_adjoint line 37
  7. def OAI.TamingCompatibility.LocalFormalAdjoint.firstOrder line 54
  8. def OAI.TamingCompatibility.LocalFormalAdjoint.formalAdjoint line 59
  9. lemma OAI.TamingCompatibility.LocalFormalAdjoint.inner_integrable line 66
  10. lemma OAI.TamingCompatibility.LocalFormalAdjoint.firstOrder_pairing line 69
  11. lemma OAI.TamingCompatibility.LocalFormalAdjoint.lineDeriv_multiply line 97
  12. lemma OAI.TamingCompatibility.LocalFormalAdjoint.formalAdjoint_expanded line 111
  13. def OAI.TamingCompatibility.LocalFormalAdjoint.weightedCoefficient line 123
  14. lemma OAI.TamingCompatibility.LocalFormalAdjoint.weightedCoefficient_apply line 128
  15. lemma OAI.TamingCompatibility.LocalFormalAdjoint.weighted_firstOrder line 134
  16. def OAI.TamingCompatibility.LocalFormalAdjoint.weightedFormalAdjoint line 143
  17. lemma OAI.TamingCompatibility.LocalFormalAdjoint.weighted_firstOrder_pairing line 148