Literal composition, scaling and spatial differentiation of the actual matrix-coefficient witnesses.

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientAlgebra1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientAlgebra2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientAlgebra3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientAlgebra4 = inferInstance

noncomputable def EulerPacketCylinderField.MatrixCoefficient.comp {T : ℝ} {a b : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (B : MatrixCoefficient T b) : MatrixCoefficient T fun (z : EulerPacketPointJets.Domain) => a z ∘SL b z

Comp, bundling path, orbit, fun, B and the required compatibility proofs.

Equations

• A.comp B = { path := (EulerBoundedFieldCalculus.pathCompositionMap A.path) B.path, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerPacketCylinderField.MatrixCoefficient.add {T : ℝ} {a b : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (B : MatrixCoefficient T b) : MatrixCoefficient T (a + b)

Add, bundling path, orbit, raw_eq.

Equations

• A.add B = { path := A.path + B.path, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerPacketCylinderField.MatrixCoefficient.smul {T : ℝ} {a : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (c : ℝ) : MatrixCoefficient T (c • a)

Smul, bundling path, orbit, raw_eq.

Equations

• A.smul c = { path := c • A.path, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerPacketCylinderField.MatrixCoefficient.spatialDerivative {T : ℝ} {a : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (v : EulerSmoothLimit.Space) : MatrixCoefficient T fun (z : EulerPacketPointJets.Domain) => (fderiv ℝ (fun (x : EulerSmoothLimit.Space) => a (z.1, x, z.2.2)) z.2.1) v

Spatial derivative, bundling path, orbit, raw_eq, have and the required compatibility proofs.

Equations

• A.spatialDerivative v = { path := EulerMeanCoefficients.orbitDerivativePath A.path v, orbit := ⋯, raw_eq := ⋯ }

@[simp]

theorem EulerPacketCylinderField.MatrixCoefficient.comp_path_apply {T : ℝ} {a b : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (B : MatrixCoefficient T b) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ((A.comp B).path t) x = (A.path t) x ∘SL (B.path t) x

@[simp]

theorem EulerPacketCylinderField.MatrixCoefficient.smul_path_apply {T : ℝ} {a : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (c : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ((A.smul c).path t) x = c • (A.path t) x

theorem EulerPacketCylinderField.MatrixCoefficient.spatialDerivative_path_apply {T : ℝ} {a : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (v : EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ((A.spatialDerivative v).path t) x = (fderiv ℝ (⇑(A.path t)) x) v