OAI/Analysis/Conductivity/Fourier/CylinderModeGreen.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.flatCylinderEnergy line 15
2. lemma OAI.ScalarConductivity.flatCylinderEnergy_continuous_left line 20
3. lemma OAI.ScalarConductivity.flatCylinderEnergy_continuous_right line 25
4. lemma OAI.ScalarConductivity.cylinderMode_inner line 30
5. def OAI.ScalarConductivity.smoothCylinderModeJet line 40
6. lemma OAI.ScalarConductivity.flatCylinderEnergy_distinct_modes line 47
7. lemma OAI.ScalarConductivity.torusRate_sq_of_lower line 54
8. lemma OAI.ScalarConductivity.flatCylinderEnergy_same_mode line 60
9. theorem OAI.ScalarConductivity.flatCylinder_mode_green line 79