Actual nonlinear and coefficient operations on raw cylinder-path witnesses.

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

Map, constructed using ofLifted.

Equations

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

noncomputable def EulerPacketCylinderField.Field.derivative {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (i : Fin 4) : Field P T fun (z : EulerPacketPointJets.Domain) => (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => raw (z.1, y)) z.2) (EulerCylinderSobolev.standardDirection i)

The literal mixed derivative is represented by the actual derivative path.

Equations

• G.derivative i = { path := EulerCylinderSmoothOrbit.derivativePath P G.path i, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerPacketCylinderField.Field.scalarProduct {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) : Field P T fun (z : EulerPacketPointJets.Domain) => L (raw z) • raw' z

Scalar product, bundling path, orbit, raw_eq.

Equations

• G.scalarProduct H L hL = { path := EulerCylinderPathProduct.scalarProductPath P L hL G.path H.path ⋯ ⋯, orbit := ⋯, raw_eq := ⋯ }

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

Bilinear, bundling path, orbit, raw_eq.

Equations

• G.bilinear H B = { path := EulerCylinderPathProduct.bilinearProductPath P B G.path H.path ⋯ ⋯, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerPacketCylinderField.Field.advection {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') : Field P T fun (z : EulerPacketPointJets.Domain) => (fderiv ℝ (fun (y : EulerSmoothLimit.Space) => raw' (z.1, y, z.2.2)) z.2.1) (raw z)

Spatial advection is the literal ordinary derivative of the second raw field.

Equations

• G.advection H = { path := EulerCylinderPathProduct.advectionPath P G.path H.path ⋯ ⋯, orbit := ⋯, raw_eq := ⋯ }

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.Field.instPacketCylinderFieldProducts1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.Field.instPacketCylinderFieldProducts2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.Field.instPacketCylinderFieldProducts3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.Field.instPacketCylinderFieldProducts4 = inferInstance

noncomputable def EulerPacketCylinderField.Field.multiply {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (A : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (coef : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hcoef : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), coef (↑t, x, θ) = (A t) x) : Field P T fun (z : EulerPacketPointJets.Domain) => (coef z) (raw z)

A genuine smooth coefficient path multiplies a raw field without a new regularity premise.

Equations

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