OAI/Analysis/Conductivity/Fourier/CascadePeriodicity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.angularInteger line 13
  2. lemma OAI.ScalarConductivity.angularShift_apply line 15
  3. lemma OAI.ScalarConductivity.sin_int_angular_shift line 19
  4. lemma OAI.ScalarConductivity.cos_int_angular_shift line 27
  5. lemma OAI.ScalarConductivity.cascadeTerm_angularPeriodic line 35
  6. lemma OAI.ScalarConductivity.cascadeValue_angularPeriodic line 44
  7. lemma OAI.ScalarConductivity.crossingTensor_angularPeriodic line 51
  8. lemma OAI.ScalarConductivity.angularShift_dilation line 67
  9. lemma OAI.ScalarConductivity.cascadeStageTensor_angularPeriodic line 85
  10. lemma OAI.ScalarConductivity.cascadeTensor_angularPeriodic line 98
  11. lemma OAI.ScalarConductivity.cascadeValue_one_angularPeriodic line 110
  12. lemma OAI.ScalarConductivity.cascadeTensor_one_angularPeriodic line 114
  13. lemma OAI.ScalarConductivity.finiteEndingValue_angularPeriodic line 118
  14. lemma OAI.ScalarConductivity.finiteEndingTensor_angularPeriodic line 134