OAI/Analysis/Conductivity/Geometry/FlatTorusPDE.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.expCosLinear line 13
2. lemma OAI.ScalarConductivity.expCosLinear_deriv line 15
3. lemma OAI.ScalarConductivity.expCosLinear_fderiv line 23
4. lemma OAI.ScalarConductivity.expCosLinear_hessian line 29
5. def OAI.ScalarConductivity.flatAxis line 60
6. def OAI.ScalarConductivity.flatTensorLaplacianCLM line 62
7. def OAI.ScalarConductivity.flatTensorLaplacian line 69
8. lemma OAI.ScalarConductivity.flatPhaseMode_harmonic line 72
9. lemma OAI.ScalarConductivity.weighted_flatPhaseMode_harmonic line 97
10. theorem OAI.ScalarConductivity.flatFourier_harmonic line 107