OAI/Analysis/Conductivity/Sources/CopiedScalarCoefficient.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.copiedScalarCoefficient line 15
  2. lemma OAI.ScalarConductivity.copiedScalarCoefficient_on line 19
  3. lemma OAI.ScalarConductivity.copiedScalarCoefficient_outside line 28
  4. lemma OAI.ScalarConductivity.copiedScalarCoefficient_measurable line 32
  5. lemma OAI.ScalarConductivity.copiedScalarCoefficient_bounds line 41
  6. lemma OAI.ScalarConductivity.copiedScalarCoefficient_one line 51
  7. lemma OAI.ScalarConductivity.copiedScalarCoefficient_collar line 57
  8. lemma OAI.ScalarConductivity.copiedScalarCoefficient_root line 67
  9. lemma OAI.ScalarConductivity.copiedScalarCoefficient_child line 75
  10. lemma OAI.ScalarConductivity.sourceChildEuclidean_inverse_quasi line 102
  11. lemma OAI.ScalarConductivity.sourceChild_inverse_ballae line 108
  12. def OAI.ScalarConductivity.SourceSupported line 114
  13. lemma OAI.ScalarConductivity.sourceSupported_iff line 117
  14. lemma OAI.ScalarConductivity.SourceSupported.add line 131
  15. lemma OAI.ScalarConductivity.SourceSupported.smul line 137
  16. lemma OAI.ScalarConductivity.childH10Transport_support line 143
  17. def OAI.ScalarConductivity.childZeroTransport line 162
  18. lemma OAI.ScalarConductivity.SourceSupported.child line 165
  19. lemma OAI.ScalarConductivity.childH10Transport_bounded line 170
  20. lemma OAI.ScalarConductivity.copied_child_energy line 179