OAI/Analysis/Conductivity/Fourier/RectangularRayTrace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.rayDirection line 11
  2. def OAI.ScalarConductivity.rayDenominator line 14
  3. def OAI.ScalarConductivity.rectangularRay line 17
  4. lemma OAI.ScalarConductivity.rayDirection_unit line 20
  5. lemma OAI.ScalarConductivity.rayDirection_abs line 27
  6. lemma OAI.ScalarConductivity.rayDenominator_lower line 34
  7. lemma OAI.ScalarConductivity.continuous_rayDirection line 48
  8. lemma OAI.ScalarConductivity.continuous_rectangularRay line 55
  9. lemma OAI.ScalarConductivity.fourier_one_translation_bound line 65
  10. lemma OAI.ScalarConductivity.rayDirection_difference line 79
  11. lemma OAI.ScalarConductivity.rayDenominator_difference line 88
  12. lemma OAI.ScalarConductivity.rectangularRay_difference line 100