Recovering actual time derivatives from the zero-endpoint weak identity

The terminal primitive is an explicit integral of an L² equivalence class. Integration by parts and the kernel of its initial trace identify the strong momentum representative used by the mean and transverse variational inverses.

theorem EulerTimeWeakDerivative.absolutelyContinuous_norm {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} {f : ℝ → E} (hf : AbsolutelyContinuousOnInterval f a b) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => ‖f t‖) a b

Taking norms preserves absolute continuity by the reverse triangle inequality.

theorem EulerTimeWeakDerivative.absolutelyContinuous_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a b : ℝ} {f g : ℝ → E} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => inner ℝ (f t) (g t)) a b

Real inner products of absolutely continuous Hilbert-valued paths are absolutely continuous; polarization reduces this to scalar products.

theorem EulerTimeWeakDerivative.primitive_inner_identity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f v : ↥(EulerTimeLp.TimeLp T E)) : inner ℝ ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) f) v + inner ℝ f ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v) = -inner ℝ ((EulerTerminalTimePrimitive.initialTrace T hT) f) ((EulerTerminalTimePrimitive.initialTrace T hT) v)

Exact integration by parts for the genuine L² terminal primitives.

theorem EulerTimeWeakDerivative.primitive_inner_zero_trace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f v : ↥(EulerTimeLp.TimeLp T E)) (hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0) : inner ℝ ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) f) v = -inner ℝ f ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)

Zero-endpoint tests remove the boundary term in primitive integration by parts.

noncomputable def EulerTimeWeakDerivative.constantField {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (hT : 0 ≤ T) (c : E) : ↥(EulerTimeLp.TimeLp T E)

An actual constant time field, embedded in Bochner L².

Equations

• EulerTimeWeakDerivative.constantField T hT c = EulerTimeLp.pathLp T hT (ContinuousMap.const (↑(Set.Icc 0 T)) c)

theorem EulerTimeWeakDerivative.constantField_ae {E : Type u_1} [NormedAddCommGroup E] (T : ℝ) (hT : 0 ≤ T) (c : E) : ↑↑(constantField T hT c) =ᵐ[EulerTimeLp.timeMeasure T] fun (x : ℝ) => c

The Bochner constant has its literal pointwise representative almost everywhere.

theorem EulerTimeWeakDerivative.initialTrace_eq_neg_integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) : (EulerTerminalTimePrimitive.initialTrace T hT) u = -∫ (t : ℝ), ↑↑u t ∂EulerTimeLp.timeMeasure T

The trace of the primitive is minus the Bochner integral of the derivative.

theorem EulerTimeWeakDerivative.constantField_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (c : E) (v : ↥(EulerTimeLp.TimeLp T E)) : inner ℝ (constantField T hT c) v = -inner ℝ c ((EulerTerminalTimePrimitive.initialTrace T hT) v)

Constant fields pair only with the initial trace of a terminal primitive.

theorem EulerTimeWeakDerivative.initialTrace_constantField {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (c : E) : (EulerTerminalTimePrimitive.initialTrace T hT) (constantField T hT c) = -T • c

The initial trace of a constant derivative is its value times minus the length.

theorem EulerTimeWeakDerivative.exists_constant_of_zero_trace_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 < T) (r : ↥(EulerTimeLp.TimeLp T E)) (hr : ∀ (v : ↥(EulerTimeLp.TimeLp T E)), (EulerTerminalTimePrimitive.initialTrace T ⋯) v = 0 → inner ℝ r v = 0) : ∃ (c : E), r = constantField T ⋯ c

Orthogonality to all zero-trace derivatives forces an actual constant L² field.

theorem EulerTimeWeakDerivative.weak_derivative_eq_primitive_add_constant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 < T) (p h : ↥(EulerTimeLp.TimeLp T E)) (hweak : ∀ (v : ↥(EulerTimeLp.TimeLp T E)), (EulerTerminalTimePrimitive.initialTrace T ⋯) v = 0 → inner ℝ p v = -inner ℝ h ((EulerTerminalTimePrimitive.primitiveTimeLp T ⋯) v)) : ∃ (c : E), p = (EulerTerminalTimePrimitive.primitiveTimeLp T ⋯) h + constantField T ⋯ c

The zero-endpoint weak derivative identity constructs an actual momentum representative: a terminal primitive plus a constant.

theorem EulerTimeWeakDerivative.exists_ac_representative_of_weak {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 < T) (p h : ↥(EulerTimeLp.TimeLp T E)) (hweak : ∀ (v : ↥(EulerTimeLp.TimeLp T E)), (EulerTerminalTimePrimitive.initialTrace T ⋯) v = 0 → inner ℝ p v = -inner ℝ h ((EulerTerminalTimePrimitive.primitiveTimeLp T ⋯) v)) : ∃ (η : ℝ → E), AbsolutelyContinuousOnInterval η 0 T ∧ ↑↑p =ᵐ[EulerTimeLp.timeMeasure T] η ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑h t) t

The weak identity supplies a genuine absolutely continuous representative whose almost-everywhere derivative is the prescribed momentum forcing.