Weighted complex physical Stokes bound

An exponential weight makes the linear Volterra operator small on a fixed finite interval, independent of its length.

theorem CKN.Leray.regularisedComplexShiftedStokesIntegral_weighted_norm_le (F : ℝ → ↥ComplexTensorL2) (T t M lam : ℝ) (hT : 0 ≤ T) (ht : t ≤ T) (hM : 0 ≤ M) (hlam : 0 < lam) (hF : ∀ (s : ℝ), 0 ≤ s → s ≤ T → ‖F s‖ ≤ M * Real.exp (lam * s)) : ‖∫ (τ : ℝ) in 0..T, regularisedComplexShiftedStokesIntegrand F t τ‖ ≤ M / √(2 * Real.exp 1) * Real.exp (lam * t) * (lam ^ (-(1 / 2)) * Real.Gamma (1 / 2))

A tensor path controlled by an exponential weight has a translated Stokes integral controlled by the same weight and the Gamma kernel.