OAI/Geometry/PrescribedPotential/RealFrameScalar.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Real Frame Scalar.

  1. def OAI.HigherJet.frameGradient line 19
  2. lemma OAI.HigherJet.norm_frameGradient_sq line 22
  3. lemma OAI.HigherJet.dir_mul line 27
  4. lemma OAI.HigherJet.frameGradient_mul line 38
  5. lemma OAI.HigherJet.frameGradient_add line 47
  6. lemma OAI.HigherJet.frameGradient_const line 54
  7. lemma OAI.HigherJet.frameLaplace_mul line 59
  8. lemma OAI.HigherJet.frameLaplace_add line 87
  9. lemma OAI.HigherJet.frameLaplace_const line 100
  10. lemma OAI.HigherJet.frameGradient_eq_zero_of_localMax line 112
  11. lemma OAI.HigherJet.frameLaplace_nonpos_of_localMax line 117