Bounded maps commute with the genuine time-H¹ reconstruction

This identity permits spatial translations to be applied to the two actual Bochner fields before reconstructing the continuous time representative. It is an equality of the constructed operators, independent of any smoothness assumption on their inputs.

theorem EulerTimeH1Reconstruction.mean_timeLift {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (T : ℝ) (hT : 0 ≤ T) (A : E →L[ℝ] F) (p : ↥(EulerTimeLp.TimeLp T E)) : (mean T hT) ((EulerTimeLpBoundedMap.timeLift T A) p) = A ((mean T hT) p)

The actual time average commutes with every bounded linear map.

theorem EulerTimeH1Reconstruction.reconstruction_timeLift {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (T : ℝ) (hT : 0 ≤ T) (A : E →L[ℝ] F) (p q : ↥(EulerTimeLp.TimeLp T E)) (t : ↑(Set.Icc 0 T)) : ((reconstruction T hT) ((EulerTimeLpBoundedMap.timeLift T A) p, (EulerTimeLpBoundedMap.timeLift T A) q)) t = A (((reconstruction T hT) (p, q)) t)

The continuous time representative commutes with every bounded linear map.