Initial-zero versions of the actual H¹ product and reconstruction lemmas. These permit nonzero terminal values and hence explicit affine coordinate lifts in the fixed-space endpoint problem.

theorem EulerInitialTimePrimitive.eq_initialRealPrimitive_of_ac_hasDerivAt_ae {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑u t) t) (hzero : η 0 = 0) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : η t = initialRealPrimitive T u t

theorem EulerInitialTimePrimitive.initialPrimitiveTimeLp_eq_primitive_of_trace_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) (hu : (EulerTerminalTimePrimitive.initialTrace T hT) u = 0) : (initialPrimitiveTimeLp T hT) u = (EulerTerminalTimePrimitive.primitiveTimeLp T hT) u

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

Initial product derivative, given by (timeMultiplier T hT A₁).comp (initialPrimitiveTimeLp T hT) + timeMultiplier T hT A.

Equations

• EulerInitialTimePrimitive.initialProductDerivative T hT A A₁ = EulerTimeLp.timeMultiplier T hT A₁ ∘SL EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT + EulerTimeLp.timeMultiplier T hT A

noncomputable def EulerInitialTimePrimitive.initialProductPrimitive {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 : ↥(EulerTimeLp.TimeLp T E)) (t : ℝ) : F

Initial product primitive, given by extendPath T hT A t (initialRealPrimitive T u t).

Equations

• EulerInitialTimePrimitive.initialProductPrimitive T hT A u t = (EulerVolterraConvolution.extendPath T hT A t) (EulerInitialTimePrimitive.initialRealPrimitive T u t)

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

theorem EulerInitialTimePrimitive.initialProductPrimitive_absolutelyContinuous {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A A₁ : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) : AbsolutelyContinuousOnInterval (initialProductPrimitive T hT A u) 0 T

theorem EulerInitialTimePrimitive.initialProductPrimitive_hasDerivAt_ae {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A A₁ : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (initialProductPrimitive T hT A u) (↑↑((initialProductDerivative T hT A A₁) u) t) t

theorem EulerInitialTimePrimitive.initialPrimitive_initialProductDerivative {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (T : ℝ) (hT : 0 ≤ T) (A A₁ : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A₁ t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ↑(Set.Icc 0 T)) : ((initialPrimitive T hT) ((initialProductDerivative T hT A A₁) u)) t = (A t) (((initialPrimitive T hT) u) t)

theorem EulerInitialTimePrimitive.initialProductDerivative_eq_product_of_trace_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A A₁ : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (u : ↥(EulerTimeLp.TimeLp T E)) (hu : (EulerTerminalTimePrimitive.initialTrace T hT) u = 0) : (initialProductDerivative T hT A A₁) u = (EulerTimeH1OperatorProduct.productDerivative T hT A A₁) u

noncomputable def EulerInitialTimePrimitive.constantFieldOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) : E →L[ℝ] ↥(EulerTimeLp.TimeLp T E)

Constants embedded as a genuine bounded operator into time L².

Equations

• EulerInitialTimePrimitive.constantFieldOperator T hT = EulerTimeLp.pathLpOperator T hT ∘SL ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T)

theorem EulerInitialTimePrimitive.constantFieldOperator_ae {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (x : E) : ↑↑((constantFieldOperator T hT) x) =ᵐ[EulerTimeLp.timeMeasure T] fun (x_1 : ℝ) => x

theorem EulerInitialTimePrimitive.initialPrimitive_constantFieldOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (x : E) (t : ↑(Set.Icc 0 T)) : ((initialPrimitive T hT) ((constantFieldOperator T hT) x)) t = ↑t • x