OAI/Analysis/Conductivity/Fourier/AngularFourierConjugacy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.normalizedAngularTensor_quadratic line 12
  2. lemma OAI.ScalarConductivity.angular_vecMul_zero line 23
  3. lemma OAI.ScalarConductivity.angular_vecMul_one line 27
  4. lemma OAI.ScalarConductivity.angular_vecMul_inverse line 31
  5. lemma OAI.ScalarConductivity.torusQuadratic_angular_conjugacy line 46
  6. lemma OAI.ScalarConductivity.torusRate_angular_conjugacy line 54
  7. def OAI.ScalarConductivity.angularNormalizedLift line 62
  8. lemma OAI.ScalarConductivity.torusAngular_normalizedLift line 66
  9. theorem OAI.ScalarConductivity.flatPhaseMode_angular_conjugacy line 75
  10. def OAI.ScalarConductivity.angularInverseMatrix line 93
  11. lemma OAI.ScalarConductivity.angular_mul_inverse line 96
  12. lemma OAI.ScalarConductivity.angular_inverse_mul line 103
  13. def OAI.ScalarConductivity.angularFrequencyEquiv line 110
  14. lemma OAI.ScalarConductivity.angularFrequencyEquiv_apply line 121
  15. lemma OAI.ScalarConductivity.angularFrequencyEquiv_symm_vecMul line 124
  16. theorem OAI.ScalarConductivity.flatFourier_angular_conjugacy line 129
  17. lemma OAI.ScalarConductivity.normalizedFourierCoefficients_angular_conjugacy line 143
  18. lemma OAI.ScalarConductivity.angular_conjugacy_gap line 155