OAI/Analysis/Conductivity/Fourier/TorusPoissonFlow.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ScalarConductivity.TorusL2 line 15
2. lemma OAI.ScalarConductivity.poissonMultiplier_bound line 17
3. def OAI.ScalarConductivity.torusPoissonFlow line 23
4. lemma OAI.ScalarConductivity.torusPoissonFlow_coeff line 28
5. lemma OAI.ScalarConductivity.torusPoissonFlow_zero line 34
6. lemma OAI.ScalarConductivity.torusPoissonFlow_tendsto line 41
7. lemma OAI.ScalarConductivity.torusFourierCoeff_bound line 54
8. lemma OAI.ScalarConductivity.torusPoissonFlow_norm line 60