Actual integral pairings and their strong limits for metric energy passage.

theorem EulerTimeLpPairing.inner_eq_integral (T : ℝ) (a b : ↥(EulerTimeLp.TimeLp T ℝ)) : inner ℝ a b = ∫ (t : ℝ), ↑↑a t * ↑↑b t ∂EulerTimeLp.timeMeasure T

The actual scalar Bochner inner product is the integral of the literal product.

theorem EulerTimeLpPairing.path_inner_eq_integral (T : ℝ) (hT : 0 ≤ T) (a b : C(↑(Set.Icc 0 T), ℝ)) : inner ℝ (EulerTimeLp.pathLp T hT a) (EulerTimeLp.pathLp T hT b) = ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT a t * EulerVolterraConvolution.extendPath T hT b t

Continuous-path Bochner pairings equal the ordinary interval integral.

theorem EulerTimeLpPairing.integral_product_path_tendsto (T : ℝ) (hT : 0 ≤ T) (a : C(↑(Set.Icc 0 T), ℝ)) (f : ℕ → C(↑(Set.Icc 0 T), ℝ)) (g : C(↑(Set.Icc 0 T), ℝ)) (hf : Filter.Tendsto f Filter.atTop (nhds g)) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT a t * EulerVolterraConvolution.extendPath T hT (f n) t) Filter.atTop (nhds (∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT a t * EulerVolterraConvolution.extendPath T hT g t))

Signed integral coefficients pass continuously through uniform scalar energy convergence.

theorem EulerTimeLpPairing.integral_product_timeLp_tendsto (T : ℝ) (a : ↥(EulerTimeLp.TimeLp T ℝ)) (f : ℕ → ↥(EulerTimeLp.TimeLp T ℝ)) (g : ↥(EulerTimeLp.TimeLp T ℝ)) (hf : Filter.Tendsto f Filter.atTop (nhds g)) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ), ↑↑a t * ↑↑(f n) t ∂EulerTimeLp.timeMeasure T) Filter.atTop (nhds (∫ (t : ℝ), ↑↑a t * ↑↑g t ∂EulerTimeLp.timeMeasure T))

Strong Bochner convergence passes signed scalar weighted integrals to their actual limit.

theorem EulerTimeLpPairing.integral_three_paths (T : ℝ) (hT : 0 ≤ T) (a b c x y f : C(↑(Set.Icc 0 T), ℝ)) : ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT a t * EulerVolterraConvolution.extendPath T hT x t + EulerVolterraConvolution.extendPath T hT b t * EulerVolterraConvolution.extendPath T hT y t + EulerVolterraConvolution.extendPath T hT c t * EulerVolterraConvolution.extendPath T hT f t = ((∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT a t * EulerVolterraConvolution.extendPath T hT x t) + ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT b t * EulerVolterraConvolution.extendPath T hT y t) + ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT c t * EulerVolterraConvolution.extendPath T hT f t

Three continuous weighted scalar paths have the literal additive interval integral.

theorem EulerTimeLpPairing.integral_energy_limit (T : ℝ) (hT : 0 ≤ 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) ⟨0, ⋯⟩ ≤ ((∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT a t * EulerVolterraConvolution.extendPath T hT (X n) t) + ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT b t * EulerVolterraConvolution.extendPath T hT (Y n) t) + ∫ (t : ℝ), ↑↑c t * ↑↑(F n) t ∂EulerTimeLp.timeMeasure T) : x ⟨T, ⋯⟩ - x ⟨0, ⋯⟩ ≤ ((∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT a t * EulerVolterraConvolution.extendPath T hT x t) + ∫ (t : ℝ) in 0..T, EulerVolterraConvolution.extendPath T hT b t * EulerVolterraConvolution.extendPath T hT y t) + ∫ (t : ℝ), ↑↑c t * ↑↑f t ∂EulerTimeLp.timeMeasure T

An actual integral energy inequality survives uniform state convergence and strong L² forcing convergence, with the signed loss term unchanged.