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

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The compact planar interpretation of the finite scalar program. Its time-periodic Hamiltonian has one common compact support inside the open unit square, and generates a smooth divergence-free, zero-mean field.

  1. def OAI.ForcedComputation.PlanarHamiltonian.periodicHamiltonian line 14
  2. def OAI.ForcedComputation.PlanarHamiltonian.periodicVelocity line 18
  3. def OAI.ForcedComputation.PlanarHamiltonian.commonSupport line 21
  4. theorem OAI.ForcedComputation.PlanarHamiltonian.commonSupport_compact line 24
  5. theorem OAI.ForcedComputation.PlanarHamiltonian.commonSupport_in_unit line 28
  6. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicHamiltonian_smooth line 43
  7. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicHamiltonian_slice_smooth line 51
  8. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicHamiltonian_periodic line 57
  9. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicHamiltonian_support line 70
  10. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicVelocity_eq_sum line 92
  11. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicVelocity_smooth line 101
  12. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicVelocity_periodic line 115
  13. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicVelocity_properties line 123
  14. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicPulse_on_unit line 135
  15. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicHamiltonian_on_unit line 144
  16. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicVelocity_on_unit line 152
  17. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicPulse_zero_near_zero line 161
  18. theorem OAI.ForcedComputation.PlanarHamiltonian.periodicVelocity_zero_near_zero line 196