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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The horizontal part of the autonomous suspension is the Hamiltonian field of the planar slice at its current spatial phase.

  1. def OAI.ForcedComputation.planeInclusion line 14
  2. theorem OAI.ForcedComputation.planeInclusion_basis line 18
  3. theorem OAI.ForcedComputation.atHeight_hasFDerivAt line 23
  4. theorem OAI.ForcedComputation.spatialD_slice line 31
  5. theorem OAI.ForcedComputation.suspensionField_atHeight line 43
  6. theorem OAI.ForcedComputation.suspensionField_tracks_interval line 63

    Source documentation

    The exact planar slice equation determines each finite interval of the actual autonomous material flow.

    theorem suspensionField_tracks_interval {H : FieldExpr} (hH : H.Valid)
    (hP : CubePeriodic 1 (SpatialExpression.spatialValue H))
    {ψ : ℝ → Plane} {Φ : ℝ → Space → Space} {a b : ℝ} (x : Space)
    (hc : ContinuousOn (suspensionPath ψ) (Icc a b))
    (hp : suspensionPath ψ a = Φ a x)
    (hψ : ∀ s ∈ Ico a b, HasDerivAt ψ
      (PlanarHamiltonian.field (fun Y => SpatialExpression.spatialValue H (atHeight Y s))
        (ψ s)) s)
    (hg : ∀ s ∈ Ico a b, unitSpatialClock (ψ s) = 1)
    (hΦ : IsMaterialFlow 1 (fun y => SpatialExpression.suspensionField H y.2) Φ) :
    EqOn (fun s => Φ s x) (suspensionPath ψ) (Icc a b) := by
…

    Mentions: OAI.ForcedComputation.SpatialExpression.spatialValue, OAI.ForcedComputation.suspensionPath, OAI.ForcedComputation.PlanarHamiltonian.field, OAI.ForcedComputation.unitSpatialClock, OAI.ForcedComputation.SpatialExpression.suspensionField