The actual transverse forward operator on raw packet fields

The returned velocity and normalized pressure come from the constructed supported cylinder solution. All source-frame hypotheses are discharged by the deformation data. This module covers the forward interval, with genuine prescribed initial coordinates; the zero initial datum gives the forced operator used when t₀ = 0.

noncomputable def EulerTransversePacketProvider.Forcing.vector {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : EulerPacketProfileRecursion.VectorField

Vector as an element of VectorField.

Equations

• G.vector I z = EulerSourceCylinderClassical.field P D.support ⋯ ⋯ D.T ⋯ D.frame D.frameDerivative D.frameLower ⋯ ⋯ G.path I.value ⋯ ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

noncomputable def EulerTransversePacketProvider.Forcing.vectorDerivative {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : EulerPacketProfileRecursion.VectorField

Vector derivative as an element of VectorField.

Equations

• G.vectorDerivative I z = EulerSourceCylinderClassical.derivativeField P D.support ⋯ ⋯ D.T ⋯ D.frame D.frameDerivative D.frameLower ⋯ ⋯ G.path I.value ⋯ ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

noncomputable def EulerTransversePacketProvider.Forcing.scalar {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : EulerPacketProfileRecursion.ScalarField

Scalar as an element of ScalarField.

Equations

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

theorem EulerTransversePacketProvider.Forcing.vector_hasDerivWithinAt {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivWithinAt (fun (r : ℝ) => G.vector I (r, x, θ)) (G.vectorDerivative I (↑t, x, θ)) (Set.Icc 0 D.T) ↑t

theorem EulerTransversePacketProvider.Forcing.equation {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.vectorDerivative I (↑t, x, θ) + (D.strain (↑t, x, θ)) (G.vector I (↑t, x, θ)) + deriv (fun (s : ℝ) => G.scalar I (↑t, x, s)) θ • D.normalField (↑t, x, θ) = raw (↑t, x, θ)

The literal transverse equation, including its constructed angular pressure.

theorem EulerTransversePacketProvider.Forcing.vector_tangent {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : inner ℝ (D.normalField (t, x, θ)) (G.vector I (t, x, θ)) = 0

theorem EulerTransversePacketProvider.Forcing.scalar_normalized {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, G.scalar I (t, x, θ) = 0

theorem EulerTransversePacketProvider.Forcing.vector_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, G.vector I (t, x, θ) = 0

theorem EulerTransversePacketProvider.Forcing.vector_spatial_smooth {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => G.vector I (t, y)

theorem EulerTransversePacketProvider.Forcing.vectorDerivative_spatial_smooth {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => G.vectorDerivative I (t, y)

theorem EulerTransversePacketProvider.Forcing.scalar_spatial_smooth {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => G.scalar I (t, y)

theorem EulerTransversePacketProvider.Forcing.vector_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : G.vector I (t, x, θ) = 0

theorem EulerTransversePacketProvider.Forcing.scalar_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : G.scalar I (t, x, θ) = 0

theorem EulerTransversePacketProvider.Forcing.vector_periodic {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) : Function.Periodic (fun (θ : ℝ) => G.vector I (t, x, θ)) P

theorem EulerTransversePacketProvider.Forcing.scalar_periodic {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) : Function.Periodic (fun (θ : ℝ) => G.scalar I (t, x, θ)) P

noncomputable def EulerTransversePacketProvider.highSolve {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (P : ℝ) [Fact (0 < P)] (D : Data U) (I : InitialData P D) (raw : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField × EulerPacketProfileRecursion.ScalarField

A total raw-field map backed by the actual forward solution on its admissible domain.

Equations

• EulerTransversePacketProvider.highSolve P D I raw = if h : Nonempty (EulerTransversePacketProvider.Forcing P D raw) then have G := Classical.choice h; (G.vector I, G.scalar I) else (0, 0)

theorem EulerTransversePacketProvider.highSolve_of_admissible {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : Data U) (I : InitialData P D) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing P D raw)) : highSolve P D I raw = ((Classical.choice h).vector I, (Classical.choice h).scalar I)

theorem EulerTransversePacketProvider.highSolve_contract {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : Data U) (I : InitialData P D) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing P D raw)) : ∃ (a_t : EulerPacketProfileRecursion.VectorField), (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), HasDerivWithinAt (fun (r : ℝ) => (highSolve P D I raw).1 (r, x, θ)) (a_t (↑t, x, θ)) (Set.Icc 0 D.T) ↑t) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), a_t (↑t, x, θ) + (D.strain (↑t, x, θ)) ((highSolve P D I raw).1 (↑t, x, θ)) + deriv (fun (s : ℝ) => (highSolve P D I raw).2 (↑t, x, s)) θ • D.normalField (↑t, x, θ) = raw (↑t, x, θ)) ∧ (∀ (t : ℝ), ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => (highSolve P D I raw).1 (t, y)) ∧ (∀ (t : ℝ), ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => (highSolve P D I raw).2 (t, y)) ∧ ∀ (t : ℝ) (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, (highSolve P D I raw).2 (t, x, θ) = 0