OAI/Analysis/Conductivity/Variational/CompactPhysicalCorrections.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ScalarConductivity.PhysicalSourcePair line 13
  2. def OAI.ScalarConductivity.CompactSmoothPair line 15
  3. def OAI.ScalarConductivity.PairSupported line 18
  4. def OAI.ScalarConductivity.physicalSourceMoment line 21
  5. lemma OAI.ScalarConductivity.CompactSmoothPair.zero line 26
  6. lemma OAI.ScalarConductivity.CompactSmoothPair.add line 27
  7. lemma OAI.ScalarConductivity.CompactSmoothPair.sub line 29
  8. lemma OAI.ScalarConductivity.CompactSmoothPair.integrable line 31
  9. lemma OAI.ScalarConductivity.CompactSmoothPair.torque_integrable line 33
  10. lemma OAI.ScalarConductivity.PairSupported.mono line 43
  11. lemma OAI.ScalarConductivity.PairSupported.zero line 45
  12. lemma OAI.ScalarConductivity.PairSupported.add line 46
  13. lemma OAI.ScalarConductivity.PairSupported.sub line 48
  14. lemma OAI.ScalarConductivity.physicalSourceMoment_zero line 52
  15. lemma OAI.ScalarConductivity.physicalSourceMoment_add line 55
  16. lemma OAI.ScalarConductivity.physicalSourceMoment_sub line 69
  17. def OAI.ScalarConductivity.PhysicallyCorrectable line 76
  18. lemma OAI.ScalarConductivity.symmetricSource_eq_of_weak line 81
  19. lemma OAI.ScalarConductivity.coordinateDivergence_add line 101
  20. lemma OAI.ScalarConductivity.symmetricSource_add line 112
  21. lemma OAI.ScalarConductivity.PhysicallyCorrectable.zero line 126
  22. lemma OAI.ScalarConductivity.PhysicallyCorrectable.add line 131
  23. lemma OAI.ScalarConductivity.RegularCorrectionBox.correct line 143