Classical constraints of the actual mean packet provider

The inverse-frame velocity is the smooth representative of the constructed ordinary solenoidal coordinate velocity. Its divergence therefore vanishes pointwise. The actual initial boundary condition supplies compact support.

noncomputable def EulerMeanPacketProvider.Forcing.coordinateOrdinaryPath {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2)

The actual solenoidal coordinate velocity, regarded in ordinary L².

Equations

• G.coordinateOrdinaryPath = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 D.T)) EulerMeanSolenoidal.solenoidalSpace.subtypeL) G.solution.coordinateVelocityPath

@[simp]

theorem EulerMeanPacketProvider.Forcing.coordinateOrdinaryPath_apply {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) : G.coordinateOrdinaryPath t = ↑(G.solution.velocity ↑t)

theorem EulerMeanPacketProvider.Forcing.coordinateOrdinaryPath_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T a) G.coordinateOrdinaryPath

theorem EulerMeanPacketProvider.Forcing.inverse_velocityPath {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) : (D.opInv t) (G.velocityPath t) = G.coordinateOrdinaryPath t

The inverse-frame field is the actual solenoidal coordinate class.

theorem EulerMeanPacketProvider.Forcing.inverse_vector_eq_coordinate {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (D.inverseFrame (↑t, x, θ)) (G.vector (↑t, x, θ)) = EulerMeanScalarPressure.pathRepresentative D.T G.coordinateOrdinaryPath ⋯ t x

This equality identifies the raw inverse-frame velocity pointwise.

theorem EulerMeanPacketProvider.Forcing.inverse_vector_divergence {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => (D.inverseFrame (↑t, y, θ)) (G.vector (↑t, y, θ))) x = 0

The source's divergence constraint holds as an ordinary pointwise derivative.

theorem EulerMeanPacketProvider.Forcing.inverse_vector_smooth {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (θ : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space) => (D.inverseFrame (↑t, y, θ)) (G.vector (↑t, y, θ))

theorem EulerMeanPacketProvider.Forcing.initial_vector_ae {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (θ : ℝ) : (fun (x : EulerSmoothLimit.Space) => G.vector (0, x, θ)) =ᵐ[MeasureTheory.volume] ↑↑(D.L • (EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff D.ℓ ⋯)) ↑(G.solution.label 0))

The initial raw velocity is the actual localized boundary value.

theorem EulerMeanPacketProvider.Forcing.initial_vector_support {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (θ : ℝ) : (tsupport fun (x : EulerSmoothLimit.Space) => G.vector (0, x, θ)) ⊆ {x : EulerSmoothLimit.Space | ‖D.ℓ • x‖ ≤ 2}

The initial support is contained in the source's scaled radius-two ball.

theorem EulerMeanPacketProvider.Forcing.initial_vector_compact {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (θ : ℝ) : HasCompactSupport fun (x : EulerSmoothLimit.Space) => G.vector (0, x, θ)

theorem EulerMeanPacketProvider.Forcing.vector_joint_continuous {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : Continuous fun (z : ↑(Set.Icc 0 D.T) × EulerSmoothLimit.Space × ℝ) => G.vector (↑z.1, z.2)

The time-space representative is jointly continuous on the actual interval.