Quantitative pointwise bounds for genuine time-H¹ representatives

Absolute continuity and the actual Bochner L² derivative give exact integral increments, square-root continuity, and initial/terminal trace bounds.

theorem EulerTimeH1PointwiseBounds.eq_primitive_add_terminal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (g : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑g t) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : η t = EulerTerminalTimePrimitive.realPrimitive T g t + η T

The terminal primitive plus the actual terminal value reconstructs any H¹ representative.

theorem EulerTimeH1PointwiseBounds.increment_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (g : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑g t) t) (s t : ℝ) (hs : s ∈ Set.Icc 0 T) (ht : t ∈ Set.Icc 0 T) : η t - η s = ∫ (r : ℝ) in s..t, EulerTerminalTimePrimitive.zeroExtension T g r

The increment is the actual integral of the L² derivative's zero extension.

theorem EulerTimeH1PointwiseBounds.increment_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (g : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑g t) t) (s t : ℝ) (hs : s ∈ Set.Icc 0 T) (ht : t ∈ Set.Icc 0 T) (hst : s ≤ t) : ‖η t - η s‖ ^ 2 ≤ (t - s) * ‖g‖ ^ 2

The exact square-root modulus follows from Bochner Cauchy--Schwarz.

theorem EulerTimeH1PointwiseBounds.increment_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (g : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑g t) t) (s t : ℝ) (hs : s ∈ Set.Icc 0 T) (ht : t ∈ Set.Icc 0 T) (hst : s ≤ t) : ‖η t - η s‖ ≤ √(t - s) * ‖g‖

A genuine H¹ path has the quantitative square-root continuity bound.

theorem EulerTimeH1PointwiseBounds.norm_le_initial_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (g : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑g t) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ‖η t‖ ≤ ‖η 0‖ + √t * ‖g‖

The actual initial trace and L² derivative control the whole time path.

theorem EulerTimeH1PointwiseBounds.norm_le_initial_add_uniform {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (g : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑g t) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ‖η t‖ ≤ ‖η 0‖ + √T * ‖g‖

The uniform-in-time version needed by fixed-index inverse estimates.

theorem EulerTimeH1PointwiseBounds.norm_le_terminal_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (g : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑g t) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ‖η t‖ ≤ ‖η T‖ + √(T - t) * ‖g‖

The actual terminal trace has the corresponding backward-in-time bound.