Actual cylinder-path witnesses for the constructed transverse solution and corrector.

noncomputable def EulerTransversePacketProvider.Forcing.vectorField {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) : EulerPacketCylinderField.Field P D.T (G.vector I)

Vector field, bundling path, orbit, raw_eq.

Equations

• G.vectorField I = { path := G.fullVelocityPath I, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerTransversePacketProvider.Forcing.vectorDerivativeField {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) : EulerPacketCylinderField.Field P D.T (G.vectorDerivative I)

Vector derivative field, bundling path, orbit, raw_eq.

Equations

• G.vectorDerivativeField I = { path := G.fullDerivativePath I, orbit := ⋯, raw_eq := ⋯ }

theorem EulerTransversePacketProvider.Forcing.vectorField_time {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) : EulerPacketCylinderField.TimeDerivative ⋯ (G.vectorField I) (G.vectorDerivativeField I)

noncomputable def EulerTransversePacketProvider.Forcing.correctorField {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) : EulerPacketCylinderField.Field P D.T (G.corrector I)

Corrector field, bundling path, orbit, raw_eq.

Equations

• G.correctorField I = { path := G.correctorPath I, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerTransversePacketProvider.Forcing.correctorDerivativeField {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) : EulerPacketCylinderField.Field P D.T (G.correctorDerivative I)

Corrector derivative field, bundling path, orbit, raw_eq.

Equations

• G.correctorDerivativeField I = { path := G.correctorTimePath I, orbit := ⋯, raw_eq := ⋯ }

theorem EulerTransversePacketProvider.Forcing.correctorField_time {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) : EulerPacketCylinderField.TimeDerivative ⋯ (G.correctorField I) (G.correctorDerivativeField I)

theorem EulerTransversePacketProvider.Forcing.vectorField_supported {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)) : (G.vectorField I).path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketProvider.Forcing.vectorDerivativeField_supported {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)) : (G.vectorDerivativeField I).path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketProvider.Forcing.correctorField_supported {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)) : (G.correctorField I).path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketProvider.Forcing.correctorDerivativeField_supported {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)) : (G.correctorDerivativeField I).path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯