OAI/Analysis/Conductivity/Fourier/TorusFlatMode.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.flat_proj_norm line 12
  2. def OAI.ScalarConductivity.torusAngular line 18
  3. lemma OAI.ScalarConductivity.torusAngular_norm line 21
  4. def OAI.ScalarConductivity.flatMode line 27
  5. lemma OAI.ScalarConductivity.flatMode_smooth line 30
  6. lemma OAI.ScalarConductivity.axial_exp_iterated_bound line 35
  7. lemma OAI.ScalarConductivity.angular_cos_iterated_bound line 50
  8. lemma OAI.ScalarConductivity.flatMode_iterated_bound line 59
  9. lemma OAI.ScalarConductivity.flatMode_derivative_summable line 80
  10. def OAI.ScalarConductivity.flatPhaseMode line 94
  11. lemma OAI.ScalarConductivity.flatPhaseMode_smooth line 97
  12. lemma OAI.ScalarConductivity.angular_phase_iterated_bound line 102
  13. lemma OAI.ScalarConductivity.flatPhaseMode_iterated_bound line 112
  14. lemma OAI.ScalarConductivity.weighted_phase_iterated_bound line 133
  15. lemma OAI.ScalarConductivity.flatPhaseMode_translation line 143