The physical Euler evolution carried by a particle parent. Its acceleration law and the smoothness of its closed spatial slices are consequences of the actual flow identities, rather than extra premises.

Spatial smoothness of the actual physical particle inverse follows from its inverse identities and the genuine determinant-one Jacobian.

theorem EulerParentPacketFrames.ParticleInverse.hasFDerivAt {A : Parent} (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : HasFDerivAt (I.field t) ((A.inverse.field t) (A.ell⁻¹ • I.field t x)) x

theorem EulerParentPacketFrames.ParticleInverse.smooth {A : Parent} (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) : ContDiff ℝ (↑⊤) (I.field t)

structure EulerParentPacketFrames.Evolution (A : Parent) : Type

Evolution data, collecting inverse, velocity, pressure, force, force_continuous, velocity_match and their compatibility conditions.

• inverse : ParticleInverse A

  Inverse of Evolution, of type ParticleInverse A.

• velocity : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space

  Velocity field of Evolution, of type ℝ × Space → Space.

• pressure : ℝ × EulerSmoothLimit.Space → ℝ

  Pressure field of Evolution, of type ℝ × Space → ℝ.

• force : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space

  Force of Evolution, of type Icc (0 : ℝ) A.T → Space → Space.

• force_continuous : Continuous (Function.uncurry self.force)
• velocity_match (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (A.velocity.field t) x = self.velocity (↑t, A.position t x)
• velocity_differentiable (t : ℝ) : t ∈ Set.Ioo 0 A.T → ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ self.velocity (t, x)
• pressure_differentiable (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => self.pressure (↑t, y)) x
• pressure_gradient (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : gradient (fun (y : EulerSmoothLimit.Space) => self.pressure (↑t, y)) x = self.force t x
• momentum_zero (t : ℝ) : t ∈ Set.Ioo 0 A.T → ∀ (x : EulerSmoothLimit.Space), EulerLagrangian.momentumResidual self.velocity self.pressure (t, x) = 0
• divergence_zero (t : ℝ) : t ∈ Set.Ioo 0 A.T → ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => self.velocity (t, y)) x = 0

theorem EulerParentPacketFrames.Evolution.acceleration_match {A : Parent} (E : Evolution A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (A.acceleration.field t) x = -E.force t (A.position t x)

theorem EulerParentPacketFrames.Evolution.velocity_pullback {A : Parent} (E : Evolution A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : E.velocity (↑t, x) = (A.velocity.field t) (E.inverse.field t x)

theorem EulerParentPacketFrames.Evolution.force_pullback {A : Parent} (E : Evolution A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : E.force t x = -(A.acceleration.field t) (E.inverse.field t x)

theorem EulerParentPacketFrames.Evolution.velocity_smooth {A : Parent} (E : Evolution A) (t : ↑(Set.Icc 0 A.T)) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => E.velocity (↑t, x)

theorem EulerParentPacketFrames.Evolution.force_smooth {A : Parent} (E : Evolution A) (t : ↑(Set.Icc 0 A.T)) : ContDiff ℝ (↑⊤) (E.force t)

theorem EulerParentPacketFrames.Evolution.strain_eq {A : Parent} (E : Evolution A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (A.strain.field t) x = fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) (A.position t (A.ell • x))

theorem EulerParentPacketFrames.Evolution.curvature_eq {A : Parent} (E : Evolution A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (A.curvature.field t) x = fderiv ℝ (E.force t) (A.position t (A.ell • x))

def EulerParentPacketFrames.Evolution.restrictTime {A : Parent} (E : Evolution A) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) : Evolution (A.restrictTime S hS hST)

Restrict time, bundling inverse, velocity, pressure, force and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.