Actual spatial translations of the fixed mean time space

Translation preserves ordinary solenoidal L² and its Bochner time space. The action is isometric and strongly continuous and commutes with the actual terminal primitive and initial trace.

Strong continuity of isometric spatial actions on time L²

This uses dominated convergence with the actual square-integrable time field. It does not assume operator-norm continuity of spatial translations.

theorem EulerTimeLpBoundedMap.timeLift_norm_sub_sq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A B : E →L[ℝ] E) (u : ↥(EulerTimeLp.TimeLp T E)) : ‖(timeLift T A) u - (timeLift T B) u‖ ^ 2 = ∫ (t : ℝ), ‖A (↑↑u t) - B (↑↑u t)‖ ^ 2 ∂EulerTimeLp.timeMeasure T

A pointwise formula for the square distance between two genuine lifted fields.

theorem EulerTimeLpBoundedMap.timeLift_strongly_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type u_2} [TopologicalSpace X] [FirstCountableTopology X] (T : ℝ) (A : X → E →L[ℝ] E) (hA : ∀ (x : X) (v : E), ‖(A x) v‖ = ‖v‖) (hc : ∀ (v : E), Continuous fun (x : X) => (A x) v) (u : ↥(EulerTimeLp.TimeLp T E)) : Continuous fun (x : X) => (timeLift T (A x)) u

A strongly continuous family of spatial isometries remains strongly continuous on the genuine Bochner time space.

noncomputable def EulerMeanTimeTranslation.solenoidalTranslation (a : EulerSmoothLimit.Space) : ↥EulerMeanSolenoidal.solenoidalSpace →ₗᵢ[ℝ] ↥EulerMeanSolenoidal.solenoidalSpace

Spatial translation restricted to the actual ordinary solenoidal space.

Equations

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

@[simp]

theorem EulerMeanTimeTranslation.solenoidalTranslation_coe (a : EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.solenoidalSpace) : ↑((solenoidalTranslation a) u) = (EulerMeanSolenoidal.translation a) ↑u

theorem EulerMeanTimeTranslation.solenoidalTranslation_add (a b : EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.solenoidalSpace) : (solenoidalTranslation a) ((solenoidalTranslation b) u) = (solenoidalTranslation (a + b)) u

@[simp]

theorem EulerMeanTimeTranslation.solenoidalTranslation_zero (u : ↥EulerMeanSolenoidal.solenoidalSpace) : (solenoidalTranslation 0) u = u

theorem EulerMeanTimeTranslation.translation_continuous (u : ↥EulerMeanSolenoidal.L2) : Continuous fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u

Strong continuity is proved for every ordinary L² equivalence class.

theorem EulerMeanTimeTranslation.solenoidalTranslation_continuous (u : ↥EulerMeanSolenoidal.solenoidalSpace) : Continuous fun (a : EulerSmoothLimit.Space) => (solenoidalTranslation a) u

The same strong continuity holds on the closed solenoidal subspace.

noncomputable def EulerMeanTimeTranslation.timeTranslation (T : ℝ) (a : EulerSmoothLimit.Space) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2) →ₗᵢ[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Actual spatial translation at every Bochner time slice.

Equations

• EulerMeanTimeTranslation.timeTranslation T a = EulerTimeLpBoundedMap.timeLiftIsometry T (EulerMeanSolenoidal.translation a)

noncomputable def EulerMeanTimeTranslation.timeSolenoidalTranslation (T : ℝ) (a : EulerSmoothLimit.Space) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →ₗᵢ[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Actual spatial translation on the fixed solenoidal time Hilbert space.

Equations

• EulerMeanTimeTranslation.timeSolenoidalTranslation T a = EulerTimeLpBoundedMap.timeLiftIsometry T (EulerMeanTimeTranslation.solenoidalTranslation a)

theorem EulerMeanTimeTranslation.timeTranslation_ae (T : ℝ) (a : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : ↑↑((timeTranslation T a) u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (EulerMeanSolenoidal.translation a) (↑↑u t)

theorem EulerMeanTimeTranslation.timeSolenoidalTranslation_ae (T : ℝ) (a : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : ↑↑((timeSolenoidalTranslation T a) u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (solenoidalTranslation a) (↑↑u t)

theorem EulerMeanTimeTranslation.timeTranslation_add (T : ℝ) (a b : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (timeTranslation T a) ((timeTranslation T b) u) = (timeTranslation T (a + b)) u

@[simp]

theorem EulerMeanTimeTranslation.timeTranslation_zero (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (timeTranslation T 0) u = u

theorem EulerMeanTimeTranslation.timeSolenoidalTranslation_add (T : ℝ) (a b : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (timeSolenoidalTranslation T a) ((timeSolenoidalTranslation T b) u) = (timeSolenoidalTranslation T (a + b)) u

@[simp]

theorem EulerMeanTimeTranslation.timeSolenoidalTranslation_zero (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (timeSolenoidalTranslation T 0) u = u

theorem EulerMeanTimeTranslation.timeTranslation_continuous (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : Continuous fun (a : EulerSmoothLimit.Space) => (timeTranslation T a) u

The actual spatial action is continuous in translation for every time-L² field.

theorem EulerMeanTimeTranslation.timeSolenoidalTranslation_continuous (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : Continuous fun (a : EulerSmoothLimit.Space) => (timeSolenoidalTranslation T a) u

Strong continuity on the fixed mean derivative space.

theorem EulerMeanTimeTranslation.timeTranslation_realPrimitive (T : ℝ) (a : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (t : ℝ) : EulerTerminalTimePrimitive.realPrimitive T ((timeTranslation T a) u) t = (EulerMeanSolenoidal.translation a) (EulerTerminalTimePrimitive.realPrimitive T u t)

theorem EulerMeanTimeTranslation.timeSolenoidalTranslation_realPrimitive (T : ℝ) (a : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (t : ℝ) : EulerTerminalTimePrimitive.realPrimitive T ((timeSolenoidalTranslation T a) u) t = (solenoidalTranslation a) (EulerTerminalTimePrimitive.realPrimitive T u t)

theorem EulerMeanTimeTranslation.timeTranslation_initialTrace (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (EulerTerminalTimePrimitive.initialTrace T hT) ((timeTranslation T a) u) = (EulerMeanSolenoidal.translation a) ((EulerTerminalTimePrimitive.initialTrace T hT) u)

theorem EulerMeanTimeTranslation.timeSolenoidalTranslation_initialTrace (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerTerminalTimePrimitive.initialTrace T hT) ((timeSolenoidalTranslation T a) u) = (solenoidalTranslation a) ((EulerTerminalTimePrimitive.initialTrace T hT) u)

theorem EulerMeanTimeTranslation.timeTranslation_primitiveTimeLp (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (EulerTerminalTimePrimitive.primitiveTimeLp T hT) ((timeTranslation T a) u) = (timeTranslation T a) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) u)

theorem EulerMeanTimeTranslation.timeSolenoidalTranslation_primitiveTimeLp (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerTerminalTimePrimitive.primitiveTimeLp T hT) ((timeSolenoidalTranslation T a) u) = (timeSolenoidalTranslation T a) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) u)