Products of genuine time-H¹ paths and differentiable operator paths

The product derivative is constructed in the actual Bochner L² space from the coefficient multiplier and terminal primitive. Its integral is identified with the literal pointwise product by absolute continuity and uniqueness of primitives.

theorem EulerTimeH1OperatorProduct.clm_apply_absolutelyContinuous {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {A : ℝ → E →L[ℝ] F} {u : ℝ → E} (hA : AbsolutelyContinuousOnInterval A a b) (hu : AbsolutelyContinuousOnInterval u a b) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => (A t) (u t)) a b

Pointwise application of two absolutely continuous operator/vector paths is absolutely continuous. The estimate uses their actual compact-interval bounds.

theorem EulerTimeH1OperatorProduct.operatorPath_hasDerivWithinAt_of_extension {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)) (a : ℝ → E →L[ℝ] F) (ha : ∀ (t : ↑(Set.Icc 0 T)), A t = a ↑t) (hader : ∀ (t : ↑(Set.Icc 0 T)), HasDerivAt a (A' t) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A' t) (Set.Icc 0 T) ↑t

A genuine differentiable extension supplies the within-interval derivative hypothesis for its clamped continuous path, including both endpoints.

theorem EulerTimeH1OperatorProduct.operatorPath_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)) (hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A' t) (Set.Icc 0 T) ↑t) : AbsolutelyContinuousOnInterval (EulerVolterraConvolution.extendPath T hT A) 0 T

Within-interval differentiability with a continuous derivative implies actual absolute continuity of the clamped coefficient path.

noncomputable def EulerTimeH1OperatorProduct.productDerivative {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)

The derivative of A(t) Ju(t), constructed as an actual bounded L² operator.

Equations

• EulerTimeH1OperatorProduct.productDerivative T hT A A' = EulerTimeLp.timeMultiplier T hT A' ∘SL EulerTerminalTimePrimitive.primitiveTimeLp T hT + EulerTimeLp.timeMultiplier T hT A

theorem EulerTimeH1OperatorProduct.productDerivative_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)) : ↑↑((productDerivative T hT A A') u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A' t) (EulerTerminalTimePrimitive.realPrimitive T u t) + (EulerVolterraConvolution.extendPath T hT A t) (↑↑u t)

The product derivative has its literal Leibniz-rule representative.

noncomputable def EulerTimeH1OperatorProduct.productPrimitive {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)) : ℝ → F

The actual pointwise coefficient-times-primitive path.

Equations

• EulerTimeH1OperatorProduct.productPrimitive T hT A u t = (EulerVolterraConvolution.extendPath T hT A t) (EulerTerminalTimePrimitive.realPrimitive T u t)

@[simp]

theorem EulerTimeH1OperatorProduct.productPrimitive_terminal {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)) : productPrimitive T hT A u T = 0

Every such product has zero terminal trace.

theorem EulerTimeH1OperatorProduct.productPrimitive_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)) (hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A' t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) : AbsolutelyContinuousOnInterval (productPrimitive T hT A u) 0 T

The product path is genuinely absolutely continuous.

theorem EulerTimeH1OperatorProduct.productPrimitive_hasDerivAt_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)) [CompleteSpace E] (hA : ∀ (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 (productPrimitive T hT A u) (↑↑((productDerivative T hT A A') u) t) t

The constructed L² field is the actual a.e. derivative of the pointwise product.

theorem EulerTimeH1OperatorProduct.productPrimitive_eq_realPrimitive {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)) [CompleteSpace E] [CompleteSpace F] (hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A' t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : productPrimitive T hT A u t = EulerTerminalTimePrimitive.realPrimitive T ((productDerivative T hT A A') u) t

The literal product is the terminal primitive of the derivative constructed in L². This identifies the product as a genuine terminal-zero H¹ path.

theorem EulerTimeH1OperatorProduct.terminalPrimitive_productDerivative {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)) [CompleteSpace E] [CompleteSpace F] (hA : ∀ (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)) : ((EulerTerminalTimePrimitive.terminalPrimitive T hT) ((productDerivative T hT A A') u)) t = (A t) (((EulerTerminalTimePrimitive.terminalPrimitive T hT) u) t)

Integrating the product derivative recovers the literal pointwise product at every time, including both endpoints.

theorem EulerTimeH1OperatorProduct.primitiveTimeLp_productDerivative {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)) [CompleteSpace E] [CompleteSpace F] (hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A' t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) : (EulerTerminalTimePrimitive.primitiveTimeLp T hT) ((productDerivative T hT A A') u) = (EulerTimeLp.timeMultiplier T hT A) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) u)

The same product rule is an exact identity of actual Bochner L² fields.

theorem EulerTimeH1OperatorProduct.initialTrace_productDerivative {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)) [CompleteSpace E] [CompleteSpace F] (hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A' t) (Set.Icc 0 T) ↑t) (u : ↥(EulerTimeLp.TimeLp T E)) : (EulerTerminalTimePrimitive.initialTrace T hT) ((productDerivative T hT A A') u) = (A ⟨0, ⋯⟩) ((EulerTerminalTimePrimitive.initialTrace T hT) u)

The actual initial trace transforms by the coefficient's initial value.

theorem EulerTimeH1OperatorProduct.productDerivative_norm_le {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)) : ‖(productDerivative T hT A A') u‖ ≤ (‖A'‖ * √(T ^ 2 / 2) + ‖A‖) * ‖u‖

A uniform bound on the actual derivative in terms of the coefficient and its derivative; the time primitive retains its sharp square-root bound.