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

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

A finite rational syntax for the planar Hamiltonian processor. Each pulse has one polynomial potential, one rational rectangle cutoff, and one rational time interval. Its analytic interpretation is the actual compact Hamiltonian field, including the cutoff collar.

  1. theorem OAI.ForcedComputation.PlanarHamiltonian.field_const_mul line 18
  2. theorem OAI.ForcedComputation.PlanarHamiltonian.field_sum line 25
  3. inductive OAI.ForcedComputation.PlanarHamiltonian.Primitive line 32
  4. def OAI.ForcedComputation.PlanarHamiltonian.Primitive.encoding line 37
  5. instance OAI.ForcedComputation.PlanarHamiltonian.(instance at line 50) line 50
  6. def OAI.ForcedComputation.PlanarHamiltonian.Primitive.potential line 52
  7. theorem OAI.ForcedComputation.PlanarHamiltonian.Primitive.potential_smooth line 57
  8. structure OAI.ForcedComputation.PlanarHamiltonian.Pulse line 69
  9. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.encoding line 76
  10. instance OAI.ForcedComputation.PlanarHamiltonian.(instance at line 82) line 82
  11. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.Valid line 84
  12. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.hamiltonian line 86
  13. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatial line 89
  14. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.velocity line 91
  15. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.hamiltonian_smooth line 94
  16. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.hamiltonian_compactSupport line 97
  17. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatial_smooth line 101
  18. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatial_compactSupport line 104
  19. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatial_tsupport line 107
  20. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.velocity_zero_of_notMem line 114
  21. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.velocity_zero_on_disjoint line 120
  22. theorem OAI.ForcedComputation.PlanarHamiltonian.collar_disjoint_of_gap line 127
  23. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.velocity_zero_of_gap line 144
  24. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.velocity_smooth line 150
  25. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.velocity_hamiltonian line 155
  26. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.velocity_divergence line 159
  27. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.velocity_integral line 167
  28. def OAI.ForcedComputation.PlanarHamiltonian.processorHamiltonian line 173
  29. def OAI.ForcedComputation.PlanarHamiltonian.processorVelocity line 176
  30. theorem OAI.ForcedComputation.PlanarHamiltonian.processorHamiltonian_smooth line 179
  31. theorem OAI.ForcedComputation.PlanarHamiltonian.processorHamiltonian_compactSupport line 185
  32. theorem OAI.ForcedComputation.PlanarHamiltonian.processorVelocity_eq_sum line 196
  33. theorem OAI.ForcedComputation.PlanarHamiltonian.processorVelocity_smooth line 205
  34. theorem OAI.ForcedComputation.PlanarHamiltonian.processorVelocity_properties line 214
  35. def OAI.ForcedComputation.PlanarHamiltonian.translationPulse line 224

    Source documentation

    The translation pulse used for both extraction and insertion.

    def translationPulse (R : RationalBox 2) (p : Fin 2 → ℚ) (δ a b : ℚ) : Pulse where
…

    Mentions: OAI.ForcedComputation.PlanarHamiltonian.Pulse

  36. theorem OAI.ForcedComputation.PlanarHamiltonian.translationPulse_realizes line 231