Exact mixed-word invariance on cylinder L² and its time-function spaces.

Exact word-norm invariance along a genuine isometric orbit

Every actual derivative word of a smooth linear-isometric orbit is the orbit of its derivative at zero. Consequently its fixed-Sobolev word block is independent of the translation parameter, with constant one and no radius change. This applies equally to spatial L² and its time-function spaces.

noncomputable def EulerIsometricAction.derivativeAtZero {X : Type u_1} {E : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (u : E) (v : X) : E

Derivative at zero, given by fderiv ℝ (fun a => τ a u) 0 v.

Equations

• EulerIsometricAction.derivativeAtZero τ u v = (fderiv ℝ (fun (a : X) => (τ a) u) 0) v

theorem EulerIsometricAction.derivativeAtZero_translation {X : Type u_1} {E : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : X) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (u : E) (hu : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) u) (v a : X) : (τ a) (derivativeAtZero τ u v) = (fderiv ℝ (fun (b : X) => (τ b) u) a) v

theorem EulerIsometricAction.derivativeAtZero_smooth {X : Type u_1} {E : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : X) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (u : E) (hu : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) u) (v : X) : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) (derivativeAtZero τ u v)

noncomputable def EulerIsometricAction.wordAtZero {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (directions : ι → X) (u : E) {n : ℕ} (w : Fin n → ι) : E

Word at zero, given by wordDerivative directions (fun a => τ a u) w 0.

Equations

• EulerIsometricAction.wordAtZero τ directions u w = EulerParameterWordGevrey.wordDerivative directions (fun (a : X) => (τ a) u) w 0

theorem EulerIsometricAction.wordAtZero_zero {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (hzero : ∀ (u : E), (τ 0) u = u) (directions : ι → X) (u : E) (w : Fin 0 → ι) : wordAtZero τ directions u w = u

theorem EulerIsometricAction.wordAtZero_snoc {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : X) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (directions : ι → X) (u : E) (hu : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) u) {n : ℕ} (w : Fin n → ι) (i : ι) : wordAtZero τ directions u (Fin.snoc w i) = wordAtZero τ directions (derivativeAtZero τ u (directions i)) w

theorem EulerIsometricAction.wordAtZero_translation {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : X) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (hzero : ∀ (u : E), (τ 0) u = u) (directions : ι → X) (u : E) (hu : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) u) {n : ℕ} (w : Fin n → ι) (a : X) : (τ a) (wordAtZero τ directions u w) = EulerParameterWordGevrey.wordDerivative directions (fun (b : X) => (τ b) u) w a

theorem EulerIsometricAction.wordAtZero_smooth {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : X) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (hzero : ∀ (u : E), (τ 0) u = u) (directions : ι → X) (u : E) (hu : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) u) {n : ℕ} (w : Fin n → ι) : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) (wordAtZero τ directions u w)

theorem EulerIsometricAction.wordSum_orbit_constant {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : X) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (hzero : ∀ (u : E), (τ 0) u = u) [Fintype ι] (directions : ι → X) (u : E) (hu : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) u) (n : ℕ) (a : X) : EulerParameterWordGevrey.wordSum directions (fun (b : X) => (τ b) u) n a = EulerParameterWordGevrey.wordSum directions (fun (b : X) => (τ b) u) n 0

theorem EulerIsometricAction.baseSize_orbit_constant {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : X) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (hzero : ∀ (u : E), (τ 0) u = u) [Fintype ι] (directions : ι → X) (q : ℕ) (u : E) (hu : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) u) (a : X) : EulerParameterWordGevrey.baseSize directions q (fun (b : X) => (τ b) u) a = EulerParameterWordGevrey.baseSize directions q (fun (b : X) => (τ b) u) 0

theorem EulerIsometricAction.block_orbit_constant {X : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : X → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : X) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (hzero : ∀ (u : E), (τ 0) u = u) [Fintype ι] (directions : ι → X) (q : ℕ) (u : E) (hu : ContDiff ℝ ↑⊤ fun (a : X) => (τ a) u) (n : ℕ) (a : X) : EulerParameterWordGevrey.block directions q (fun (b : X) => (τ b) u) n a = EulerParameterWordGevrey.block directions q (fun (b : X) => (τ b) u) n 0

theorem EulerLpCylinderTranslation.pathTranslate_norm_map (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (a : EulerLiftedGradientSpace.LiftTangent) (f : C(K, ↥(CylinderL2 P V))) : ‖(pathTranslate P a) f‖ = ‖f‖

noncomputable def EulerLpCylinderTranslation.pathTranslateIsometry (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (a : EulerLiftedGradientSpace.LiftTangent) : C(K, ↥(CylinderL2 P V)) →ₗᵢ[ℝ] C(K, ↥(CylinderL2 P V))

Path translate isometry, bundling toLinearMap, norm_map.

Equations

• EulerLpCylinderTranslation.pathTranslateIsometry P a = { toLinearMap := ↑(EulerLpCylinderTranslation.pathTranslate P a), norm_map' := ⋯ }

theorem EulerLpCylinderTranslation.path_block_constant (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] {ι : Type u_3} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (f : C(K, ↥(CylinderL2 P V))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) f) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P b) f) n a = EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P b) f) n 0

noncomputable def EulerLpCylinderTranslation.timeTranslateIsometry (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) : ↥(EulerTimeLp.TimeLp T ↥(CylinderL2 P V)) →ₗᵢ[ℝ] ↥(EulerTimeLp.TimeLp T ↥(CylinderL2 P V))

Time translate isometry, given by timeLiftIsometry T (translate P a).

Equations

• EulerLpCylinderTranslation.timeTranslateIsometry P T a = EulerTimeLpBoundedMap.timeLiftIsometry T (EulerLpCylinderTranslation.translate P a)

theorem EulerLpCylinderTranslation.timeTranslateIsometry_add (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (a b : EulerLiftedGradientSpace.LiftTangent) (f : ↥(EulerTimeLp.TimeLp T ↥(CylinderL2 P V))) : (timeTranslateIsometry P T a) ((timeTranslateIsometry P T b) f) = (timeTranslateIsometry P T (a + b)) f

theorem EulerLpCylinderTranslation.timeTranslateIsometry_zero (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (f : ↥(EulerTimeLp.TimeLp T ↥(CylinderL2 P V))) : (timeTranslateIsometry P T 0) f = f

theorem EulerLpCylinderTranslation.time_block_constant (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (T : ℝ) (f : ↥(EulerTimeLp.TimeLp T ↥(CylinderL2 P V))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (translate P a).toContinuousLinearMap) f) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (translate P b).toContinuousLinearMap) f) n a = EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (translate P b).toContinuousLinearMap) f) n 0

theorem EulerLpCylinderTranslation.pathLp_orbit_contDiff (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(CylinderL2 P V))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) f) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (translate P a).toContinuousLinearMap) (EulerTimeLp.pathLp T hT f)

theorem EulerLpCylinderTranslation.pathLp_block_le (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(CylinderL2 P V))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) f) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (translate P b).toContinuousLinearMap) (EulerTimeLp.pathLp T hT f)) n a ≤ √T * EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P b) f) n a

The actual Ctime-to-time-L² inclusion preserves all mixed word blocks with exactly the square-root time length factor.