Rel Loc Htpy Formal Sol exists sol
RelLoc.HtpyFormalSol.exists_sol
Plain-language statement
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.
Exact Lean statement
theorem RelLoc.HtpyFormalSol.exists_sol (𝓕₀ : R.HtpyFormalSol) (C : Set (ℝ × E)) (hC : IsClosed C)
(K : Set E) (hK : IsCompact K) (h_hol : ∀ᶠ p : ℝ × E near C, (𝓕₀ p.1).IsHolonomicAt p.2) :
∃ f : ℝ → E → F,
(𝒞 ∞ <| uncurry f) ∧
(∀ p ∈ C, f (p : ℝ × E).1 p.2 = (𝓕₀ p.1).f p.2) ∧
∀ x ∈ K, ∀ t ∈ I, (x, f t x, D (f t) x) ∈ RFormal artifact
Lean source
theorem RelLoc.HtpyFormalSol.exists_sol (𝓕₀ : R.HtpyFormalSol) (C : Set (ℝ × E)) (hC : IsClosed C) (K : Set E) (hK : IsCompact K) (h_hol : ∀ᶠ p : ℝ × E near C, (𝓕₀ p.1).IsHolonomicAt p.2) : ∃ f : ℝ → E → F, (𝒞 ∞ <| uncurry f) ∧ (∀ p ∈ C, f (p : ℝ × E).1 p.2 = (𝓕₀ p.1).f p.2) ∧ ∀ x ∈ K, ∀ t ∈ I, (x, f t x, D (f t) x) ∈ R := by obtain ⟨𝓕, _, h₂, -, h₄⟩ := 𝓕₀.improve_htpy h_op h_ample zero_lt_one C hC (I ×ˢ K) (isCompact_Icc.prod hK) h_hol refine ⟨fun s ↦ (𝓕 (1, s)).f, ?_, ?_, ?_⟩ · exact 𝓕.f_diff.comp ((contDiff_const.prodMk contDiff_id).prodMap contDiff_id) · intro p hp exact (Prod.ext_iff.mp ((h₂.forall_mem principal_le_nhdsSet) p hp 1)).1 · intro x hx t ht rw [show D (𝓕 (1, t)).f x = (𝓕 (1, t)).φ x from (h₄.forall_mem principal_le_nhdsSet) (t, x) (mk_mem_prod ht hx)] exact 𝓕.is_sol (1, t) x- Project
- Sphere eversion
- License
- Apache-2.0
- Commit
- ded8fda5e76b
- Source
- SphereEversion/Local/ParametricHPrinciple.lean:304-319
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Continuous of Path
Continuous.ofPath
Plain-language statement
Loop.ofPath is continuous, general version.
Source project: Sphere eversion
Person-level attribution pending.
Injective update iff
DualPair.injective_update_iff
Project documentation
Map a dual pair under a linear equivalence. -/ @[simps] def map (p : DualPair E) (L : E ≃L[ℝ] E') : DualPair E' := ⟨p.π ∘L ↑L.symm, L p.v, (congr_arg p.π <| L.symm_apply_apply p.v).trans p.pairing⟩ theorem update_comp_left (p : DualPair E) (ψ' : F →L[ℝ] G) (φ : E →L[ℝ] F) (w : F) : p.update (ψ' ∘L φ) (ψ' w) = ψ' ∘L p.update φ w := by ext1 u simp only [upd...
Source project: Sphere eversion
Person-level attribution pending.
Extend loops
extend_loops
Project documentation
A more precise version of sfHomotopy_in. -/ theorem sfHomotopy_in' {ι} (h₀ : SurroundingFamily g b γ₀ U) (h₁ : SurroundingFamily g b γ₁ U) (τ : ι → ℝ) (x : ι → E) (i : ι) {V : Set E} (hx : x i ∈ V) {t : ℝ} (ht : t ∈ I) {s : ℝ} (h_in₀ : ∀ i, x i ∈ V → ∀ t ∈ I, ∀ (s : ℝ), τ i ≠ 1 → (x i, γ₀ (x i) t s) ∈ Ω) (h_in₁ : ∀ i, x i ∈ V → ∀ t ∈ I, ∀ (s : ℝ), τ i ≠...
Source project: Sphere eversion
Person-level attribution pending.