OAI/Analysis/Conductivity/Fourier/TorusFourierSmooth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.flatFourier line 11
2. lemma OAI.ScalarConductivity.axial_halfspace_open line 14
3. lemma OAI.ScalarConductivity.axial_halfspace_connected line 17
4. lemma OAI.ScalarConductivity.weighted_phase_halfspace_bound line 21
5. lemma OAI.ScalarConductivity.flatFourier_smooth_halfspace line 35
6. lemma OAI.ScalarConductivity.flatFourier_smooth line 47
7. lemma OAI.ScalarConductivity.flatFourier_iterated line 57
8. lemma OAI.ScalarConductivity.flatFourier_iterated_norm line 73