theorem exist_loops_aux1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] {g b : E → F} {Ω : Set (E × F)} {K : Set E} [NormedSpace ℝ F] [FiniteDimensional ℝ F] (hK : IsCompact K) (hΩ_op : IsOpen Ω) (hb : 𝒞 (↑⊤) b) (hgK : ∀ᶠ (x : E) in nhdsSet K, g x = b x) (hconv : ∀ (x : E), g x ∈ hull (connectedComponentIn (Prod.mk x ⁻¹' Ω) (b x))) : ∃ (γ : E → ℝ → Loop F), ∃ V ∈ nhdsSet K, ∃ ε > 0, SurroundingFamilyIn g b γ V Ω ∧ (∀ x ∈ V, Metric.ball (x, b x) (ε + ε) ⊆ Ω) ∧ ∀ x ∈ V, ∀ (t s : ℝ), dist (↑(γ x t) s) (b x) < ε

theorem exist_loops_aux2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] {g b : E → F} {Ω : Set (E × F)} {K : Set E} [NormedSpace ℝ F] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : IsOpen Ω) (hg : 𝒞 (↑⊤) g) (hb : 𝒞 (↑⊤) b) (hgK : ∀ᶠ (x : E) in nhdsSet K, g x = b x) (hconv : ∀ (x : E), g x ∈ hull (connectedComponentIn (Prod.mk x ⁻¹' Ω) (b x))) : ∃ (γ : E → ℝ → Loop F), SurroundingFamilyIn g b γ Set.univ Ω ∧ 𝒞 ↑⊤ ↿γ ∧ ∀ᶠ (x : E) in nhdsSet K, ∀ (t s : ℝ), Metric.closedBall (x, b x) (dist (↑(γ x t) s) (b x)) ⊆ Ω

structure NiceLoop {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] (g b : E → F) (Ω : Set (E × F)) (K : Set E) [NormedSpace ℝ F] (γ : ℝ → E → Loop F) : Prop

A "nice" family of loops consists of all the properties we want from the exist_loops lemma: it is a smooth homotopy in Ω with fixed endpoints from the constant loop at b x to a loop with average g x that is also constantly b x near K. The first two conditions are implementation specific: the homotopy is constant outside the unit interval.

• t_le_zero (x : E) (t : ℝ) : t ≤ 0 → γ t x = γ 0 x
• t_ge_one (x : E) (t : ℝ) : t ≥ 1 → γ t x = γ 1 x
• t_zero (x : E) (s : ℝ) : ↑(γ 0 x) s = b x
• s_zero (x : E) (t : ℝ) : ↑(γ t x) 0 = b x
• avg (x : E) : (γ 1 x).average = g x
• mem_Ω (x : E) (t s : ℝ) : (x, ↑(γ t x) s) ∈ Ω
• smooth : 𝒞 ↑⊤ ↿γ
• rel_K : ∀ᶠ (x : E) in nhdsSet K, ∀ (t s : ℝ), ↑(γ t x) s = b x

theorem exist_loops {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] {g b : E → F} {Ω : Set (E × F)} {K : Set E} [NormedSpace ℝ F] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : IsOpen Ω) (hg : 𝒞 (↑⊤) g) (hb : 𝒞 (↑⊤) b) (hgK : ∀ᶠ (x : E) in nhdsSet K, g x = b x) (hconv : ∀ (x : E), g x ∈ hull (connectedComponentIn (Prod.mk x ⁻¹' Ω) (b x))) : ∃ (γ : ℝ → E → Loop F), NiceLoop g b Ω K γ