Continuous derivatives upgrade genuine time-H¹ paths to classical paths

If the actual L² derivative has a continuous representative, terminal integration constructs a C¹ extension agreeing with the original AC path. Thus the time derivative holds at every interior time and within the closed interval at both endpoints.

noncomputable def EulerTimeH1ContinuousDerivative.continuousIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (q : C(↑(Set.Icc 0 T), E)) (t : ℝ) : E

Integrating the genuine continuous derivative after clamping time.

Equations

• EulerTimeH1ContinuousDerivative.continuousIntegral T hT q t = ∫ (r : ℝ) in T..t, EulerVolterraConvolution.extendPath T hT q r

theorem EulerTimeH1ContinuousDerivative.continuousIntegral_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (q : C(↑(Set.Icc 0 T), E)) (t : ℝ) : HasDerivAt (continuousIntegral T hT q) (EulerVolterraConvolution.extendPath T hT q t) t

This concrete integral has the prescribed derivative everywhere.

theorem EulerTimeH1ContinuousDerivative.continuousIntegral_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (q : C(↑(Set.Icc 0 T), E)) : ContDiff ℝ 1 (continuousIntegral T hT q)

The concrete integral is C¹ as a map on the real line.

theorem EulerTimeH1ContinuousDerivative.continuousIntegral_eq_realPrimitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (q : ↥(EulerTimeLp.TimeLp T E)) (qC : C(↑(Set.Icc 0 T), E)) (hq : ↑↑q =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT qC) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : continuousIntegral T hT qC t = EulerTerminalTimePrimitive.realPrimitive T q t

The continuous integral is the actual terminal primitive of its L² representative.

theorem EulerTimeH1ContinuousDerivative.eq_continuousIntegral_add_terminal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (q : ↥(EulerTimeLp.TimeLp T E)) (qC : C(↑(Set.Icc 0 T), E)) (hq : ↑↑q =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT qC) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (r : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑q r) r) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : η t = continuousIntegral T hT qC t + η T

A genuine H¹ path agrees with a concrete C¹ extension when its actual L² derivative has a continuous representative.

theorem EulerTimeH1ContinuousDerivative.hasDerivWithinAt_of_continuous_representative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (q : ↥(EulerTimeLp.TimeLp T E)) (qC : C(↑(Set.Icc 0 T), E)) (hq : ↑↑q =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT qC) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (r : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑q r) r) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt η (qC t) (Set.Icc 0 T) ↑t

The actual derivative is classical throughout the closed time interval, interpreting endpoint derivatives within that interval.

theorem EulerTimeH1ContinuousDerivative.hasDerivAt_of_continuous_representative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (q : ↥(EulerTimeLp.TimeLp T E)) (qC : C(↑(Set.Icc 0 T), E)) (hq : ↑↑q =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT qC) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (r : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑q r) r) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt η (qC ⟨t, ⋯⟩) t

At every interior time the actual AC path has an ordinary two-sided derivative.