OAI/Analysis/Conductivity/Fourier/TorusNonresonance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.torusQuadratic line 13
2. lemma OAI.ScalarConductivity.real_outer_pair_injective line 16
3. def OAI.ScalarConductivity.torusResonanceForm line 36
4. lemma OAI.ScalarConductivity.torusResonance_proper line 41
5. theorem OAI.ScalarConductivity.exists_nonresonant_angular_tensor line 62
6. lemma OAI.ScalarConductivity.torusQuadratic_sublevel_finite line 102
7. lemma OAI.ScalarConductivity.torusQuadratic_pos line 125
8. lemma OAI.ScalarConductivity.torus_modes_have_first line 140
9. theorem OAI.ScalarConductivity.torus_leading_pair_gap line 153