OAI/Analysis/Conductivity/Fourier/AngularPeriodization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.angularShift line 12
  2. lemma OAI.ScalarConductivity.angularShift_zero line 14
  3. lemma OAI.ScalarConductivity.angularShift_add line 15
  4. lemma OAI.ScalarConductivity.angularShift_succ line 19
  5. def OAI.ScalarConductivity.angularPeriodize line 24
  6. def OAI.ScalarConductivity.AngularPeriodic line 27
  7. lemma OAI.ScalarConductivity.angularPeriodize_periodic line 31
  8. lemma OAI.ScalarConductivity.angular_translates_locallyFinite line 45
  9. lemma OAI.ScalarConductivity.angularPeriodize_smooth line 75
  10. lemma OAI.ScalarConductivity.angularPeriodize_local_sum line 83
  11. lemma OAI.ScalarConductivity.angularPeriodize_finite line 111
  12. lemma OAI.ScalarConductivity.angularPeriodize_fderiv line 116
  13. lemma OAI.ScalarConductivity.AngularPeriodic.fderiv line 139
  14. lemma OAI.ScalarConductivity.coordinateDivergence_comp_add line 145
  15. lemma OAI.ScalarConductivity.symmetricSource_congr_nhds line 152
  16. lemma OAI.ScalarConductivity.symmetricSource_finset_sum line 164
  17. lemma OAI.ScalarConductivity.symmetricSource_angular_translate line 179
  18. theorem OAI.ScalarConductivity.symmetricSource_angularPeriodize line 191
  19. lemma OAI.ScalarConductivity.angularPeriodize_symmetric line 215