Uniqueness, initial traces, and genuine positive time budgets for the Volterra construction.

theorem EulerVolterraConvolution.mild_solution_unique {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (k : ℝ → ℝ) (hK : ContinuousOn (fun (p : ℝ × Y) => (K p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hk : MeasureTheory.IntegrableOn k (Set.Ioc 0 T) MeasureTheory.volume) (hk0 : ∀ r ∈ Set.Ioc 0 T, 0 ≤ k r) (hbound : ∀ r ∈ Set.Ioc 0 T, ∀ (y : Y), ‖(K r) y‖ ≤ k r * ‖y‖) (a : C(↑(Set.Icc 0 T), X)) (F : ↑(Set.Icc 0 T) → X → Y) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × X) => F p.1 p.2) (R L : ℝ) (hL : 0 ≤ L) (hFL : ∀ (t : ↑(Set.Icc 0 T)) (x y : X), ‖x‖ ≤ R → ‖y‖ ≤ R → ‖F t x - F t y‖ ≤ L * ‖x - y‖) (hsmall : kernelMass T k * L < 1) (u v : C(↑(Set.Icc 0 T), X)) (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ R) (hsolu : ∀ (t : ↑(Set.Icc 0 T)), u t = a t + ∫ (r : ℝ) in 0..↑t, (K r) (F (Set.projIcc 0 T hT (↑t - r)) (u (Set.projIcc 0 T hT (↑t - r))))) (hsolv : ∀ (t : ↑(Set.Icc 0 T)), v t = a t + ∫ (r : ℝ) in 0..↑t, (K r) (F (Set.projIcc 0 T hT (↑t - r)) (v (Set.projIcc 0 T hT (↑t - r))))) : u = v

Two actual mild solutions in the contraction ball agree as continuous paths.

theorem EulerVolterraConvolution.mild_solution_initial {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (a u : C(↑(Set.Icc 0 T), X)) (F : ↑(Set.Icc 0 T) → X → Y) (hsol : ∀ (t : ↑(Set.Icc 0 T)), u t = a t + ∫ (r : ℝ) in 0..↑t, (K r) (F (Set.projIcc 0 T hT (↑t - r)) (u (Set.projIcc 0 T hT (↑t - r))))) : u ⟨0, ⋯⟩ = a ⟨0, ⋯⟩

The actual Volterra integral vanishes at time zero, giving the prescribed initial trace.

theorem EulerSobolevHeat.parabolicConstant_nonneg (ν : ℝ) : 0 ≤ parabolicConstant ν

The viscosity-dependent coefficient in the parabolic kernel bound is nonnegative.

theorem EulerSobolevHeat.parabolic_mass_continuous (ν : ℝ) : Continuous fun (T : ℝ) => T + 2 * parabolicConstant ν * √T

The explicit parabolic kernel mass is continuous at zero and vanishes there.

theorem EulerSobolevHeat.exists_positive_time_budget (ν M L margin Tmax : ℝ) (hmargin : 0 < margin) (hTmax : 0 < Tmax) : ∃ (T : ℝ), 0 < T ∧ T ≤ Tmax ∧ (T + 2 * parabolicConstant ν * √T) * M < margin ∧ (T + 2 * parabolicConstant ν * √T) * L < 1

The actual parabolic kernel has a strictly positive interval satisfying both Picard budgets.