OAI/Analysis/Conductivity/Geometry/CentralSlopeJet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.collarSlopeJet line 14
  2. lemma OAI.ScalarConductivity.collarSlopeJet_eq_zero line 21
  3. lemma OAI.ScalarConductivity.collarSlopeJet_zero_not_tsupport line 27
  4. lemma OAI.ScalarConductivity.compact_collar_slope_jet line 33
  5. lemma OAI.ScalarConductivity.ballWholePiJetCLM_slope_ae line 48
  6. def OAI.ScalarConductivity.physicalChildSlopeJet line 59
  7. lemma OAI.ScalarConductivity.exists_parentSlopeExtension line 64
  8. lemma OAI.ScalarConductivity.exists_childSlopeExtension line 72
  9. lemma OAI.ScalarConductivity.parentSlopeJet_zero_central line 88
  10. lemma OAI.ScalarConductivity.physicalChildSlopeJet_zero_central line 93
  11. def OAI.ScalarConductivity.centralSlopeJet line 103
  12. theorem OAI.ScalarConductivity.centralSlopeExtension_exists line 107