StationaryBundle.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The complete analytic bundle for a smooth periodic autonomous field started from rest. The finite planar processor is supplied separately.

structure OAI.ForcedComputation.StationaryFluidProperties line 13
theorem OAI.ForcedComputation.startup_bundle line 30

theorem OAI.ForcedComputation.startup_bundle_with_flow line 54

Source documentation

Startup preserves the actual autonomous material trajectories, with an onto nonnegative clock. The statement applies to every chosen particle and observation set at once.

theorem startup_bundle_with_flow {L ν : ℝ} (hL : 0 < L) (hν : 0 ≤ ν)
    {W : Space → Space} (hW : ContDiff ℝ ∞ W)
    (hp : CubePeriodic L W) (hd : ∀ x, divergence W x = 0)
    (hm : (∫ x in fundamentalCube L, W x) = 0) :
    StationaryFluidProperties L ν (rampVelocity startupRamp W) ∧
      ∃ Φ : ℝ → Space → Space,
        IsMaterialFlow L (fun y => W y.2) Φ ∧
        IsMaterialFlow L (rampVelocity startupRamp W)
          (fun t x => Φ (accumulatedClock startupRamp t) x) ∧
        ∀ x O, Reaches (fun t => Φ (accumulatedClock startupRamp t) x) O ↔
          Reaches (fun t => Φ t x) O :=
…

Mentions: OAI.ForcedComputation.StationaryFluidProperties, OAI.ForcedComputation.rampVelocity, OAI.ForcedComputation.startupRamp, OAI.ForcedComputation.accumulatedClock, OAI.ForcedComputation.Reaches