OAI/Analysis/Conductivity/Fourier/FourierPairFlux.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.torusCellIntegral_congr_slice line 14
  2. theorem OAI.ScalarConductivity.fourier_pair_boundary_flux line 22
  3. lemma OAI.ScalarConductivity.flatFourier_add line 74
  4. lemma OAI.ScalarConductivity.flatFourier_single line 83
  5. lemma OAI.ScalarConductivity.flatFourier_zero line 93
  6. lemma OAI.ScalarConductivity.flatFourier_const_mul line 96
  7. lemma OAI.ScalarConductivity.flatFourier_translation line 100
  8. lemma OAI.ScalarConductivity.translated_fourier_coeff_bound line 109
  9. def OAI.ScalarConductivity.normalizedFourierCoefficients line 124
  10. lemma OAI.ScalarConductivity.normalizedFourierCoefficients_zero_iff line 127
  11. lemma OAI.ScalarConductivity.normalizedFourierCoefficients_bound line 132
  12. lemma OAI.ScalarConductivity.flatFourier_normalized_translation line 144
  13. lemma OAI.ScalarConductivity.pureWallMode_eq_flatPhaseMode line 159
  14. lemma OAI.ScalarConductivity.single_fourier_coeff_bound line 163