OAI/Analysis/Conductivity/Fourier/TorusPeriodicDescent.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.torusPeriodicDescent line 20
2. lemma OAI.ScalarConductivity.torusAngles_scaled line 24
3. lemma OAI.ScalarConductivity.torusPeriodicDescent_real line 29
4. lemma OAI.ScalarConductivity.torusPeriodicDescent_angles line 38
5. lemma OAI.ScalarConductivity.isOpenMap_torusRealProjection line 47
6. lemma OAI.ScalarConductivity.torusRealProjection_surjective line 52
7. lemma OAI.ScalarConductivity.continuous_torusPeriodicDescent line 55
8. lemma OAI.ScalarConductivity.integral_unitTorus_iterated_general line 70
9. lemma OAI.ScalarConductivity.integral_unitCircle_haar_interval line 85
10. lemma OAI.ScalarConductivity.torusPeriodicDescent_integral line 90