OAI/Analysis/Conductivity/Flux/TorusCylinderGreenReal.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.continuous_memLp_finiteCylinder_general line 20
  2. lemma OAI.ScalarConductivity.torusPeriodicDescent_cylinderIntegral line 29
  3. theorem OAI.ScalarConductivity.torusCylinder_green_real line 38
  4. lemma OAI.ScalarConductivity.continuous_torusFluxComponent line 80
  5. def OAI.ScalarConductivity.cylinderFluxLp line 84
  6. lemma OAI.ScalarConductivity.cylinderFluxLp_ae line 88
  7. def OAI.ScalarConductivity.cylinderFluxPairL line 93
  8. lemma OAI.ScalarConductivity.cylinderFluxPairL_apply line 98
  9. lemma OAI.ScalarConductivity.cylinderFluxPairL_integral line 103
  10. def OAI.ScalarConductivity.torusFluxLp line 117
  11. lemma OAI.ScalarConductivity.torusFluxLp_ae line 121
  12. def OAI.ScalarConductivity.torusSpectralSynthesis line 125
  13. lemma OAI.ScalarConductivity.torusSpectralSynthesis_single line 129
  14. def OAI.ScalarConductivity.torusFluxPairL line 135
  15. lemma OAI.ScalarConductivity.torusFluxPairL_integral line 139
  16. lemma OAI.ScalarConductivity.torusFluxPairL_single line 150