Strong Bochner energy passage on every genuine subinterval of the original time interval.

noncomputable def EulerTimeLpSubinterval.subintervalWeight (T s t : ℝ) (c : ↥(EulerTimeLp.TimeLp T ℝ)) : ↥(EulerTimeLp.TimeLp T ℝ)

Restrict a genuine scalar L² coefficient to a measurable closed time subinterval.

Equations

• EulerTimeLpSubinterval.subintervalWeight T s t c = MeasureTheory.MemLp.toLp ((Set.Icc s t).indicator ↑↑c) ⋯

theorem EulerTimeLpSubinterval.subintervalWeight_ae (T s t : ℝ) (c : ↥(EulerTimeLp.TimeLp T ℝ)) : ↑↑(subintervalWeight T s t c) =ᵐ[EulerTimeLp.timeMeasure T] (Set.Icc s t).indicator ↑↑c

The subinterval coefficient has its actual indicator representative.

theorem EulerTimeLpSubinterval.subinterval_inner_eq (T s t : ℝ) (c f : ↥(EulerTimeLp.TimeLp T ℝ)) : inner ℝ (subintervalWeight T s t c) f = ∫ (r : ℝ) in Set.Icc s t, ↑↑c r * ↑↑f r ∂EulerTimeLp.timeMeasure T

A subinterval pairing is exactly the integral of the actual forcing over that subinterval.

theorem EulerTimeLpSubinterval.subinterval_path_inner (T : ℝ) (hT : 0 ≤ T) (s t : ℝ) (h0s : 0 ≤ s) (hst : s ≤ t) (htT : t ≤ T) (a b : C(↑(Set.Icc 0 T), ℝ)) : inner ℝ (subintervalWeight T s t (EulerTimeLp.pathLp T hT a)) (EulerTimeLp.pathLp T hT b) = ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT b r

For actual continuous paths a subinterval pairing is the ordinary interval integral.

theorem EulerTimeLpSubinterval.subinterval_path_tendsto (T : ℝ) (hT : 0 ≤ T) (s t : ℝ) (h0s : 0 ≤ s) (hst : s ≤ t) (htT : t ≤ T) (a : C(↑(Set.Icc 0 T), ℝ)) (X : ℕ → C(↑(Set.Icc 0 T), ℝ)) (x : C(↑(Set.Icc 0 T), ℝ)) (hX : Filter.Tendsto X Filter.atTop (nhds x)) : Filter.Tendsto (fun (n : ℕ) => ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT (X n) r) Filter.atTop (nhds (∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT x r))

Uniform scalar path limits preserve every signed subinterval integral.

theorem EulerTimeLpSubinterval.subinterval_forcing_tendsto (T s t : ℝ) (c : ↥(EulerTimeLp.TimeLp T ℝ)) (F : ℕ → ↥(EulerTimeLp.TimeLp T ℝ)) (f : ↥(EulerTimeLp.TimeLp T ℝ)) (hF : Filter.Tendsto F Filter.atTop (nhds f)) : Filter.Tendsto (fun (n : ℕ) => ∫ (r : ℝ) in Set.Icc s t, ↑↑c r * ↑↑(F n) r ∂EulerTimeLp.timeMeasure T) Filter.atTop (nhds (∫ (r : ℝ) in Set.Icc s t, ↑↑c r * ↑↑f r ∂EulerTimeLp.timeMeasure T))

Strong L² time limits preserve every actual signed subinterval forcing integral.

theorem EulerTimeLpSubinterval.integral_energy_subinterval_limit (T : ℝ) (hT : 0 ≤ T) (s t : ℝ) (h0s : 0 ≤ s) (hst : s ≤ t) (htT : t ≤ T) (a b : C(↑(Set.Icc 0 T), ℝ)) (c : ↥(EulerTimeLp.TimeLp T ℝ)) (X Y : ℕ → C(↑(Set.Icc 0 T), ℝ)) (F : ℕ → ↥(EulerTimeLp.TimeLp T ℝ)) (x y : C(↑(Set.Icc 0 T), ℝ)) (f : ↥(EulerTimeLp.TimeLp T ℝ)) (hX : Filter.Tendsto X Filter.atTop (nhds x)) (hY : Filter.Tendsto Y Filter.atTop (nhds y)) (hF : Filter.Tendsto F Filter.atTop (nhds f)) (henergy : ∀ (n : ℕ), (X n) ⟨t, ⋯⟩ - (X n) ⟨s, ⋯⟩ ≤ ((∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT (X n) r) + ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT b r * EulerVolterraConvolution.extendPath T hT (Y n) r) + ∫ (r : ℝ) in Set.Icc s t, ↑↑c r * ↑↑(F n) r ∂EulerTimeLp.timeMeasure T) : 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, ↑↑c r * ↑↑f r ∂EulerTimeLp.timeMeasure T

Actual integral energy bounds pass to limits on each subinterval, with the radius term retaining its sign.