The actual continuous-path embedding as a bounded linear time-space map.

theorem EulerTimeLp.pathLp_add {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (hT : 0 ≤ T) (f g : C(↑(Set.Icc 0 T), E)) : pathLp T hT (f + g) = pathLp T hT f + pathLp T hT g

The actual continuous-path inclusion preserves addition.

theorem EulerTimeLp.pathLp_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (r : ℝ) (f : C(↑(Set.Icc 0 T), E)) : pathLp T hT (r • f) = r • pathLp T hT f

The actual continuous-path inclusion preserves real scalar multiplication.

noncomputable def EulerTimeLp.pathLpOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) : C(↑(Set.Icc 0 T), E) →L[ℝ] ↥(TimeLp T E)

The genuine continuous-path to Bochner L² embedding is a bounded linear map.

Equations

• EulerTimeLp.pathLpOperator T hT = { toFun := EulerTimeLp.pathLp T hT, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (↑(MeasureTheory.measureUnivNNReal (EulerTimeLp.timeMeasure T)) ^ (1 / 2)) ⋯

theorem EulerTimeLp.pathLpOperator_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : (pathLpOperator T hT) f = pathLp T hT f

The bounded embedding is exactly the actual L² equivalence class of the path.