Integration by parts for an actual H¹ representative against zero-endpoint tests. The identity follows from the proved primitive representation and does not posit a weak derivative as an additional assumption.

theorem EulerTimeH1WeakPairing.inner_zero_trace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (p q : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hp : ↑↑p =ᵐ[EulerTimeLp.timeMeasure T] η) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑q t) t) (v : ↥(EulerTimeLp.TimeLp T E)) (hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0) : inner ℝ p v = -inner ℝ q ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)

theorem EulerTimeH1WeakPairing.pathLp_inner_zero_trace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (v : ↥(EulerTimeLp.TimeLp T E)) (hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0) : inner ℝ (EulerTimeLp.pathLp T hT p) v = -inner ℝ (EulerTimeLp.pathLp T hT q) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)

A continuous derivative on the closed interval gives the exact weak pairing of the corresponding genuine time L² elements.