OAI/Analysis/Conductivity/Fourier/PeriodicBandCompactness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.exists_angular_translate_mem_box line 12
2. lemma OAI.ScalarConductivity.periodic_band_nonzero_eventually line 37
3. lemma OAI.ScalarConductivity.pairMinor_wallCoordinatePair line 62
4. lemma OAI.ScalarConductivity.direction_boxCoordinates line 67
5. lemma OAI.ScalarConductivity.pureMode_pairMinor_noncritical line 74
6. lemma OAI.ScalarConductivity.familyDirection_smooth line 97
7. lemma OAI.ScalarConductivity.AngularPeriodic.direction line 104
8. theorem OAI.ScalarConductivity.periodic_pure_mode_rank_eventually line 110
9. theorem OAI.ScalarConductivity.elliptic_fourier_matching_regular line 136