Recovering the actual initial trace from a full time weak identity

The terminal primitive and its exact integration-by-parts identity identify both an absolutely continuous representative and its initial trace. The boundary value is a conclusion of testing against all terminal-zero H¹ paths.

theorem EulerTimeWeakBoundary.weak_boundary_eq_primitive_add_constant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (p h : ↥(EulerTimeLp.TimeLp T E)) (b : E) (hweak : ∀ (v : ↥(EulerTimeLp.TimeLp T E)), inner ℝ p v + inner ℝ h ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v) + inner ℝ b ((EulerTerminalTimePrimitive.initialTrace T hT) v) = 0) : p = (EulerTerminalTimePrimitive.primitiveTimeLp T hT) h + EulerTimeWeakDerivative.constantField T hT (b - (EulerTerminalTimePrimitive.initialTrace T hT) h)

The full weak identity determines the integration constant explicitly.

noncomputable def EulerTimeWeakBoundary.boundaryRepresentative {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (h : ↥(EulerTimeLp.TimeLp T E)) (b : E) : ℝ → E

The actual AC representative with the boundary value forced by the weak form.

Equations

• EulerTimeWeakBoundary.boundaryRepresentative T hT h b t = EulerTerminalTimePrimitive.realPrimitive T h t + (b - (EulerTerminalTimePrimitive.initialTrace T hT) h)

@[simp]

theorem EulerTimeWeakBoundary.boundaryRepresentative_initial {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (h : ↥(EulerTimeLp.TimeLp T E)) (b : E) : boundaryRepresentative T hT h b 0 = b

This representative has precisely the initial value appearing in the weak form.

theorem EulerTimeWeakBoundary.boundaryRepresentative_absolutelyContinuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (h : ↥(EulerTimeLp.TimeLp T E)) (b : E) : AbsolutelyContinuousOnInterval (boundaryRepresentative T hT h b) 0 T

The explicitly reconstructed representative is genuinely absolutely continuous.

theorem EulerTimeWeakBoundary.boundaryRepresentative_hasDerivAt_ae {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (h : ↥(EulerTimeLp.TimeLp T E)) (b : E) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (boundaryRepresentative T hT h b) (↑↑h t) t

Its a.e. derivative is the actual L² field in the weak identity.

theorem EulerTimeWeakBoundary.weak_boundary_representation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (p h : ↥(EulerTimeLp.TimeLp T E)) (b : E) (hweak : ∀ (v : ↥(EulerTimeLp.TimeLp T E)), inner ℝ p v + inner ℝ h ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v) + inner ℝ b ((EulerTerminalTimePrimitive.initialTrace T hT) v) = 0) : ↑↑p =ᵐ[EulerTimeLp.timeMeasure T] boundaryRepresentative T hT h b

The full weak identity identifies its original L² field with this actual representative, not merely with a formal boundary functional.

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

Existence of a genuine AC representative with the derived initial trace and prescribed a.e. derivative; this also covers the degenerate zero-length interval.