OAI/Analysis/Conductivity/Sobolev/ChildH1Pullback.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.sourceChildEuclidean_contDiff line 14
  2. lemma OAI.ScalarConductivity.sourceChildEuclidean_gradient line 19
  3. def OAI.ScalarConductivity.childPullbackComponentCLM line 33
  4. def OAI.ScalarConductivity.childPullbackJetCLM line 38
  5. lemma OAI.ScalarConductivity.childPullbackComponentCLM_ae line 41
  6. lemma OAI.ScalarConductivity.childPullbackJetCLM_ae line 56
  7. lemma OAI.ScalarConductivity.sourceChildEuclidean_quasi line 75
  8. lemma OAI.ScalarConductivity.sourceChildEuclidean_ball_quasi line 80
  9. lemma OAI.ScalarConductivity.childPullbackJetCLM_smooth line 84
  10. lemma OAI.ScalarConductivity.childPullbackJetCLM_H1 line 104
  11. def OAI.ScalarConductivity.childH1Pullback line 118
  12. lemma OAI.ScalarConductivity.childH1Pullback_smooth line 122