The complete transverse history/forward field as a genuine cylinder path

All raw fields are canonical continuous representatives of the constructed L² paths. Restriction recovers the actual history and forward solutions.

noncomputable def EulerTransversePacketJoin.vector {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : EulerPacketProfileRecursion.VectorField

Vector, defined pointwise by pointField P (velocityPath τ hτ hτT B G) (velocityPath_orbit τ hτ hτT B G) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• EulerTransversePacketJoin.vector τ hτ hτT B G z = EulerCylinderSmoothOrbit.pointField P (EulerTransversePacketJoin.velocityPath τ hτ hτT B G) ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

noncomputable def EulerTransversePacketJoin.vectorDerivative {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : EulerPacketProfileRecursion.VectorField

Vector derivative, defined pointwise by pointField P (derivativePath τ hτ hτT B G) (derivativePath_orbit τ hτ hτT B G) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• EulerTransversePacketJoin.vectorDerivative τ hτ hτT B G z = EulerCylinderSmoothOrbit.pointField P (EulerTransversePacketJoin.derivativePath τ hτ hτT B G) ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

noncomputable def EulerTransversePacketJoin.scalar {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : EulerPacketProfileRecursion.ScalarField

Scalar, defined pointwise by scalarPointField P (pressurePath τ hτ hτT B G) (pressurePath_orbit τ hτ hτT B G) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• EulerTransversePacketJoin.scalar τ hτ hτT B G z = EulerCylinderScalarPrimitive.scalarPointField P (EulerTransversePacketJoin.pressurePath τ hτ hτT B G) ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

noncomputable def EulerTransversePacketJoin.vectorField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : EulerPacketCylinderField.Field P D.T (vector τ hτ hτT B G)

Vector field, bundling path, orbit, raw_eq.

Equations

• EulerTransversePacketJoin.vectorField τ hτ hτT B G = { path := EulerTransversePacketJoin.velocityPath τ hτ hτT B G, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerTransversePacketJoin.vectorDerivativeField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : EulerPacketCylinderField.Field P D.T (vectorDerivative τ hτ hτT B G)

Vector derivative field, bundling path, orbit, raw_eq.

Equations

• EulerTransversePacketJoin.vectorDerivativeField τ hτ hτT B G = { path := EulerTransversePacketJoin.derivativePath τ hτ hτT B G, orbit := ⋯, raw_eq := ⋯ }

theorem EulerTransversePacketJoin.vectorField_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : EulerPacketCylinderField.TimeDerivative ⋯ (vectorField τ hτ hτT B G) (vectorDerivativeField τ hτ hτT B G)

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

theorem EulerTransversePacketJoin.scalar_eq_pointField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : scalar τ hτ hτT B G (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P (pressurePath τ hτ hτT B G) ⋯ t (x, ↑θ)

noncomputable def EulerTransversePacketJoin.scalarGradientField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : EulerPacketCylinderField.Field P D.T (EulerPacketCylinderField.pressureGradient (scalar τ hτ hτT B G))

Scalar gradient field, constructed using EulerPacketCylinderField.scalarGradientField.

Equations

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

theorem EulerTransversePacketJoin.vector_left {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : vector τ hτ hτT B G (↑t, x, θ) = B.field (G.initial τ hτ ⋯) t (x, ↑θ)

theorem EulerTransversePacketJoin.vectorDerivative_left {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : vectorDerivative τ hτ hτT B G (↑t, x, θ) = B.derivativeField (G.initial τ hτ ⋯) t (x, ↑θ)

theorem EulerTransversePacketJoin.scalar_left {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : scalar τ hτ hτT B G (↑t, x, θ) = B.pressureField (G.initial τ hτ ⋯) t (x, ↑θ)

theorem EulerTransversePacketJoin.vector_right {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc τ D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : vector τ hτ hτT B G (↑t, x, θ) = (G.tail τ ⋯ hτT).vector (forwardInitial τ hτ hτT B G) (↑t - τ, x, θ)

theorem EulerTransversePacketJoin.vectorDerivative_right {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc τ D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : vectorDerivative τ hτ hτT B G (↑t, x, θ) = (G.tail τ ⋯ hτT).vectorDerivative (forwardInitial τ hτ hτT B G) (↑t - τ, x, θ)

theorem EulerTransversePacketJoin.scalar_right {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc τ D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : scalar τ hτ hτT B G (↑t, x, θ) = (G.tail τ ⋯ hτT).scalar (forwardInitial τ hτ hτT B G) (↑t - τ, x, θ)