OAI/Analysis/Conductivity/Fourier/AngularIntegratedTrace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.continuous_sourceAngular line 11
2. lemma OAI.ScalarConductivity.continuous_parametric_interval line 17
3. lemma OAI.ScalarConductivity.continuous_torus_interval_swap line 24
4. def OAI.ScalarConductivity.sourcePhysicalEnergy line 33
5. lemma OAI.ScalarConductivity.sourcePhysicalEnergy_nonneg line 36
6. lemma OAI.ScalarConductivity.continuous_sourcePhysicalEnergy line 39
7. lemma OAI.ScalarConductivity.integrate_torus_interval_bound line 44
8. theorem OAI.ScalarConductivity.sourceAngular_integrated_trace line 56