Operator products of genuine H¹ fields with arbitrary terminal trace

Unlike a terminal primitive, a momentum field need not vanish at the final time. This file constructs the derivative of a C¹ coefficient times any actual AC representative with Bochner L² value and derivative classes.

noncomputable def EulerTimeH1FieldProduct.fieldProductDerivative {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)) (p q : ↥(EulerTimeLp.TimeLp T E)) : ↥(EulerTimeLp.TimeLp T F)

The product derivative is constructed in the actual L² space.

Equations

• EulerTimeH1FieldProduct.fieldProductDerivative T hT A A' p q = (EulerTimeLp.timeMultiplier T hT A') p + (EulerTimeLp.timeMultiplier T hT A) q

theorem EulerTimeH1FieldProduct.fieldProductDerivative_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)) (p q : ↥(EulerTimeLp.TimeLp T E)) : ↑↑(fieldProductDerivative T hT A A' p q) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A' t) (↑↑p t) + (EulerVolterraConvolution.extendPath T hT A t) (↑↑q t)

The constructed derivative is the pointwise Leibniz expression a.e.

theorem EulerTimeH1FieldProduct.fieldProduct_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)) (p : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hp : ↑↑p =ᵐ[EulerTimeLp.timeMeasure T] η) : ↑↑((EulerTimeLp.timeMultiplier T hT A) p) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A t) (η t)

The actual Bochner product has the given continuous product representative.

theorem EulerTimeH1FieldProduct.operatorPath_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)) (hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A' t) (Set.Icc 0 T) ↑t) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (EulerVolterraConvolution.extendPath T hT A) (EulerVolterraConvolution.extendPath T hT A' t) t

Within-interval coefficient derivatives give genuine derivatives almost everywhere; endpoints have zero time measure.

theorem EulerTimeH1FieldProduct.fieldProduct_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) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A t) (η t)) 0 T

C¹ operator application preserves actual absolute continuity.

theorem EulerTimeH1FieldProduct.fieldProduct_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)) (hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A' t) (Set.Icc 0 T) ↑t) (p q : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hp : ↑↑p =ᵐ[EulerTimeLp.timeMeasure T] η) (hηder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑q t) t) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath T hT A r) (η r)) (↑↑(fieldProductDerivative T hT A A' p q) t) t

The L² product derivative is the derivative of the actual product representative. No vanishing terminal trace is assumed.

theorem EulerTimeH1FieldProduct.fieldProduct_h1 {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) (p q : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hp : ↑↑p =ᵐ[EulerTimeLp.timeMeasure T] η) (hηder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑q t) t) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A t) (η t)) 0 T ∧ (↑↑((EulerTimeLp.timeMultiplier T hT A) p) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (EulerVolterraConvolution.extendPath T hT A t) (η t)) ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath T hT A r) (η r)) (↑↑(fieldProductDerivative T hT A A' p q) t) t

A complete H¹ product conclusion, with actual value and derivative classes.

theorem EulerTimeH1FieldProduct.fieldProductDerivative_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)) (p q : ↥(EulerTimeLp.TimeLp T E)) : ‖fieldProductDerivative T hT A A' p q‖ ≤ ‖A'‖ * ‖p‖ + ‖A‖ * ‖q‖

The constructed derivative has the expected operator-norm bound.