OAI/Geometry/PrescribedPotential/LinearFrameCalculus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Linear Frame Calculus.

  1. def OAI.KaehlerCalculus.frameMatrix line 18
  2. def OAI.KaehlerCalculus.pullMetric line 21
  3. lemma OAI.KaehlerCalculus.frameMatrix_mulVec line 24
  4. lemma OAI.KaehlerCalculus.pullMetric_smooth line 27
  5. lemma OAI.KaehlerCalculus.wderiv_comp_linear line 34
  6. lemma OAI.KaehlerCalculus.mderiv_comp_linear line 44
  7. lemma OAI.KaehlerCalculus.mderiv_congruence line 50
  8. lemma OAI.KaehlerCalculus.mderiv_pullMetric line 57
  9. lemma OAI.KaehlerCalculus.fundamental_pullMetric line 66
  10. lemma OAI.KaehlerCalculus.pullMetric_closed line 73