OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarPeriodicProperties.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Periodicity and zero mean for the planar torus interpretation of the Hamiltonian, with integration over its unit-square fundamental domain.

  1. def OAI.ForcedComputation.PlanePeriodic line 13
  2. theorem OAI.ForcedComputation.plane_opposite_faces line 16
  3. theorem OAI.ForcedComputation.integral_planar_periodic_derivative line 23
  4. theorem OAI.ForcedComputation.planar_field_mean_zero line 60
  5. theorem OAI.ForcedComputation.planar_field_periodic line 85
  6. theorem OAI.ForcedComputation.planar_slice_potential_smooth line 91
  7. theorem OAI.ForcedComputation.planar_slice_potential_periodic line 106
  8. theorem OAI.ForcedComputation.planarSlice_mean_zero line 119
  9. theorem OAI.ForcedComputation.planarSlice_smooth line 125
  10. theorem OAI.ForcedComputation.planarSlice_divergence line 129
  11. theorem OAI.ForcedComputation.planarSlice_spatial_periodic line 133
  12. theorem OAI.ForcedComputation.processor_slice_zero line 139
  13. theorem OAI.ForcedComputation.normalized_planar_zero_near_zero line 158