Packet Existence

noncomputable def EulerPacketExistence.extendCurve {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) (α : C(↑(Set.Icc a b), E)) (t : ℝ) : E

Extend a continuous curve from a compact interval by endpoint values.

Equations

• EulerPacketExistence.extendCurve t₀ α t = α (Set.projIcc a b ⋯ t)

theorem EulerPacketExistence.continuous_extendCurve {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) (α : C(↑(Set.Icc a b), E)) : Continuous (extendCurve t₀ α)

theorem EulerPacketExistence.extendCurve_of_mem {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) (α : C(↑(Set.Icc a b), E)) {t : ℝ} (ht : t ∈ Set.Icc a b) : extendCurve t₀ α t = α ⟨t, ht⟩

theorem EulerPacketExistence.continuous_comp_extendCurve {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) {f : ℝ → E → E} (hf : Continuous (Function.uncurry f)) (α : C(↑(Set.Icc a b), E)) : Continuous fun (t : ℝ) => f t (extendCurve t₀ α t)

noncomputable def EulerPacketExistence.picardStep {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) {f : ℝ → E → E} (hf : Continuous (Function.uncurry f)) [NormedSpace ℝ E] [CompleteSpace E] (x : E) (α : C(↑(Set.Icc a b), E)) : C(↑(Set.Icc a b), E)

The Volterra map on all continuous curves, without a spatial-radius restriction. Global Lipschitz continuity makes an iterate contractive.

Equations

• EulerPacketExistence.picardStep t₀ hf x α = { toFun := fun (t : ↑(Set.Icc a b)) => x + ∫ (s : ℝ) in ↑t₀..↑t, f s (EulerPacketExistence.extendCurve t₀ α s), continuous_toFun := ⋯ }

theorem EulerPacketExistence.picardStep_apply {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) {f : ℝ → E → E} (hf : Continuous (Function.uncurry f)) [NormedSpace ℝ E] [CompleteSpace E] (x : E) (α : C(↑(Set.Icc a b), E)) (t : ↑(Set.Icc a b)) : (picardStep t₀ hf x α) t = x + ∫ (s : ℝ) in ↑t₀..↑t, f s (extendCurve t₀ α s)

theorem EulerPacketExistence.picard_iterate_point_bound {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) {f : ℝ → E → E} (hf : Continuous (Function.uncurry f)) [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (f t)) (x : E) (α β : C(↑(Set.Icc a b), E)) (n : ℕ) (t : ↑(Set.Icc a b)) : dist (((picardStep t₀ hf x)^[n] α) t) (((picardStep t₀ hf x)^[n] β) t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n.factorial * dist α β

theorem EulerPacketExistence.picard_iterate_bound {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) {f : ℝ → E → E} (hf : Continuous (Function.uncurry f)) [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (f t)) (x : E) (α β : C(↑(Set.Icc a b), E)) (n : ℕ) : dist ((picardStep t₀ hf x)^[n] α) ((picardStep t₀ hf x)^[n] β) ≤ (↑K * max (b - ↑t₀) (↑t₀ - a)) ^ n / ↑n.factorial * dist α β

theorem EulerPacketExistence.exists_picard_fixed_point {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) {f : ℝ → E → E} (hf : Continuous (Function.uncurry f)) [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (f t)) (x : E) : ∃ (α : C(↑(Set.Icc a b), E)), Function.IsFixedPt (picardStep t₀ hf x) α

theorem EulerPacketExistence.exists_solution_on_compact_interval {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (t₀ : ↑(Set.Icc a b)) {f : ℝ → E → E} (hf : Continuous (Function.uncurry f)) [NormedSpace ℝ E] [CompleteSpace E] {K : NNReal} (hLip : ∀ (t : ℝ), LipschitzWith K (f t)) (x : E) : ∃ (α : ℝ → E), α ↑t₀ = x ∧ ∀ t ∈ Set.Icc a b, HasDerivAt α (f t (α t)) t

A globally Lipschitz time-dependent vector field has a solution on every finite interval. Full derivatives also hold at the endpoints.

theorem EulerPacketExistence.exists_global_solution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {K : NNReal} (hf : Continuous (Function.uncurry f)) (hLip : ∀ (t : ℝ), LipschitzWith K (f t)) (x : E) : ∃ (u : ℝ → E), u 0 = x ∧ ∀ (t : ℝ), HasDerivAt u (f t (u t)) t

Global existence for a jointly continuous vector field with a uniform global Lipschitz constant in the state variable. Finite-interval solutions are glued using the proved ODE uniqueness theorem.

noncomputable def EulerPacketExistence.scalarCoefficientA (β t : ℝ) : ℝ

The displacement coefficient in the first-order form of equation (30).

Equations

• EulerPacketExistence.scalarCoefficientA β t = 2 * (1 - β * (β * t ^ 2)) / (1 + (β * t ^ 2) ^ 2)

noncomputable def EulerPacketExistence.scalarCoefficientB (β t : ℝ) : ℝ

The velocity coefficient in the first-order form of equation (30).

Equations

• EulerPacketExistence.scalarCoefficientB β t = -(4 * β ^ 2 * t ^ 3) / (1 + (β * t ^ 2) ^ 2)

noncomputable def EulerPacketExistence.scalarVectorField (β t : ℝ) (x : ℝ × ℝ) : ℝ × ℝ

The scalar equation as a globally Lipschitz two-dimensional system.

Equations

• EulerPacketExistence.scalarVectorField β t x = (x.2, EulerPacketExistence.scalarCoefficientA β t * x.1 + EulerPacketExistence.scalarCoefficientB β t * x.2)

theorem EulerPacketExistence.scalar_coefficient_bounds {β t : ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) : |scalarCoefficientA β t| ≤ 3 ∧ |scalarCoefficientB β t| ≤ 4

theorem EulerPacketExistence.continuous_scalarVectorField (β : ℝ) : Continuous (Function.uncurry (scalarVectorField β))

theorem EulerPacketExistence.lipschitz_scalarVectorField {β : ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) (t : ℝ) : LipschitzWith 7 (scalarVectorField β t)

theorem EulerPacketExistence.equation30_exists_global {β : ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) (v₀ v₁ : ℝ) : ∃ (V : ℝ → ℝ) (V₁ : ℝ → ℝ), V 0 = v₀ ∧ V₁ 0 = v₁ ∧ (∀ (t : ℝ), HasDerivAt V (V₁ t) t) ∧ ∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (β * s ^ 2) ^ 2) * V₁ s) (2 * (1 - β * (β * t ^ 2)) * V t) t

Global construction of equation (30) for arbitrary real initial data.

theorem EulerPacketExistence.equation30_exists_growing_primary {ε lam : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hlam : 0 ≤ lam) : ∃ (V : ℝ → ℝ) (V₁ : ℝ → ℝ), V 0 = 1 ∧ V₁ 0 = lam ∧ (∀ (t : ℝ), HasDerivAt V (V₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) ∧ Real.exp (1 / (4 * ε)) ≤ V (1 / ε) ∧ (∀ (t : ℝ), 0 ≤ t → 0 < V t) ∧ (∀ (t : ℝ), 1 ≤ t → |V₁ t / V t| ≤ 4) ∧ ∀ (y : ℝ), 0 < y → y ≤ 1 / 2 → have z := -ε * EulerPacketGrowth.invertedScalarDeriv ε V V₁ y / EulerPacketGrowth.invertedScalar ε V y; |z ^ 2 - 2 / (1 + y ^ 4)| ≤ 360 * ε

A constructed primary scalar solution has the exponential growth, positivity, and uniform logarithmic-slope properties used in the source. There is no solution-existence hypothesis in this statement.

theorem EulerPacketExistence.equation30_exists_fundamental_system {β : ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) : ∃ (F : ℝ → ℝ) (F₁ : ℝ → ℝ) (G : ℝ → ℝ) (G₁ : ℝ → ℝ), F 0 = 1 ∧ F₁ 0 = 0 ∧ G 0 = 0 ∧ G₁ 0 = 1 ∧ (∀ (t : ℝ), HasDerivAt F (F₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt G (G₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (β * s ^ 2) ^ 2) * F₁ s) (2 * (1 - β * (β * t ^ 2)) * F t) t) ∧ ∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (β * s ^ 2) ^ 2) * G₁ s) (2 * (1 - β * (β * t ^ 2)) * G t) t

Construction of the two exact fundamental solutions required by the relative propagator and Duhamel estimates.