OAI/Analysis/Conductivity/Sobolev/VoltageOriginalH10.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.voltageValueComponentJet line 15
  2. def OAI.ScalarConductivity.voltageGradientComponentJet line 21
  3. def OAI.ScalarConductivity.voltageComponentJetCLM line 27
  4. lemma OAI.ScalarConductivity.voltageComponentJetCLM_ae line 34
  5. def OAI.ScalarConductivity.voltageOriginalJetCLM line 50
  6. lemma OAI.ScalarConductivity.voltageOriginalJetCLM_ae line 58
  7. lemma OAI.ScalarConductivity.voltage_component_smoothJet line 81
  8. lemma OAI.ScalarConductivity.voltageOriginalJetCLM_compact line 106
  9. theorem OAI.ScalarConductivity.voltageOriginalJetCLM_zeroTrace line 147
  10. theorem OAI.ScalarConductivity.voltage_original_H10_extension line 156