Picard-Lindelöf with explicit confinement conjunct (vendored from Mathlib)

This file is vendored from Mathlib/Analysis/ODE/PicardLindelof.lean (Yury Kudryashov, Winston Yin): it copies two upstream theorems and adds one conjunct to each public conclusion; the proofs are otherwise the upstream proofs. The two upstream sources were IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith and IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt (present in Mathlib/Analysis/ODE/PicardLindelof.lean through mathlib v4.29.1; the local-flow refactor later moved these public wrappers to Mathlib/Analysis/ODE/ExistUnique.lean, which this file does not import, while keeping the FunSpace machinery this file's proofs actually use — exists_isFixedPt_next, compProj_*, hasDerivWithinAt_picard_Icc, exists_forall_closedBall_funSpace_dist_le_mul — in place, so the proofs below still elaborate against current mathlib unchanged). The single difference from each original is marked inline below with a Vendored addition comment.

The new conjunct exposes FunSpace.compProj_mem_closedBall's guarantee at the public theorem level: every flow trajectory α x t stays inside closedBall x₀ a (the outer ball where the field is Lipschitz). The underlying property is already proved upstream in Mathlib; in fact, the upstream public proof of exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith (now in Mathlib/Analysis/ODE/ExistUnique.lean) already invokes compProj_mem_closedBall hf.mul_max_le internally (to constrain the iterate to the Lipschitz region). We are only re-exporting that invariant through the public conclusion.

Intended upstreaming: this file is structured as a near-mechanical patch to Mathlib/Analysis/ODE/PicardLindelof.lean; the eventual Mathlib PR would drop the _confined suffix and replace the two original theorems with their strengthened forms (no API breaks for downstream consumers, since the conclusion only grows).

In-project consumer: Vlasov.OT.CharacteristicFlow (where exists_vlasov_extend_one_window threads the confinement conjunct through to Helper 1, vlasov_window_confinement).

theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith_confined {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (α : E → ℝ → E), (∀ x ∈ Metric.closedBall x₀ ↑r, α x ↑t₀ = x ∧ (∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t) ∧ ∀ t ∈ Set.Icc tmin tmax, α x t ∈ Metric.closedBall x₀ ↑a) ∧ ∃ (L' : NNReal), ∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith L' (fun (x : E) => α x t) (Metric.closedBall x₀ ↑r)

Picard-Lindelöf with confinement (vendored from Mathlib, awaiting upstream PR). Same conclusion as exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith plus an additional conjunct ∀ t ∈ Icc tmin tmax, α x t ∈ closedBall x₀ a — exposing the FunSpace confinement guarantee at the public API level. The underlying property is already proved upstream (the existing proof of _lipschitzOnWith invokes FunSpace.compProj_mem_closedBall hf.mul_max_le internally to constrain the iterate to the Lipschitz region); we only re-export it.

theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt_confined {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (α : E → ℝ → E), ∀ x ∈ Metric.closedBall x₀ ↑r, α x ↑t₀ = x ∧ (∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t) ∧ ∀ t ∈ Set.Icc tmin tmax, α x t ∈ Metric.closedBall x₀ ↑a

Picard-Lindelöf with confinement, thin wrapper (vendored). Drops the Lipschitz-in-initial-point conjunct from _lipschitzOnWith_confined. This is the form exists_vlasov_extend_one_window consumes — Vlasov doesn't need the flow's Lipschitz dependence on the initial point.