OAI/Analysis/Conductivity/Sobolev/ChildH10Transport.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.gradient_apply_single line 15
  2. lemma OAI.ScalarConductivity.sourceChildEuclidean_symm_gradient line 20
  3. def OAI.ScalarConductivity.childTransportComponentCLM line 34
  4. def OAI.ScalarConductivity.childTransportJetCLM line 40
  5. lemma OAI.ScalarConductivity.childTransportComponentCLM_smooth_ae line 43
  6. lemma OAI.ScalarConductivity.childTransportJetCLM_smooth line 62
  7. lemma OAI.ScalarConductivity.childTransportJetCLM_H10 line 80
  8. def OAI.ScalarConductivity.childH10Transport line 96
  9. lemma OAI.ScalarConductivity.childH10Transport_mem_H10 line 100
  10. def OAI.ScalarConductivity.physicalChildCompletionJoin line 112
  11. lemma OAI.ScalarConductivity.physicalChildCompletionJoin_mem_H10 line 117
  12. lemma OAI.ScalarConductivity.physicalChildCompletionJoin_jet line 121
  13. def OAI.ScalarConductivity.centralInteriorComponentCLM line 132
  14. def OAI.ScalarConductivity.centralInteriorJetCLM line 142
  15. lemma OAI.ScalarConductivity.centralInteriorComponentCLM_smooth_value line 145
  16. lemma OAI.ScalarConductivity.centralInteriorComponentCLM_smooth_gradient line 161
  17. lemma OAI.ScalarConductivity.centralInteriorJetCLM_smooth_H10 line 188
  18. theorem OAI.ScalarConductivity.centralInteriorJetCLM_central_H10 line 219
  19. def OAI.ScalarConductivity.centralInteriorCompletion line 232
  20. lemma OAI.ScalarConductivity.centralInteriorCompletion_mem_H10 line 237