OAI/Analysis/Conductivity/Variational/VoltageRecombination.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.voltageRecombine line 14
  2. def OAI.ScalarConductivity.fieldRecombine line 18
  3. lemma OAI.ScalarConductivity.voltageRecombine_apply line 30
  4. lemma OAI.ScalarConductivity.fieldRecombine_apply line 33
  5. lemma OAI.ScalarConductivity.voltageGradient_recombine line 37
  6. def OAI.ScalarConductivity.voltageJetRecombine line 50
  7. lemma OAI.ScalarConductivity.voltageJetRecombine_toLp line 55
  8. lemma OAI.ScalarConductivity.voltageJetRecombine_smooth line 80
  9. lemma OAI.ScalarConductivity.voltageJetRecombine_compact line 87
  10. theorem OAI.ScalarConductivity.voltageJetRecombine_H1 line 95
  11. theorem OAI.ScalarConductivity.voltageJetRecombine_H10 line 107
  12. lemma OAI.ScalarConductivity.fieldRecombine_inner line 117
  13. lemma OAI.ScalarConductivity.fieldRecombine_innerLp line 123
  14. theorem OAI.ScalarConductivity.voltageJetRecombine_cauchy line 133
  15. theorem OAI.ScalarConductivity.voltageJetRecombine_weak line 144
  16. theorem OAI.ScalarConductivity.voltageJetRecombine_constitution line 154
  17. theorem OAI.ScalarConductivity.scalar_voltage_recombine line 166
  18. lemma OAI.ScalarConductivity.voltageGradient_const line 188
  19. def OAI.ScalarConductivity.voltageConstantJet line 193
  20. lemma OAI.ScalarConductivity.voltageConstantJet_H1 line 197
  21. theorem OAI.ScalarConductivity.scalar_voltage_affine_recombine line 208
  22. lemma OAI.ScalarConductivity.voltageGradient_affine_recombine line 240
  23. lemma OAI.ScalarConductivity.voltageJetRecombine_affine_toLp line 249