OAI/Analysis/Conductivity/Sobolev/CylinderSobolevGraph.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ScalarConductivity.CylinderTraceAmbient line 11
  2. def OAI.ScalarConductivity.cylinderPolynomialGraphL line 14
  3. def OAI.ScalarConductivity.cylinderSobolevGraph line 19
  4. def OAI.ScalarConductivity.cylinderH1Space line 22
  5. instance OAI.ScalarConductivity.cylinderSobolevGraph_complete line 25
  6. instance OAI.ScalarConductivity.cylinderH1Space_complete line 29
  7. lemma OAI.ScalarConductivity.cylinderSobolevGraph_trace_bound line 32
  8. def OAI.ScalarConductivity.cylinderSobolevJetCLM line 52
  9. lemma OAI.ScalarConductivity.cylinderSobolevGraph_norm_bound line 56
  10. lemma OAI.ScalarConductivity.cylinderSobolevJet_antilipschitz line 73
  11. lemma OAI.ScalarConductivity.cylinderSobolevJet_mem_H1 line 78
  12. theorem OAI.ScalarConductivity.cylinderH1_unique_trace_graph line 89