Genuine Sobolev arrays and bounded spatial evaluation for ordinary L² translation orbits.

theorem EulerMeanSmoothRepresentative.instMeanOrbitSobolev1 : Fact (0 < 1)

noncomputable def EulerMeanSmoothRepresentative.coordinateTuple {n : ℕ} (w : Fin n → Fin 4) : Fin n → EulerSmoothLimit.Space

Coordinate tuple, defined pointwise by (standardDirection (w i)).1.

Equations

• EulerMeanSmoothRepresentative.coordinateTuple w i = (EulerCylinderSobolev.standardDirection (w i)).1

theorem EulerMeanSmoothRepresentative.coordinateTuple_norm_le {n : ℕ} (w : Fin n → Fin 4) : ‖coordinateTuple w‖ ≤ 1

theorem EulerMeanSmoothRepresentative.iteratedFDeriv_orbitDerivative (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (v : EulerSmoothLimit.Space) (n : ℕ) (a : EulerSmoothLimit.Space) (m : Fin n → EulerSmoothLimit.Space) : (iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation b) (orbitDerivative u v)) a) m = (iteratedFDeriv ℝ (n + 1) (fun (b : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation b) u) a) (Fin.snoc m v)

Iterating an actual strong orbit derivative is the same as evaluating the next full tensor.

theorem EulerMeanSmoothRepresentative.ordinarySpatialJet_word (n q : ℕ) (hn : n ≤ q) (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (w : Fin n → Fin 4) : (ordinarySpatialJet q u hu).word w = EulerMeanOrdinaryLift.ordinaryLift ((iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) 0) (coordinateTuple w))

The coordinates of the constructed jet are actual ordinary-space derivative tensors.

noncomputable def EulerMeanSmoothRepresentative.ordinarySobolev (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : ↥(EulerCylinderSobolevSpace.SobolevSpace 1 q)

A concrete element of the previously constructed complete cylinder Sobolev space.

Equations

• EulerMeanSmoothRepresentative.ordinarySobolev q u hu = EulerCylinderSobolevSpace.ofJet 1 (EulerMeanSmoothRepresentative.ordinarySpatialJet q u hu)

@[simp]

theorem EulerMeanSmoothRepresentative.ordinarySobolev_value (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : EulerCylinderSobolevSpace.value 1 (ordinarySobolev q u hu) = EulerMeanOrdinaryLift.ordinaryLift u

theorem EulerMeanSmoothRepresentative.ordinarySobolev_coordinate (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (w : EulerCylinderSobolevSpace.SobolevWord q) : ↑(ordinarySobolev q u hu) w = EulerMeanOrdinaryLift.ordinaryLift ((iteratedFDeriv ℝ (↑w.fst) (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) 0) (coordinateTuple w.snd))

theorem EulerMeanSmoothRepresentative.ordinarySobolev_norm_le (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : ‖ordinarySobolev q u hu‖ ≤ ∑ n ∈ Finset.range (q + 1), ‖iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) 0‖

The finite Sobolev array is bounded directly by actual L² orbit-derivative norms.

theorem EulerMeanSmoothRepresentative.ordinarySobolev_continuous {T : Type u_1} [TopologicalSpace T] (q : ℕ) (u : T → ↥EulerMeanSolenoidal.L2) (hu : ∀ (t : T), SmoothOrbit (u t)) (hjet : ∀ n ≤ q, Continuous fun (t : T) => iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) (u t)) 0) : Continuous fun (t : T) => ordinarySobolev q (u t) ⋯

Continuity of finitely many actual derivative tensors gives continuity in genuine Sobolev norm.