Actual L² forcing bounds imply continuous scalar integral majorants on every time subinterval.

theorem EulerTimeLpSubintervalBound.integrable_time_product (T : ℝ) (u v : ↥(EulerTimeLp.TimeLp T ℝ)) : MeasureTheory.Integrable (fun (t : ℝ) => ↑↑u t * ↑↑v t) (EulerTimeLp.timeMeasure T)

Two genuine real L² time fields have an integrable product.

theorem EulerTimeLpSubintervalBound.subinterval_forcing_bound (T : ℝ) (hT : 0 ≤ T) (s t : ℝ) (h0s : 0 ≤ s) (hst : s ≤ t) (htT : t ≤ T) (k g : C(↑(Set.Icc 0 T), ℝ)) (hk : ∀ (r : ↑(Set.Icc 0 T)), 0 ≤ k r) (F : ↥(EulerTimeLp.TimeLp T ℝ)) (hF : ↑↑F ≤ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT g) : ∫ (r : ℝ) in Set.Icc s t, ↑↑(EulerTimeLp.pathLp T hT k) r * ↑↑F r ∂EulerTimeLp.timeMeasure T ≤ ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT k r * EulerVolterraConvolution.extendPath T hT g r

A genuine almost-everywhere forcing bound gives its signed coefficient comparison on every time subinterval.

def EulerTimeLpSubintervalBound.scalarEnergyRhs (T : ℝ) (a b k X Y F : C(↑(Set.Icc 0 T), ℝ)) : C(↑(Set.Icc 0 T), ℝ)

The actual continuous scalar right-hand side after an almost-everywhere forcing estimate.

Equations

• EulerTimeLpSubintervalBound.scalarEnergyRhs T a b k X Y F = a * X + b * Y + k * F

theorem EulerTimeLpSubintervalBound.scalar_rhs_subinterval (T : ℝ) (hT : 0 ≤ T) (s t : ℝ) (h0s : 0 ≤ s) (hst : s ≤ t) (htT : t ≤ T) (a b k X Y g : C(↑(Set.Icc 0 T), ℝ)) (hk : ∀ (r : ↑(Set.Icc 0 T)), 0 ≤ k r) (F : ↥(EulerTimeLp.TimeLp T ℝ)) (hF : ↑↑F ≤ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT g) (he : X ⟨t, ⋯⟩ - X ⟨s, ⋯⟩ ≤ ((∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT X r) + ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT b r * EulerVolterraConvolution.extendPath T hT Y r) + ∫ (r : ℝ) in Set.Icc s t, ↑↑(EulerTimeLp.pathLp T hT k) r * ↑↑F r ∂EulerTimeLp.timeMeasure T) : X ⟨t, ⋯⟩ - X ⟨s, ⋯⟩ ≤ ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT (scalarEnergyRhs T a b k X Y g) r

Passing the actual forcing estimate through the integral yields a continuous scalar energy majorant.