OAI/Probability/SKSupport/Moments/JetFields.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.compactJet line 15
  2. lemma OAI.ZeroTemperatureSK.compactJet_hasDerivAt line 18
  3. lemma OAI.ZeroTemperatureSK.deriv_compactJet line 30
  4. def OAI.ZeroTemperatureSK.compactJetField line 35
  5. lemma OAI.ZeroTemperatureSK.compactRate_jet_one line 53
  6. lemma OAI.ZeroTemperatureSK.compactRate_jet_two line 59
  7. lemma OAI.ZeroTemperatureSK.compactRate_jet_three line 74
  8. lemma OAI.ZeroTemperatureSK.compactJetField_generator_one line 91
  9. lemma OAI.ZeroTemperatureSK.compactJetField_generator_two line 101
  10. def OAI.ZeroTemperatureSK.curvatureField line 123
  11. def OAI.ZeroTemperatureSK.secondCurvatureField line 127
  12. lemma OAI.ZeroTemperatureSK.curvatureField_deriv line 132
  13. lemma OAI.ZeroTemperatureSK.curvatureField_generator line 139
  14. lemma OAI.ZeroTemperatureSK.secondCurvatureField_generator line 150
  15. lemma OAI.ZeroTemperatureSK.curvatureField_eq line 165
  16. lemma OAI.ZeroTemperatureSK.secondCurvatureField_eq line 171