OAI/Analysis/Conductivity/Fourier/CollarAngularInverse.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.complexUnitAngle line 11
  2. lemma OAI.ScalarConductivity.measurable_complexUnitAngle line 13
  3. lemma OAI.ScalarConductivity.fourier_complexUnitAngle line 17
  4. lemma OAI.ScalarConductivity.complexUnitAngle_fourier line 24
  5. lemma OAI.ScalarConductivity.complexUnitAngle_pos_mul line 33
  6. lemma OAI.ScalarConductivity.rectangularRay_max line 37
  7. lemma OAI.ScalarConductivity.rectangularRay_first_abs line 44
  8. lemma OAI.ScalarConductivity.sourceAngular_radius_pos line 49
  9. lemma OAI.ScalarConductivity.sourceAngular_radial line 59
  10. lemma OAI.ScalarConductivity.sourceAngular_time line 75
  11. def OAI.ScalarConductivity.sourceComplexDirections line 88
  12. def OAI.ScalarConductivity.sourcePhysicalAngles line 92
  13. lemma OAI.ScalarConductivity.continuous_sourceComplexDirections line 95
  14. lemma OAI.ScalarConductivity.measurable_sourcePhysicalAngles line 100
  15. lemma OAI.ScalarConductivity.sourceComplexDirections_angular line 106
  16. lemma OAI.ScalarConductivity.sourcePhysicalAngles_angular line 125