OAI/Analysis/Conductivity/Sobolev/VoltageJetCompletion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ScalarConductivity.VoltageJetSpace line 13
  2. def OAI.ScalarConductivity.compactVoltageJets line 16
  3. lemma OAI.ScalarConductivity.voltageGradient_zero line 22
  4. lemma OAI.ScalarConductivity.voltageGradient_smul line 27
  5. lemma OAI.ScalarConductivity.compactVoltageJets_zero line 32
  6. lemma OAI.ScalarConductivity.compactVoltageJets_add line 39
  7. lemma OAI.ScalarConductivity.compactVoltageJets_smul line 55
  8. def OAI.ScalarConductivity.compactVoltageJetModule line 71
  9. def OAI.ScalarConductivity.zeroVoltageJets line 78
  10. instance OAI.ScalarConductivity.zeroVoltageJets_complete line 82
  11. lemma OAI.ScalarConductivity.zeroVoltageJets_poincare line 86
  12. def OAI.ScalarConductivity.zeroVoltageGradientMap line 98
  13. lemma OAI.ScalarConductivity.zeroVoltageGradientMap_closed_range line 102