Actual forcing and initial data for the transverse forward provider

Admissibility identifies the prescribed raw forcing with a genuine supported continuous cylinder L² path whose mixed translation orbit is smooth. No regularity or equation for an output field is assumed.

structure EulerTransversePacketProvider.Forcing (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (raw : EulerPacketProfileRecursion.VectorField) : Type

Forcing data, collecting path, path_orbit, raw_eq, mean_zero.

• path : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯))

  Time-dependent path of Forcing, of type C(Icc (0 : ℝ) D.T,Supported P Space D.support D.support_measurable).

• path_orbit : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P D.support ⋯) self.path)
• raw_eq (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw (↑t, x, θ) = EulerCylinderSmoothOrbit.pointField P ((EulerLpCylinderPaths.includePath P D.support ⋯) self.path) ⋯ t (x, ↑θ)
• mean_zero (t : ↑(Set.Icc 0 D.T)) : (EulerCylinderAngleAverage.average P) ↑(self.path t) = 0

structure EulerTransversePacketProvider.InitialData (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : Type u_1

Initial data, collecting value, orbit, mean_zero.

• value : ↥(EulerLpCylinderPaths.Supported P U D.support ⋯)

  Value of InitialData, of type Supported P U D.support D.support_measurable.

• orbit : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑self.value
• mean_zero : (EulerCylinderAngleAverage.average P) ↑self.value = 0

noncomputable def EulerTransversePacketProvider.InitialData.zero (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : InitialData P D

Zero, bundling value, orbit, mean_zero.

Equations

• EulerTransversePacketProvider.InitialData.zero P D = { value := 0, orbit := ⋯, mean_zero := ⋯ }

noncomputable def EulerTransversePacketProvider.Data.clamp {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ℝ) : ↑(Set.Icc 0 D.T)

Clamp, given by projIcc 0 D.T D.T_pos.le t.

Equations

• D.clamp t = Set.projIcc 0 D.T ⋯ t

@[simp]

theorem EulerTransversePacketProvider.Data.clamp_coe {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) : D.clamp ↑t = t

noncomputable def EulerTransversePacketProvider.Data.strain {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Strain, given by D.M.field (D.clamp z.1) z.2.1.

Equations

• D.strain z = (D.M.field (D.clamp z.1)) z.2.1

noncomputable def EulerTransversePacketProvider.Data.normalField {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space

Normal field, given by D.normal.field (D.clamp z.1) z.2.1.

Equations

• D.normalField z = (D.normal.field (D.clamp z.1)) z.2.1

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Forcing.coordinatePath {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) : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderPaths.Supported P U D.support ⋯))

Coordinate path type used in transverse packet forcing.

Equations

• G.coordinatePath I = EulerSourceCylinderEquation.coordinates P D.support ⋯ D.T ⋯ D.frame D.frameDerivative D.frameLower ⋯ ⋯ G.path I.value

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Forcing.velocityPath {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) : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯))

Velocity path type used in transverse packet forcing.

Equations

• G.velocityPath I = EulerSourceCylinderEquation.velocity P D.support ⋯ D.T ⋯ D.frame D.frameDerivative D.frameLower ⋯ ⋯ G.path I.value

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Forcing.derivativePath {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) : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯))

Derivative path type used in transverse packet forcing.

Equations

• G.derivativePath I = EulerSourceCylinderEquation.velocityDerivative P D.support ⋯ D.T ⋯ D.frame D.frameDerivative D.frameLower ⋯ ⋯ G.path I.value

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Forcing.pressurePath {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) : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))

Pressure path type used in transverse packet forcing.

Equations

• G.pressurePath I = EulerSourceCylinderEquation.pressurePath P D.support ⋯ D.T ⋯ D.frame D.frameDerivative D.frameLower ⋯ ⋯ G.path I.value D.M D.normal D.normalLower ⋯ ⋯

theorem EulerTransversePacketProvider.Forcing.velocityPath_orbit {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) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P D.support ⋯) (G.velocityPath I))

theorem EulerTransversePacketProvider.Forcing.derivativePath_orbit {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) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P D.support ⋯) (G.derivativePath I))

theorem EulerTransversePacketProvider.Forcing.pressurePath_orbit {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) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (G.pressurePath I)

theorem EulerTransversePacketProvider.Forcing.velocityPath_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) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (G.velocityPath I)) ((G.derivativePath I) t) (Set.Icc 0 D.T) ↑t