Actual raw slow and normal-weighted angular advection on cylinder-path witnesses.

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.instPacketCylinderFieldAdvection1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.instPacketCylinderFieldAdvection2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.instPacketCylinderFieldAdvection3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketCylinderField.instPacketCylinderFieldAdvection3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.instPacketCylinderFieldAdvection4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

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

Equations

• EulerPacketCylinderField.instPacketCylinderFieldAdvection4 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.instPacketCylinderFieldAdvection5 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketCylinderField.instPacketCylinderFieldAdvection6 = inferInstance

noncomputable def EulerPacketCylinderField.normalComponentMap : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Embed the actual normal component into a fixed unit vector.

Equations

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

@[simp]

theorem EulerPacketCylinderField.normalComponentMap_apply (m v : EulerSmoothLimit.Space) : (normalComponentMap m) v = EulerCylinderScalarPrimitive.scalarEmbed (inner ℝ m v)

theorem EulerPacketCylinderField.normalComponentMap_project (m v : EulerSmoothLimit.Space) : EulerCylinderScalarPrimitive.scalarProject ((normalComponentMap m) v) = inner ℝ m v

noncomputable def EulerPacketCylinderField.normalComponentPath {K : Type u_1} [TopologicalSpace K] (N : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Normal component path, given by mapCoefficientPath normalComponentMap N.

Equations

• EulerPacketCylinderField.normalComponentPath N = (EulerMeanCoefficients.mapCoefficientPath EulerPacketCylinderField.normalComponentMap) N

theorem EulerPacketCylinderField.normalComponentPath_orbit {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (N : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) (hN : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath N)) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath (normalComponentPath N))

noncomputable def EulerPacketCylinderField.Field.spatialTransport {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) (raw z, 0)

Spatial transport expressed directly in the full raw covering derivative.

Equations

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

noncomputable def EulerPacketCylinderField.Field.angularTransport {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') (N : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) (hN : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath N)) (m : EulerPacketProfileRecursion.VectorField) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), m (↑t, x, θ) = (N t) x) : Field P T fun (z : EulerPacketPointJets.Domain) => inner ℝ (m z) (raw z) • (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => raw' (z.1, y)) z.2) (0, 1)

The normal factor is a real coefficient operation; no L² integrability of the normal itself is needed.

Equations

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