OAI/Analysis/Conductivity/Geometry/PhysicalCollarTrace.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.physicalRayConstant line 15
  2. lemma OAI.ScalarConductivity.physicalRayConstant_pos line 18
  3. lemma OAI.ScalarConductivity.sourceAngular_volume_in line 23
  4. theorem OAI.ScalarConductivity.sourceAngular_physical_trace_forward line 48
  5. theorem OAI.ScalarConductivity.sourceAngular_physical_trace_backward line 63
  6. def OAI.ScalarConductivity.sourcePairEquiv line 83
  7. def OAI.ScalarConductivity.sourcePairCLE line 91
  8. def OAI.ScalarConductivity.sourcePairMeasurable line 93
  9. lemma OAI.ScalarConductivity.sourcePairMeasurable_apply line 96
  10. lemma OAI.ScalarConductivity.sourcePair_volume line 98
  11. def OAI.ScalarConductivity.centralPhysical line 101
  12. lemma OAI.ScalarConductivity.centralPhysical_compact line 103
  13. lemma OAI.ScalarConductivity.sourcePair_central_image line 106
  14. lemma OAI.ScalarConductivity.integral_centralPhysical line 109
  15. lemma OAI.ScalarConductivity.linear_three_bound line 115
  16. lemma OAI.ScalarConductivity.sourcePair_energy line 140