OAI/Analysis/Conductivity/Fourier/CylinderPoissonTrace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.spectralPoissonTrace line 12
2. lemma OAI.ScalarConductivity.spectralTraceSingle_hasSum line 23
3. lemma OAI.ScalarConductivity.cylinderPolynomialJetL_single line 48
4. lemma OAI.ScalarConductivity.cylinderPolynomialTraceL_single line 54
5. lemma OAI.ScalarConductivity.endPoissonModeJet_mem_trace_graph line 60
6. theorem OAI.ScalarConductivity.endPoissonJet_mem_trace_graph line 77