theorem
OpenSmoothEmbedding.improve_formalSol
{EM : Type u_1}
[NormedAddCommGroup EM]
[NormedSpace ℝ EM]
[FiniteDimensional ℝ EM]
{HM : Type u_2}
[TopologicalSpace HM]
{IM : ModelWithCorners ℝ EM HM}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace HM M]
[IsManifold IM (↑⊤) M]
[T2Space M]
{EX : Type u_4}
[NormedAddCommGroup EX]
[NormedSpace ℝ EX]
[FiniteDimensional ℝ EX]
{HX : Type u_5}
[TopologicalSpace HX]
{IX : ModelWithCorners ℝ EX HX}
{X : Type u_6}
[MetricSpace X]
[ChartedSpace HX X]
[IsManifold IX (↑⊤) X]
(φ : OpenSmoothEmbedding (modelWithCornersSelf ℝ EM) EM IM M)
(ψ : OpenSmoothEmbedding (modelWithCornersSelf ℝ EX) EX IX X)
{R : RelMfld IM M IX X}
(hRample : R.Ample)
(hRopen : IsOpen R)
{C : Set M}
(hC : IsClosed C)
{δ : M → ℝ}
(hδ_pos : ∀ (x : M), 0 < δ x)
(hδ_cont : Continuous δ)
{F : FormalSol R}
(hFφψ : F.bs '' Set.range ↑φ ⊆ Set.range ↑ψ)
(hFC : ∀ᶠ (x : M) in nhdsSet C, F.IsHolonomicAt x)
{K₀ K₁ : Set EM}
(hK₀ : IsCompact K₀)
(hK₁ : IsCompact K₁)
(hK₀K₁ : K₀ ⊆ interior K₁)
:
∃ (F' : HtpyFormalSol R),
(∀ᶠ (t : ℝ) in nhdsSet (Set.Iic 0), F' t = F) ∧ (∀ᶠ (t : ℝ) in nhdsSet (Set.Ici 1), F' t = F' 1) ∧ (∀ᶠ (x : M) in nhdsSet C, ∀ (t : ℝ), (F' t) x = F x) ∧ (∀ (t : ℝ), ∀ x ∉ ↑φ '' K₁, (F' t) x = F x) ∧ (∀ (t : ℝ) (x : M), dist ((F' t).bs x) (F.bs x) < δ x) ∧ ∀ᶠ (x : M) in nhdsSet (C ∪ ↑φ '' K₀), (F' 1).IsHolonomicAt x