OAI/Analysis/Conductivity/Fourier/TorusLeadingRealMode.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.torusQuadratic_neg_mode line 12
  2. lemma OAI.ScalarConductivity.torusRate_neg_mode line 17
  3. lemma OAI.ScalarConductivity.torusAngular_neg_mode line 21
  4. lemma OAI.ScalarConductivity.polar_real_cosine line 27
  5. def OAI.ScalarConductivity.realTorusCoeff line 34
  6. lemma OAI.ScalarConductivity.realTorusCoeff_neg line 37
  7. lemma OAI.ScalarConductivity.realTorusCoeff_bound line 41
  8. lemma OAI.ScalarConductivity.realTorusCoeff_polar_mode line 54
  9. lemma OAI.ScalarConductivity.torusRealContinuation_polar line 69
  10. lemma OAI.ScalarConductivity.realTorusCoeff_zero_re line 96
  11. lemma OAI.ScalarConductivity.realTorusCoeff_polar_zero line 102
  12. lemma OAI.ScalarConductivity.realTorusCoeff_polar_neg line 107
  13. def OAI.ScalarConductivity.realTorusAmplitude line 117
  14. def OAI.ScalarConductivity.realTorusPhase line 120
  15. lemma OAI.ScalarConductivity.realTorusAmplitude_bound line 122
  16. lemma OAI.ScalarConductivity.torusRealContinuation_mean_free line 129
  17. lemma OAI.ScalarConductivity.torusRate_uniform_positive line 147
  18. lemma OAI.ScalarConductivity.torus_leading_rate_gap line 160