OAI/Analysis/Conductivity/Variational/CentralEnergySpace.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ScalarConductivity.spectralTraceGraph_realInner line 14
  2. abbrev OAI.ScalarConductivity.CentralTraceFields line 17
  3. abbrev OAI.ScalarConductivity.CentralAmbient line 18
  4. instance OAI.ScalarConductivity.centralAmbientNormedSpace line 20
  5. instance OAI.ScalarConductivity.centralAmbientInnerProductSpace line 21
  6. def OAI.ScalarConductivity.centralEmbedL line 23
  7. def OAI.ScalarConductivity.centralAmbientD line 29
  8. def OAI.ScalarConductivity.centralAmbientT line 32
  9. def OAI.ScalarConductivity.centralAmbientM line 37
  10. def OAI.ScalarConductivity.centralAmbientOne line 40
  11. def OAI.ScalarConductivity.centralAmbientQ line 42
  12. lemma OAI.ScalarConductivity.centralAmbientD_embed line 45
  13. lemma OAI.ScalarConductivity.centralAmbientT_embed line 48
  14. lemma OAI.ScalarConductivity.centralAmbientM_one line 51
  15. lemma OAI.ScalarConductivity.centralAmbientD_one line 54
  16. lemma OAI.ScalarConductivity.centralAmbientWeight_one line 57
  17. lemma OAI.ScalarConductivity.centralAmbientQ_one line 61
  18. lemma OAI.ScalarConductivity.centralAmbientQ_apply line 64
  19. lemma OAI.ScalarConductivity.centralEmbed_norm line 67
  20. def OAI.ScalarConductivity.centralEnergySpace line 76
  21. instance OAI.ScalarConductivity.centralEnergySpace_complete line 79
  22. def OAI.ScalarConductivity.centralD line 82
  23. def OAI.ScalarConductivity.centralT line 85
  24. def OAI.ScalarConductivity.centralM line 89
  25. def OAI.ScalarConductivity.centralOne line 92
  26. def OAI.ScalarConductivity.centralAmbientJ line 99
  27. def OAI.ScalarConductivity.centralAmbientTraceL2 line 102
  28. lemma OAI.ScalarConductivity.centralAmbientTraceL2_embed line 107
  29. lemma OAI.ScalarConductivity.central_smooth_trace_jet_bound line 111
  30. lemma OAI.ScalarConductivity.central_graph_trace_jet_bound line 120
  31. lemma OAI.ScalarConductivity.central_graph_jet_injective line 133