OAI/Analysis/Conductivity/Fourier/CylinderFourierComplete.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.cylinderL2_slice_memLp line 19
  2. lemma OAI.ScalarConductivity.torusFourierCoeff_norm_sq_le line 26
  3. def OAI.ScalarConductivity.cylinderCoefficient line 46
  4. lemma OAI.ScalarConductivity.cylinderCoefficient_aestronglyMeasurable line 49
  5. lemma OAI.ScalarConductivity.cylinderCoefficient_memLp line 54
  6. def OAI.ScalarConductivity.cylinderCoefficientLp line 63
  7. lemma OAI.ScalarConductivity.cylinderCoefficientLp_ae line 67
  8. lemma OAI.ScalarConductivity.cylinderMode_inner_coefficient line 72
  9. lemma OAI.ScalarConductivity.cylinderModes_total line 92
  10. theorem OAI.ScalarConductivity.cylinderFourier_surjective line 130
  11. def OAI.ScalarConductivity.cylinderFourierEquiv line 151
  12. lemma OAI.ScalarConductivity.cylinderCoefficient_fourier line 155
  13. lemma OAI.ScalarConductivity.cylinderFourierEquiv_symm_apply line 166
  14. theorem OAI.ScalarConductivity.cylinderCoefficient_hasSum line 173