OAI/Analysis/Conductivity/Fourier/TorusPoissonContinuous.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.poisson_series_norm_summable line 21
  2. def OAI.ScalarConductivity.torusPoissonContinuous line 32
  3. theorem OAI.ScalarConductivity.torusPoissonContinuous_toLp line 36
  4. lemma OAI.ScalarConductivity.torusPoissonContinuous_apply line 47
  5. def OAI.ScalarConductivity.torusAngles line 64
  6. lemma OAI.ScalarConductivity.mFourier_torusAngles line 67
  7. lemma OAI.ScalarConductivity.flatFourier_summable line 77
  8. lemma OAI.ScalarConductivity.complex_mode_real line 92
  9. def OAI.ScalarConductivity.torusRealContinuation line 102
  10. lemma OAI.ScalarConductivity.torusRealContinuation_eq line 105
  11. lemma OAI.ScalarConductivity.torusRealContinuation_smooth line 128