Literal smooth L² fields from the actual solved translation orbit

All full spatial derivative tensors of the canonical representative are in L². Their L² classes are reconstructed from the finitely many genuine strong coordinate derivatives. A smooth orbit of a continuous-time path supplies continuity of every tensor jet in time.

noncomputable def EulerMeanSmoothRepresentative.orbitTensorLp (u : ↥EulerMeanSolenoidal.L2) (n : ℕ) : ↥(MeasureTheory.Lp (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space) 2 MeasureTheory.volume)

The literal tensor-valued L² field assembled from actual strong derivatives.

Equations

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

theorem EulerMeanSmoothRepresentative.orbitTensorLp_ae (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (n : ℕ) : ↑↑(orbitTensorLp u n) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n (representative u hu)

theorem EulerMeanSmoothRepresentative.representative_iteratedFDeriv_memLp (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (n : ℕ) : MeasureTheory.MemLp (iteratedFDeriv ℝ n (representative u hu)) 2 MeasureTheory.volume

Integrability of full tensors is proved, rather than added as an output hypothesis.

noncomputable def EulerMeanSmoothRepresentative.smoothL2Field (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

A smooth translation orbit produces a genuine smooth spatial L² field.

Equations

• EulerMeanSmoothRepresentative.smoothL2Field u hu = { field := EulerMeanSmoothRepresentative.representative u hu, smooth := ⋯, integrable := ⋯ }

@[simp]

theorem EulerMeanSmoothRepresentative.smoothL2Field_field (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (x : EulerSmoothLimit.Space) : (smoothL2Field u hu).field x = representative u hu x

@[simp]

theorem EulerMeanSmoothRepresentative.smoothL2Field_toLp (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : (smoothL2Field u hu).toLp = u

@[simp]

theorem EulerMeanSmoothRepresentative.smoothL2Field_jetLp (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (n : ℕ) : (smoothL2Field u hu).jetLp n = orbitTensorLp u n

theorem EulerMeanSmoothRepresentative.orbitTensorLp_continuous {K : Type u_1} [TopologicalSpace K] (u : K → ↥EulerMeanSolenoidal.L2) (n : ℕ) (h : ∀ (w : Fin n → Fin 3), Continuous fun (t : K) => EulerMeanClassicalWordBounds.ordinaryWord EulerLpFiniteTensor.direction (u t) w) : Continuous fun (t : K) => orbitTensorLp (u t) n

A finite coordinate family is all that the qualitative tensor reconstruction uses.

theorem EulerMeanSmoothRepresentative.smoothL2Field_path_jet_continuous (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (smoothL2Field (p t) ⋯).jetLp n

Every literal tensor jet of the reconstructed path is continuous in L².