Actual bounded coefficient paths identified with the raw packet coefficients.

@[instance_reducible]

noncomputable def EulerPacketCylinderField.instPacketCylinderCoefficientData1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCylinderField.instPacketCylinderCoefficientData1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.instPacketCylinderCoefficientData2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCylinderField.instPacketCylinderCoefficientData2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.instPacketCylinderCoefficientData3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCylinderField.instPacketCylinderCoefficientData3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.instPacketCylinderCoefficientData4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCylinderField.instPacketCylinderCoefficientData4 = inferInstance

structure EulerPacketCylinderField.MatrixCoefficient (T : ℝ) (raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : Type

Matrix coefficient data, collecting path, orbit, raw_eq.

• path : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

  Time-dependent path of MatrixCoefficient, of type C(Icc (0 : ℝ) T,Space →ᵇ Space →L[ℝ] Space).

• orbit : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath self.path)
• raw_eq (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw (↑t, x, θ) = (self.path t) x

structure EulerPacketCylinderField.VectorCoefficient (T : ℝ) (raw : EulerPacketProfileRecursion.VectorField) : Type

Vector coefficient data, collecting path, orbit, raw_eq.

• path : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

  Time-dependent path of VectorCoefficient, of type C(Icc (0 : ℝ) T,Space →ᵇ Space).

• orbit : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath self.path)
• raw_eq (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw (↑t, x, θ) = (self.path t) x

noncomputable def EulerPacketCylinderField.MatrixCoefficient.multiply {P T : ℝ} [Fact (0 < P)] {coef : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} {raw : EulerPacketProfileRecursion.VectorField} (A : MatrixCoefficient T coef) (G : Field P T raw) : Field P T fun (z : EulerPacketPointJets.Domain) => (coef z) (raw z)

Multiply, given by G.multiply A.path A.orbit coef A.raw_eq.

Equations

• A.multiply G = G.multiply A.path ⋯ coef ⋯

noncomputable def EulerPacketCylinderField.MatrixCoefficient.adjoint {T : ℝ} {coef : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T coef) : MatrixCoefficient T fun (z : EulerPacketPointJets.Domain) => ContinuousLinearMap.adjoint (coef z)

Adjoint, bundling path, orbit, translateCoefficientPath, exact and the required compatibility proofs.

Equations

• A.adjoint = { path := EulerBoundedFieldCalculus.pathAdjointMap A.path, orbit := ⋯, raw_eq := ⋯ }

structure EulerPacketCylinderField.CoefficientData (P T : ℝ) (O : EulerPacketProfileRecursion.Operators) : Type

This data is only regularity and literal identification of the three source coefficients.

• period_eq : O.period = P
• interval_eq : O.interval = Set.Icc 0 T
• inverse : MatrixCoefficient T O.inverseFrame

  Inverse of CoefficientData, of type MatrixCoefficient T O.inverseFrame.

• strain : MatrixCoefficient T O.strain

  Strain of CoefficientData, of type MatrixCoefficient T O.strain.

• normal : VectorCoefficient T O.normal

  Normal of CoefficientData, of type VectorCoefficient T O.normal.