In this file we prove the parametric version of the local h-principle.

We will not use this to prove the global version of the h-principle, but we do use this to conclude the existence of sphere eversion from the local h-principle, which is proven in Local.HPrinciple.

The parametric h-principle states the following: Suppose that R is a local relation, 𝓕₀ : P → J¹(E, F) is a family of formal solutions of R that is holonomic near some set C ⊆ P × E, K ⊆ P × E is compact and ε : ℝ, then there exists a homotopy 𝓕 : ℝ × P → J¹(E, F) between 𝓕 and a solution that is holonomic near K, that agrees with 𝓕₀ near C and is everywhere ε-close to 𝓕₀

noncomputable def oneJetSnd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] : OneJet (P × E) F → OneJet E F

The projection J¹(P × E, F) → J¹(E, F).

Equations

• oneJetSnd p = (p.1.2, p.2.1, p.2.2 ∘SL D (fun (y : E) => (p.1.1, y)) p.1.2)

theorem continuous_oneJetSnd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] : Continuous oneJetSnd

theorem oneJetSnd_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (p : OneJet (P × E) F) : oneJetSnd p = (p.1.2, p.2.1, p.2.2 ∘SL ContinuousLinearMap.inr ℝ P E)

def RelLoc.relativize {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (P : Type u_4) [NormedAddCommGroup P] [NormedSpace ℝ P] (R : RelLoc E F) : RelLoc (P × E) F

The relation R.relativize P (𝓡 ^ P in the blueprint) is the relation on J¹(P × E, F) induced by R.

Equations

• RelLoc.relativize P R = oneJetSnd ⁻¹' R

theorem RelLoc.mem_relativize {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (R : RelLoc E F) (w : OneJet (P × E) F) : w ∈ relativize P R ↔ (w.1.2, w.2.1, w.2.2 ∘SL ContinuousLinearMap.inr ℝ P E) ∈ R

theorem RelLoc.isOpen_relativize {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (R : RelLoc E F) (h2 : IsOpen R) : IsOpen (relativize P R)

theorem relativize_slice_loc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} {σ : OneJet (P × E) F} {p : DualPair (P × E)} (q : DualPair E) (hpq : p.π ∘SL ContinuousLinearMap.inr ℝ P E = q.π) : (RelLoc.relativize P R).slice p σ = σ.2.2 (p.v - (0, q.v)) +ᵥ R.slice q (oneJetSnd σ)

theorem relativize_slice_eq_univ_loc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} {σ : OneJet (P × E) F} {p : DualPair (P × E)} (hp : p.π ∘SL ContinuousLinearMap.inr ℝ P E = 0) : ((RelLoc.relativize P R).slice p σ).Nonempty ↔ (RelLoc.relativize P R).slice p σ = Set.univ

theorem RelLoc.IsAmple.relativize {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (P : Type u_4) [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} (hR : R.IsAmple) : (RelLoc.relativize P R).IsAmple

noncomputable def FamilyJetSec.uncurry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec E F P) : JetSec (P × E) F

Turn a family of sections of J¹(E, E') parametrized by P into a section of J¹(P × E, E').

Equations

• S.uncurry = { f := fun (p : P × E) => S.f p.1 p.2, f_diff := ⋯, φ := fun (p : P × E) => D (fun (z : P × E) => S.f z.1 p.2) p + S.φ p.1 p.2 ∘SL D Prod.snd p, φ_diff := ⋯ }

@[simp]

theorem FamilyJetSec.uncurry_φ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec E F P) (p : P × E) : S.uncurry.φ p = D (fun (z : P × E) => S.f z.1 p.2) p + S.φ p.1 p.2 ∘SL D Prod.snd p

@[simp]

theorem FamilyJetSec.uncurry_f {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec E F P) (p : P × E) : S.uncurry.f p = S.f p.1 p.2

theorem FamilyJetSec.uncurry_φ' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec E F P) (p : P × E) : S.uncurry.φ p = D (fun (z : P) => S.f z p.2) p.1 ∘SL ContinuousLinearMap.fst ℝ P E + S.φ p.1 p.2 ∘SL ContinuousLinearMap.snd ℝ P E

theorem FamilyJetSec.uncurry_mem_relativize {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} (S : FamilyJetSec E F P) {s : P} {x : E} : ((s, x), S.uncurry (s, x)) ∈ RelLoc.relativize P R ↔ (x, (S s) x) ∈ R

theorem FamilyJetSec.isHolonomicAt_uncurry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec E F P) {p : P × E} : S.uncurry.IsHolonomicAt p ↔ (S p.1).IsHolonomicAt p.2

noncomputable def RelLoc.FamilyFormalSol.uncurry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} (S : FamilyFormalSol P R) : (relativize P R).FormalSol

Turn a family of formal solutions of R ⊆ J¹(E, E') parametrized by P into a formal solution of R.relativize P.

Equations

• S.uncurry = { toJetSec := S.uncurry, is_sol := ⋯ }

theorem RelLoc.FamilyFormalSol.uncurry_φ' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} (S : FamilyFormalSol P R) (p : P × E) : (S.uncurry p).2 = D (fun (z : P) => S.f z p.2) p.1 ∘SL ContinuousLinearMap.fst ℝ P E + S.φ p.1 p.2 ∘SL ContinuousLinearMap.snd ℝ P E

noncomputable def FamilyJetSec.curry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec (P × E) F G) : FamilyJetSec E F (G × P)

Turn a family of sections of J¹(P × E, F) parametrized by G into a family of sections of J¹(E, F) parametrized by G × P.

Equations

• S.curry = { f := fun (p : G × P) (x : E) => (S p.1).f (p.2, x), f_diff := ⋯, φ := fun (p : G × P) (x : E) => (S p.1).φ (p.2, x) ∘SL D (fun (x : E) => (p.2, x)) x, φ_diff := ⋯ }

theorem FamilyJetSec.curry_f {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec (P × E) F G) (p : G × P) (x : E) : (S.curry p).f x = (S p.1).f (p.2, x)

theorem FamilyJetSec.curry_φ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec (P × E) F G) (p : G × P) (x : E) : (S.curry p).φ x = (S p.1).φ (p.2, x) ∘SL D (fun (x : E) => (p.2, x)) x

theorem FamilyJetSec.curry_φ' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec (P × E) F G) (p : G × P) (x : E) : (S.curry p).φ x = (S p.1).φ (p.2, x) ∘SL ContinuousLinearMap.inr ℝ P E

theorem FamilyJetSec.isHolonomicAt_curry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (S : FamilyJetSec (P × E) F G) {t : G} {s : P} {x : E} (hS : (S t).IsHolonomicAt (s, x)) : (S.curry (t, s)).IsHolonomicAt x

theorem FamilyJetSec.curry_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} (S : FamilyJetSec (P × E) F G) {p : G × P} {x : E} (hR : ((p.2, x), (S p.1) (p.2, x)) ∈ RelLoc.relativize P R) : (x, (S.curry p) x) ∈ R

noncomputable def RelLoc.FamilyFormalSol.curry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} (S : FamilyFormalSol G (relativize P R)) : FamilyFormalSol (G × P) R

Turn a family of formal solutions of R.relativize P parametrized by G into a family of formal solutions of R parametrized by G × P.

Equations

• S.curry = { toFamilyJetSec := S.curry, is_sol := ⋯ }

theorem RelLoc.FamilyFormalSol.curry_φ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} (S : FamilyFormalSol G (relativize P R)) (p : G × P) (x : E) : (S.curry p).φ x = (S p.1).φ (p.2, x) ∘SL D (fun (x : E) => (p.2, x)) x

theorem RelLoc.FamilyFormalSol.curry_φ' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} (S : FamilyFormalSol G (relativize P R)) (p : G × P) (x : E) : ((S.curry p) x).2 = ((S p.1) (p.2, x)).2 ∘SL ContinuousLinearMap.inr ℝ P E

theorem curry_eq_iff_eq_uncurry_loc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] {R : RelLoc E F} {𝓕 : RelLoc.FamilyFormalSol G (RelLoc.relativize P R)} {𝓕₀ : RelLoc.FamilyFormalSol P R} {t : G} {x : E} {s : P} (h : (𝓕 t) (s, x) = 𝓕₀.uncurry (s, x)) : (𝓕.curry (t, s)) x = (𝓕₀ s) x

theorem RelLoc.FamilyFormalSol.improve_htpy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [FiniteDimensional ℝ P] {R : RelLoc E F} (h_op : IsOpen R) (h_ample : R.IsAmple) {ε : ℝ} (ε_pos : 0 < ε) (C : Set (P × E)) (hC : IsClosed C) (K : Set (P × E)) (hK : IsCompact K) (𝓕₀ : FamilyFormalSol P R) (h_hol : ∀ᶠ (p : P × E) in nhdsSet C, (𝓕₀ p.1).IsHolonomicAt p.2) : ∃ (𝓕 : FamilyFormalSol (ℝ × P) R), (∀ (s : P) (x : E), (𝓕 (0, s)) x = (𝓕₀ s) x) ∧ (∀ᶠ (p : P × E) in nhdsSet C, ∀ (t : ℝ), (𝓕 (t, p.1)) p.2 = (𝓕₀ p.1) p.2) ∧ (∀ (s : P) (x : E) (t : ℝ), ‖(𝓕 (t, s)).f x - 𝓕₀.f s x‖ ≤ ε) ∧ ∀ᶠ (p : P × E) in nhdsSet K, (𝓕 (1, p.1)).IsHolonomicAt p.2

theorem RelLoc.HtpyFormalSol.exists_sol {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {R : RelLoc E F} (h_op : IsOpen R) (h_ample : R.IsAmple) (𝓕₀ : R.HtpyFormalSol) (C : Set (ℝ × E)) (hC : IsClosed C) (K : Set E) (hK : IsCompact K) (h_hol : ∀ᶠ (p : ℝ × E) in nhdsSet C, (𝓕₀ p.1).IsHolonomicAt p.2) : ∃ (f : ℝ → E → F), 𝒞 (↑⊤) (Function.uncurry f) ∧ (∀ p ∈ C, f p.1 p.2 = (𝓕₀ p.1).f p.2) ∧ ∀ x ∈ K, ∀ t ∈ unitInterval, (x, f t x, D (f t) x) ∈ R

A corollary of the local parametric h-principle, forgetting the homotopy and ε-closeness, and just stating the existence of a solution that is holonomic near K. Furthermore, we assume that P = ℝ and K is of the form compact set × I. This is sufficient to prove sphere eversion.