The smooth compactly supported limit step for the proposed Euler construction. The hypotheses are summable uniform estimates for every actual iterated Fréchet derivative of the increments. Smoothness and convergence of the limit are proved, not assumed. The divergence is the usual coordinate trace of the first derivative.

theorem EulerSmoothLimit.summable_values (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) (x : Space) : Summable fun (n : ℕ) => f n x

Order-zero bounds prove actual pointwise convergence of the series.

theorem EulerSmoothLimit.uniform_convergence (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) : TendstoUniformly (fun (N : ℕ) (x : Space) => ∑ n ∈ Finset.range N, f n x) (fun (x : Space) => ∑' (n : ℕ), f n x) Filter.atTop

Uniform convergence of the ordinary sequence of finite partial sums.

theorem EulerSmoothLimit.contDiff_sum (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) : ContDiff ℝ ↑⊤ fun (x : Space) => ∑' (n : ℕ), f n x

Every order of differentiability is retained by the convergent series.

theorem EulerSmoothLimit.iterated_derivative_sum (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) (k : ℕ) (x : Space) : iteratedFDeriv ℝ k (fun (y : Space) => ∑' (n : ℕ), f n y) x = ∑' (n : ℕ), iteratedFDeriv ℝ k (f n) x

All iterated derivatives of the sum are the sums of the actual derivatives.

theorem EulerSmoothLimit.uniform_derivative_convergence (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) (k : ℕ) : TendstoUniformly (fun (N : ℕ) (x : Space) => ∑ n ∈ Finset.range N, iteratedFDeriv ℝ k (f n) x) (iteratedFDeriv ℝ k fun (x : Space) => ∑' (n : ℕ), f n x) Filter.atTop

Uniform convergence holds separately at every derivative order.

theorem EulerSmoothLimit.tsupport_sum_subset (f : ℕ → Space → Space) (K : Set Space) (hK : IsClosed K) (hsupp : ∀ (n : ℕ), Function.support (f n) ⊆ K) : (tsupport fun (x : Space) => ∑' (n : ℕ), f n x) ⊆ K

A common closed support set also contains the topological support of the sum.

theorem EulerSmoothLimit.compactSupport_sum (f : ℕ → Space → Space) (K : Set Space) (hK : IsCompact K) (hsupp : ∀ (n : ℕ), Function.support (f n) ⊆ K) : HasCompactSupport fun (x : Space) => ∑' (n : ℕ), f n x

Compact support follows from the prescribed common compact set.

theorem EulerSmoothLimit.divergence_sum (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) (x : Space) : divergence (fun (y : Space) => ∑' (n : ℕ), f n y) x = ∑' (n : ℕ), divergence (f n) x

The divergence of the series is the series of the divergences.

theorem EulerSmoothLimit.divergence_free_sum (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) (hdiv : ∀ (n : ℕ) (x : Space), divergence (f n) x = 0) (x : Space) : divergence (fun (y : Space) => ∑' (n : ℕ), f n y) x = 0

The solenoidal condition is preserved by the series.

theorem EulerSmoothLimit.memLp_sum (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) (K : Set Space) (hK : IsCompact K) (hsupp : ∀ (n : ℕ), Function.support (f n) ⊆ K) (p : ENNReal) : MeasureTheory.MemLp (fun (x : Space) => ∑' (n : ℕ), f n x) p MeasureTheory.volume

The common-support smooth limit belongs to every L^p, in particular to L².

theorem EulerSmoothLimit.memLp_iterated_derivative_sum (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) (K : Set Space) (hK : IsCompact K) (hsupp : ∀ (n : ℕ), Function.support (f n) ⊆ K) (k : ℕ) (p : ENNReal) : MeasureTheory.MemLp (iteratedFDeriv ℝ k fun (x : Space) => ∑' (n : ℕ), f n x) p MeasureTheory.volume

Every derivative of the limit is also in every L^p.

theorem EulerSmoothLimit.finite_energy_sum (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) (K : Set Space) (hK : IsCompact K) (hsupp : ∀ (n : ℕ), Function.support (f n) ⊆ K) : MeasureTheory.Integrable (fun (x : Space) => ‖∑' (n : ℕ), f n x‖ ^ 2) MeasureTheory.volume

Finite kinetic energy is obtained as integrability of the squared Euclidean norm.

theorem EulerSmoothLimit.odd_sum (f : ℕ → Space → Space) (hodd : ∀ (n : ℕ) (x : Space), f n (-x) = -f n x) (x : Space) : ∑' (n : ℕ), f n (-x) = -∑' (n : ℕ), f n x

Odd parity also passes to the pointwise series.

theorem EulerSmoothLimit.smooth_compact_solenoidal_limit (f : ℕ → Space → Space) (v : ℕ → ℕ → ℝ) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hv : ∀ (k : ℕ), Summable (v k)) (hb : ∀ (k n : ℕ) (x : Space), ‖iteratedFDeriv ℝ k (f n) x‖ ≤ v k n) (K : Set Space) (hK : IsCompact K) (hsupp : ∀ (n : ℕ), Function.support (f n) ⊆ K) (hdiv : ∀ (n : ℕ) (x : Space), divergence (f n) x = 0) : ∃ (u : Space → Space), (∀ (x : Space), HasSum (fun (n : ℕ) => f n x) (u x)) ∧ TendstoUniformly (fun (N : ℕ) (x : Space) => ∑ n ∈ Finset.range N, f n x) u Filter.atTop ∧ ContDiff ℝ (↑⊤) u ∧ tsupport u ⊆ K ∧ HasCompactSupport u ∧ MeasureTheory.MemLp u 2 MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : Space) => ‖u x‖ ^ 2) MeasureTheory.volume ∧ (∀ (x : Space), divergence u x = 0) ∧ ∀ (k : ℕ) (x : Space), iteratedFDeriv ℝ k u x = ∑' (n : ℕ), iteratedFDeriv ℝ k (f n) x

Constructs the limit initial velocity with all required qualitative properties. The pointwise HasSum and uniform-convergence conclusions ensure the result is the actual series, and every derivative order is shown to commute with that sum.