Actual Bochner L² time spaces and continuous-path embeddings used by maximal regularity.

noncomputable def EulerTimeLp.timeMeasure (T : ℝ) : MeasureTheory.Measure ℝ

Lebesgue time measure restricted to the prescribed compact evolution interval.

Equations

• EulerTimeLp.timeMeasure T = MeasureTheory.volume.restrict (Set.Icc 0 T)

instance EulerTimeLp.timeMeasureFinite (T : ℝ) : MeasureTheory.IsFiniteMeasure (timeMeasure T)

The actual compact time measure is finite.

@[reducible, inline]

noncomputable abbrev EulerTimeLp.TimeLp (T : ℝ) (E : Type u_1) [NormedAddCommGroup E] : AddSubgroup (ℝ →ₘ[timeMeasure T] E)

The actual Bochner L² space of time-dependent values in a normed space.

Equations

• EulerTimeLp.TimeLp T E = MeasureTheory.Lp E 2 (EulerTimeLp.timeMeasure T)

theorem EulerTimeLp.path_memLp {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : MeasureTheory.MemLp (EulerVolterraConvolution.extendPath T hT f) 2 (timeMeasure T)

A continuous compact-time path is genuinely square integrable after clamping.

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

A continuous time path represented in the actual Bochner L² space.

Equations

• EulerTimeLp.pathLp T hT f = MeasureTheory.MemLp.toLp (EulerVolterraConvolution.extendPath T hT f) ⋯

theorem EulerTimeLp.pathLp_ae {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : ↑↑(pathLp T hT f) =ᵐ[timeMeasure T] EulerVolterraConvolution.extendPath T hT f

The Bochner path representative is the genuine clamped continuous path almost everywhere.

theorem EulerTimeLp.pathLp_bound {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : ‖pathLp T hT f‖ ≤ ↑(MeasureTheory.measureUnivNNReal (timeMeasure T)) ^ (1 / 2) * ‖f‖

The continuous-path inclusion obeys the actual finite-time L² norm bound.

theorem EulerTimeLp.pathLp_sub {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 path embedding preserves subtraction.

theorem EulerTimeLp.pathLp_tendsto {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (hT : 0 ≤ T) (f : ℕ → C(↑(Set.Icc 0 T), E)) (g : C(↑(Set.Icc 0 T), E)) (h : Filter.Tendsto f Filter.atTop (nhds g)) : Filter.Tendsto (fun (n : ℕ) => pathLp T hT (f n)) Filter.atTop (nhds (pathLp T hT g))

Uniform convergence of actual continuous paths implies convergence in actual L² time.

theorem EulerTimeLp.norm_sq_eq_integral {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (f : ↥(TimeLp T E)) : ‖f‖ ^ 2 = ∫ (t : ℝ), ‖↑↑f t‖ ^ 2 ∂timeMeasure T

The actual Bochner L² norm squared is the integral of the squared pointwise norm, also for Banach targets.

theorem EulerTimeLp.pathLp_norm_sq {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : ‖pathLp T hT f‖ ^ 2 = ∫ (t : ℝ) in 0..T, ‖EulerVolterraConvolution.extendPath T hT f t‖ ^ 2

The actual L² time norm of a continuous path is its classical time energy integral.