Spatial bounded maps on genuine Bochner time spaces

A bounded spatial map acts on each time slice. The lift commutes with actual terminal integration and initial trace. These identities let spatial translations and their difference quotients act on a fixed time Hilbert space.

noncomputable def EulerTimeLpBoundedMap.timeLift {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (A : E →L[ℝ] F) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T F)

The actual pointwise lift of a bounded spatial map to Bochner L² time.

Equations

• EulerTimeLpBoundedMap.timeLift T A = ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) A

theorem EulerTimeLpBoundedMap.timeLift_ae {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (A : E →L[ℝ] F) (u : ↥(EulerTimeLp.TimeLp T E)) : ↑↑((timeLift T A) u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => A (↑↑u t)

theorem EulerTimeLpBoundedMap.timeLift_norm_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (A : E →L[ℝ] F) : ‖timeLift T A‖ ≤ ‖A‖

theorem EulerTimeLpBoundedMap.timeLift_apply_norm_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (A : E →L[ℝ] F) (u : ↥(EulerTimeLp.TimeLp T E)) : ‖(timeLift T A) u‖ ≤ ‖A‖ * ‖u‖

theorem EulerTimeLpBoundedMap.timeLift_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (A B : E →L[ℝ] F) : timeLift T (A + B) = timeLift T A + timeLift T B

theorem EulerTimeLpBoundedMap.timeLift_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T c : ℝ) (A : E →L[ℝ] F) : timeLift T (c • A) = c • timeLift T A

theorem EulerTimeLpBoundedMap.timeLift_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (T : ℝ) (A : F →L[ℝ] G) (B : E →L[ℝ] F) : timeLift T (A ∘SL B) = timeLift T A ∘SL timeLift T B

theorem EulerTimeLpBoundedMap.timeLift_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) : timeLift T (ContinuousLinearMap.id ℝ E) = ContinuousLinearMap.id ℝ ↥(EulerTimeLp.TimeLp T E)

theorem EulerTimeLpBoundedMap.zeroExtension_timeLift {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (A : E →L[ℝ] F) (u : ↥(EulerTimeLp.TimeLp T E)) : EulerTerminalTimePrimitive.zeroExtension T ((timeLift T A) u) =ᵐ[MeasureTheory.volume] fun (t : ℝ) => A (EulerTerminalTimePrimitive.zeroExtension T u t)

theorem EulerTimeLpBoundedMap.timeLift_norm_map {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (A : E →L[ℝ] F) (hA : ∀ (x : E), ‖A x‖ = ‖x‖) (u : ↥(EulerTimeLp.TimeLp T E)) : ‖(timeLift T A) u‖ = ‖u‖

An isometric spatial map remains isometric on the actual time space.

noncomputable def EulerTimeLpBoundedMap.timeLiftIsometry {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (A : E →ₗᵢ[ℝ] F) : ↥(EulerTimeLp.TimeLp T E) →ₗᵢ[ℝ] ↥(EulerTimeLp.TimeLp T F)

The actual pointwise lift of a linear spatial isometry.

Equations

• EulerTimeLpBoundedMap.timeLiftIsometry T A = { toLinearMap := ↑(EulerTimeLpBoundedMap.timeLift T A.toContinuousLinearMap), norm_map' := ⋯ }

theorem EulerTimeLpBoundedMap.realPrimitive_timeLift {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] (T : ℝ) (A : E →L[ℝ] F) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ℝ) : EulerTerminalTimePrimitive.realPrimitive T ((timeLift T A) u) t = A (EulerTerminalTimePrimitive.realPrimitive T u t)

Bounded spatial maps commute with the genuine Bochner terminal primitive.

theorem EulerTimeLpBoundedMap.initialTrace_timeLift {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] (T : ℝ) (hT : 0 ≤ T) (A : E →L[ℝ] F) (u : ↥(EulerTimeLp.TimeLp T E)) : (EulerTerminalTimePrimitive.initialTrace T hT) ((timeLift T A) u) = A ((EulerTerminalTimePrimitive.initialTrace T hT) u)

The terminal-zero normalization is preserved by every bounded spatial map.

theorem EulerTimeLpBoundedMap.primitiveTimeLp_timeLift {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] (T : ℝ) (hT : 0 ≤ T) (A : E →L[ℝ] F) (u : ↥(EulerTimeLp.TimeLp T E)) : (EulerTerminalTimePrimitive.primitiveTimeLp T hT) ((timeLift T A) u) = (timeLift T A) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) u)

Commutation also holds as an equality of actual Bochner L² fields.

theorem EulerTimeLpBoundedMap.timeLift_adjoint {H : Type u_4} {K : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℝ K] [CompleteSpace K] (T : ℝ) (A : H →L[ℝ] K) : ContinuousLinearMap.adjoint (timeLift T A) = timeLift T (ContinuousLinearMap.adjoint A)

The genuine time-space adjoint acts by the spatial adjoint at each time.