Uniqueness for the complex linear regularized mild equation

An exponential time weight makes the Volterra map a contraction on any finite interval for a fixed continuous physical coefficient path.

theorem CKN.Leray.regularisedComplexLinearVolterra_unique (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 ≤ T) (g : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2)) (b : ↥ComplexVectorL2) (u v : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2)) (hu : ∀ (t : ↑(RegularizedMildTimeInterval T)), u t = heatSemigroup ↑t ⋯ b - ∫ (τ : ℝ) in 0..T, if h : 0 < τ ∧ τ < ↑t then stokesL2Operator ⋯ (((regularisedTensorPhysicalMap ρ ε hε) (g (regularizedMildTimeClamp T hT (↑t - τ)))) (u (regularizedMildTimeClamp T hT (↑t - τ)))) else 0) (hv : ∀ (t : ↑(RegularizedMildTimeInterval T)), v t = heatSemigroup ↑t ⋯ b - ∫ (τ : ℝ) in 0..T, if h : 0 < τ ∧ τ < ↑t then stokesL2Operator ⋯ (((regularisedTensorPhysicalMap ρ ε hε) (g (regularizedMildTimeClamp T hT (↑t - τ)))) (v (regularizedMildTimeClamp T hT (↑t - τ)))) else 0) : u = v

A continuous complex physical trajectory solving the linear Volterra equation with a prescribed continuous coefficient is unique on every finite interval.