OAI/Analysis/Conductivity/Sobolev/ParentCompletionJoin.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.parentLocalJetCLM_smooth_H10 line 21
  2. theorem OAI.ScalarConductivity.parentLocalJetCLM_central_H10 line 44
  3. def OAI.ScalarConductivity.parentCompletionJoin line 55
  4. lemma OAI.ScalarConductivity.parentCompletionJoin_mem_H10 line 59
  5. def OAI.ScalarConductivity.lpBoundedPullbackCLM line 73
  6. lemma OAI.ScalarConductivity.lpBoundedPullbackCLM_ae line 77
  7. lemma OAI.ScalarConductivity.lpBoundedPullbackCLM_ae_of_ae line 83
  8. lemma OAI.ScalarConductivity.sourceChildCoordinates_translate line 88
  9. lemma OAI.ScalarConductivity.sourceChildCoordinates_map_volume line 95
  10. lemma OAI.ScalarConductivity.sourceChildCoordinates_quasi line 109
  11. def OAI.ScalarConductivity.sourceChildPullbackCLM line 115
  12. lemma OAI.ScalarConductivity.sourceChildPullbackCLM_ae line 120