Actual bounded time-dependent linear operators on Bochner L² time fields.

theorem EulerTimeLp.timeApply_memLp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (u : ↥(TimeLp T E)) : MeasureTheory.MemLp (fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A t) (↑↑u t)) 2 (timeMeasure T)

A continuous compact-time operator path acts on every actual square-integrable time field.

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

The genuine pointwise time-dependent operator action, represented in Bochner L².

Equations

• EulerTimeLp.timeApply T hT A u = MeasureTheory.MemLp.toLp (fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A t) (↑↑u t)) ⋯

theorem EulerTimeLp.timeApply_ae {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (u : ↥(TimeLp T E)) : ↑↑(timeApply T hT A u) =ᵐ[timeMeasure T] fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A t) (↑↑u t)

The actual Bochner action has its literal pointwise representative almost everywhere.

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

Actual time-dependent bounded operator application is linear in the time field.

Equations

• EulerTimeLp.timeApplyLinear T hT A = { toFun := EulerTimeLp.timeApply T hT A, map_add' := ⋯, map_smul' := ⋯ }

theorem EulerTimeLp.timeApply_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (u : ↥(TimeLp T E)) : ‖timeApply T hT A u‖ ≤ ‖A‖ * ‖u‖

The actual time multiplier has the uniform operator-path norm bound.

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

The bounded actual time multiplier on Bochner L² spaces.

Equations

• EulerTimeLp.timeMultiplier T hT A = (EulerTimeLp.timeApplyLinear T hT A).mkContinuous ‖A‖ ⋯

theorem EulerTimeLp.timeMultiplier_ae {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (u : ↥(TimeLp T E)) : ↑↑((timeMultiplier T hT A) u) =ᵐ[timeMeasure T] fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A t) (↑↑u t)

The continuous linear time multiplier agrees with literal pointwise application.

theorem EulerTimeLp.timeMultiplier_pathLp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (u : C(↑(Set.Icc 0 T), E)) : (timeMultiplier T hT A) (pathLp T hT u) = pathLp T hT { toFun := fun (t : ↑(Set.Icc 0 T)) => (A t) (u t), continuous_toFun := ⋯ }

A continuous path is carried to its actual pointwise operator path by the Bochner multiplier.