OAI/Analysis/Conductivity/Fourier/TorusFourierTranslation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.mFourier_spatial_add line 20
2. lemma OAI.ScalarConductivity.mFourier_norm_one line 25
3. lemma OAI.ScalarConductivity.mFourierCoeff_translation line 29
4. def OAI.ScalarConductivity.torusCoordinateShift line 47
5. lemma OAI.ScalarConductivity.mFourier_coordinateShift line 50
6. lemma OAI.ScalarConductivity.mFourierCoeff_difference line 55
7. lemma OAI.ScalarConductivity.torus_fourier_difference_bessel line 65
8. lemma OAI.ScalarConductivity.torus_phase_difference_limit line 94
9. lemma OAI.ScalarConductivity.torus_difference_integral_bound line 106
10. lemma OAI.ScalarConductivity.torus_coordinate_fourier_bound line 121
11. theorem OAI.ScalarConductivity.torus_coordinate_fourier_summable line 145
12. lemma OAI.ScalarConductivity.torusCoordinateShift_norm line 152
13. lemma OAI.ScalarConductivity.torus_lipschitz_coordinate_bound line 161