The coefficient factory agrees with the physical velocity gradient and pressure Hessian. The only matching data are the literal Lagrangian velocity and acceleration laws, not separate coefficient identities.

noncomputable def EulerParentPacketFrames.Parent.position (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Position, given by x+G.displacement.field t x.

Equations

• G.position t x = x + (G.displacement.field t) x

@[simp]

theorem EulerParentPacketFrames.Parent.position_initial (G : Parent) (x : EulerSmoothLimit.Space) : G.position G.zeroTime x = x

theorem EulerParentPacketFrames.Parent.position_hasFDerivAt (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : HasFDerivAt (G.position t) (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (⇑(G.displacement.field t)) x) x

theorem EulerParentPacketFrames.Parent.position_frame (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : HasFDerivAt (G.position t) ((G.frame.field t) x) (G.ell • x)

theorem EulerParentPacketFrames.Parent.first_physical (G : Parent) (u : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (u t) x) (hvelocity : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.velocity.field t) x = u t (G.position t x)) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.first.field t) x = fderiv ℝ (u t) (G.position t (G.ell • x)) ∘SL (G.frame.field t) x

theorem EulerParentPacketFrames.Parent.second_physical (G : Parent) (force : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (force t) x) (hacceleration : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.acceleration.field t) x = -force t (G.position t x)) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.second.field t) x = -fderiv ℝ (force t) (G.position t (G.ell • x)) ∘SL (G.frame.field t) x

theorem EulerParentPacketFrames.Parent.strain_physical (G : Parent) (u : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (u t) x) (hvelocity : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.velocity.field t) x = u t (G.position t x)) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.strain.field t) x = fderiv ℝ (u t) (G.position t (G.ell • x))

theorem EulerParentPacketFrames.Parent.curvature_physical (G : Parent) (force : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (force t) x) (hacceleration : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.acceleration.field t) x = -force t (G.position t x)) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.curvature.field t) x = fderiv ℝ (force t) (G.position t (G.ell • x))

theorem EulerParentPacketFrames.Parent.initialStrain_physical (G : Parent) (u : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (u t) x) (hvelocity : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.velocity.field t) x = u t (G.position t x)) (x : EulerSmoothLimit.Space) : G.initialStrain.field x = fderiv ℝ (u G.zeroTime) (G.ell • x)

def EulerParentPacketFrames.Parent.lowBoundsOfPhysical (G : Parent) (u force : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (u t) x) (hf : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), DifferentiableAt ℝ (force t) x) (hvelocity : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.velocity.field t) x = u t (G.position t x)) (hacceleration : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.acceleration.field t) x = -force t (G.position t x)) (Be Bc L r K : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrq : r ≤ 1 / 4) (hK : 0 ≤ K) (hexterior : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((fderiv ℝ (u G.zeroTime) x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((fderiv ℝ (u G.zeroTime) x) v) v) (hpressure : ∀ (t : ↑(Set.Icc 0 G.T)) (x v : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (force t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (G.T ^ 2 / 2) + Be * G.T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * G.T ≤ 1 / 2) : LowBounds G

The source low-order hypotheses follow from the actual physical gradient at time zero and the actual physical pressure-force derivative.

Equations

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