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

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Local two-dimensional Hamiltonian pulses for the stationary-forcing construction. The fields act on the actual plane, including throughout their cutoff collars.

  1. def OAI.ForcedComputation.PlanarHamiltonian.basis line 17
  2. def OAI.ForcedComputation.PlanarHamiltonian.spatialD line 19
  3. def OAI.ForcedComputation.PlanarHamiltonian.field line 22
  4. def OAI.ForcedComputation.PlanarHamiltonian.divergence line 26
  5. theorem OAI.ForcedComputation.PlanarHamiltonian.basis_apply line 29
  6. theorem OAI.ForcedComputation.PlanarHamiltonian.spatialD_smooth line 32
  7. theorem OAI.ForcedComputation.PlanarHamiltonian.spatialD_comm line 36
  8. theorem OAI.ForcedComputation.PlanarHamiltonian.field_smooth line 48
  9. theorem OAI.ForcedComputation.PlanarHamiltonian.field_tsupport line 53
  10. theorem OAI.ForcedComputation.PlanarHamiltonian.field_compactSupport line 59
  11. theorem OAI.ForcedComputation.PlanarHamiltonian.field_divergence line 63
  12. theorem OAI.ForcedComputation.PlanarHamiltonian.spatialD_integral_eq_zero line 81

    Source documentation

    Every compactly supported smooth Hamiltonian has zero average velocity.

    theorem spatialD_integral_eq_zero {H : Plane → ℝ} (hH : ContDiff ℝ ∞ H)
    (hc : HasCompactSupport H) (j : Fin 2) : ∫ x, spatialD j H x = 0 := by
…

    Mentions: OAI.ForcedComputation.PlanarHamiltonian.spatialD

  13. theorem OAI.ForcedComputation.PlanarHamiltonian.field_integral_eq_zero line 98
  14. theorem OAI.ForcedComputation.PlanarHamiltonian.field_congr_of_eventuallyEq line 106
  15. theorem OAI.ForcedComputation.PlanarHamiltonian.field_cutoff_plateau line 111
  16. def OAI.ForcedComputation.PlanarHamiltonian.translationPotential line 118
  17. theorem OAI.ForcedComputation.PlanarHamiltonian.translationPotential_smooth line 122
  18. theorem OAI.ForcedComputation.PlanarHamiltonian.field_translation line 126
  19. def OAI.ForcedComputation.PlanarHamiltonian.translationPath line 133
  20. theorem OAI.ForcedComputation.PlanarHamiltonian.translationPath_hasDerivAt line 135
  21. theorem OAI.ForcedComputation.PlanarHamiltonian.translationPath_cutoff_ode line 140
  22. theorem OAI.ForcedComputation.PlanarHamiltonian.translationPath_endpoints line 148
  23. def OAI.ForcedComputation.PlanarHamiltonian.horizontalPotential line 155

    Source documentation

    Polynomial Hamiltonians for the elementary shears. The coefficients are rational whenever the instruction and parking point are rational.

    def horizontalPotential (c : Plane) (a : ℝ) (x : Plane) : ℝ :=
…
  24. def OAI.ForcedComputation.PlanarHamiltonian.verticalPotential line 160
  25. theorem OAI.ForcedComputation.PlanarHamiltonian.horizontalPotential_smooth line 165
  26. theorem OAI.ForcedComputation.PlanarHamiltonian.verticalPotential_smooth line 170
  27. theorem OAI.ForcedComputation.PlanarHamiltonian.field_horizontal line 175
  28. theorem OAI.ForcedComputation.PlanarHamiltonian.field_vertical line 183
  29. def OAI.ForcedComputation.PlanarHamiltonian.horizontalPath line 191
  30. def OAI.ForcedComputation.PlanarHamiltonian.verticalPath line 194
  31. theorem OAI.ForcedComputation.PlanarHamiltonian.horizontalPath_hasDerivAt line 197
  32. theorem OAI.ForcedComputation.PlanarHamiltonian.verticalPath_hasDerivAt line 210
  33. def OAI.ForcedComputation.PlanarHamiltonian.fourShearPotential line 225

    Source documentation

    The four successive polynomial Hamiltonians have reciprocal-diagonal composition. This avoids logarithms in a finite effective force program.

    def fourShearPotential (μ : ℝ) (c : Plane) : Fin 4 → Plane → ℝ :=
…
  34. def OAI.ForcedComputation.PlanarHamiltonian.fourShearPath line 229
  35. theorem OAI.ForcedComputation.PlanarHamiltonian.fourShearPotential_smooth line 232
  36. theorem OAI.ForcedComputation.PlanarHamiltonian.fourShearPath_hasDerivAt line 237
  37. theorem OAI.ForcedComputation.PlanarHamiltonian.fourShearPath_cutoff_ode line 252
  38. theorem OAI.ForcedComputation.PlanarHamiltonian.fourShearPath_endpoints line 261
  39. theorem OAI.ForcedComputation.PlanarHamiltonian.fourShearPath_final line 268
  40. theorem OAI.ForcedComputation.PlanarHamiltonian.fourShearPath_bound line 277