Surrounding families of loops #

In order to carry out the corrugation technique of convex integration, one needs to a family of loops with various prescribed properties.

This file begins the work of constructing such a family.

The key definitions are:

The key results are:

source

noncomputable def IsPathConnected.somePath {X : Type u_1} [TopologicalSpace X] {F : Set X} (hF : IsPathConnected F) {x y : X} (hx : x ∈ F) (hy : y ∈ F) :

Path x y

An arbitrary path joining x and y in F.

Equations

hF.somePath hx hy = ⋯.somePath

Instances For

source

theorem IsPathConnected.somePath_mem {X : Type u_1} [TopologicalSpace X] {F : Set X} (hF : IsPathConnected F) {x y : X} (hx : x ∈ F) (hy : y ∈ F) (t : ↑unitInterval) :

(hF.somePath hx hy) t ∈ F

source

theorem IsPathConnected.range_somePath_subset {X : Type u_1} [TopologicalSpace X] {F : Set X} (hF : IsPathConnected F) {x y : X} (hx : x ∈ F) (hy : y ∈ F) :

Set.range ⇑(hF.somePath hx hy) ⊆ F

source

noncomputable def IsPathConnected.pathThrough {X : Type u_1} [TopologicalSpace X] {F : Set X} (hF : IsPathConnected F) {m : ℕ} {p : Fin (m + 1) → X} (hp : ∀ (i : Fin (m + 1)), p i ∈ F) (n : ℕ) :

Path (p 0) (p ↑n)

A path through p 0, ..., p n. Usually this is used with n := m.

Equations

hF.pathThrough hp 0 = Path.refl (p 0)
hF.pathThrough hp n.succ = (hF.pathThrough hp n).trans (hF.somePath ⋯ ⋯)

Instances For

source

theorem IsPathConnected.range_pathThrough_subset {X : Type u_1} [TopologicalSpace X] {F : Set X} (hF : IsPathConnected F) {m : ℕ} {p : Fin (m + 1) → X} (hp : ∀ (i : Fin (m + 1)), p i ∈ F) {n : ℕ} :

Set.range ⇑(hF.pathThrough hp n) ⊆ F

source

theorem IsPathConnected.mem_range_pathThrough' {X : Type u_1} [TopologicalSpace X] {F : Set X} (hF : IsPathConnected F) {m : ℕ} {p : Fin (m + 1) → X} (hp : ∀ (i : Fin (m + 1)), p i ∈ F) {i n : ℕ} (h : i ≤ n) :

p ↑i ∈ Set.range ⇑(hF.pathThrough hp n)

source

theorem IsPathConnected.mem_range_pathThrough {X : Type u_1} [TopologicalSpace X] {F : Set X} (hF : IsPathConnected F) {m : ℕ} {p : Fin (m + 1) → X} (hp : ∀ (i : Fin (m + 1)), p i ∈ F) {i : Fin (m + 1)} :

p i ∈ Set.range ⇑(hF.pathThrough hp m)

source

def SmoothAt' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (x : E) :

Prop

f is smooth at x if f is smooth on some neighborhood of x.

Equations

SmoothAt' f x = ∃ s ∈ nhds x, ContDiffOn ℝ (↑⊤) f s

Instances For

source

structure SurroundingPts {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : F) (p : Fin (Module.finrank ℝ F + 1) → F) (w : Fin (Module.finrank ℝ F + 1) → ℝ) :

Prop

p is a collection of points surrounding f with weights w (that are positive and sum to 1) if the weighted average of the points p is f and the points p form an affine basis of the space.

indep : AffineIndependent ℝ p
w_pos (i : Fin (Module.finrank ℝ F + 1)) : 0 < w i
w_sum : ∑ i : Fin (Module.finrank ℝ F + 1), w i = 1
avg : ∑ i : Fin (Module.finrank ℝ F + 1), w i • p i = f

Instances For

source

theorem SurroundingPts.tot {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : F} {p : Fin (Module.finrank ℝ F + 1) → F} {w : Fin (Module.finrank ℝ F + 1) → ℝ} (h : SurroundingPts f p w) :

affineSpan ℝ (Set.range p) = ⊤

source

theorem SurroundingPts.mem_affineBases {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : F} {p : Fin (Module.finrank ℝ F + 1) → F} {w : Fin (Module.finrank ℝ F + 1) → ℝ} (h : SurroundingPts f p w) :

p ∈ affineBases (Fin (Module.finrank ℝ F + 1)) ℝ F

source

theorem SurroundingPts.coord_eq_w {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : F} {p : Fin (Module.finrank ℝ F + 1) → F} {w : Fin (Module.finrank ℝ F + 1) → ℝ} (h : SurroundingPts f p w) :

{ toFun := p, ind' := ⋯, tot' := ⋯ }.coords f = w

source

def Surrounded {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : F) (s : Set F) :

Prop

f is surrounded by a set s if there is an affine basis p in s with weighted average f.

Equations

Surrounded f s = ∃ (p : Fin (Module.finrank ℝ F + 1) → F) (w : Fin (Module.finrank ℝ F + 1) → ℝ), SurroundingPts f p w ∧ ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ s

Instances For

source

theorem surrounded_iff_mem_interior_convexHull_aff_basis {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : F} {s : Set F} :

Surrounded f s ↔ ∃ b ⊆ s, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ b = ⊤ ∧ f ∈ interior (hull b)

source

theorem surrounded_of_convexHull {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : F} {s : Set F} (hs : IsOpen s) (hsf : f ∈ hull s) :

Surrounded f s

source

theorem smooth_surrounding {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {x : F} {p : Fin (Module.finrank ℝ F + 1) → F} {w : Fin (Module.finrank ℝ F + 1) → ℝ} (h : SurroundingPts x p w) :

∃ (W : F → (Fin (Module.finrank ℝ F + 1) → F) → Fin (Module.finrank ℝ F + 1) → ℝ), ∀ᶠ (yq : F × (Fin (Module.finrank ℝ F + 1) → F)) in nhds (x, p), SmoothAt' (Function.uncurry W) yq ∧ (∀ (i : Fin (Module.finrank ℝ F + 1)), 0 < W yq.1 yq.2 i) ∧ ∑ i : Fin (Module.finrank ℝ F + 1), W yq.1 yq.2 i = 1 ∧ ∑ i : Fin (Module.finrank ℝ F + 1), W yq.1 yq.2 i • yq.2 i = yq.1

source

theorem smooth_surroundingPts {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {x : F} {p : Fin (Module.finrank ℝ F + 1) → F} {w : Fin (Module.finrank ℝ F + 1) → ℝ} (h : SurroundingPts x p w) :

∃ (W : F → (Fin (Module.finrank ℝ F + 1) → F) → Fin (Module.finrank ℝ F + 1) → ℝ), ∀ᶠ (yq : F × (Fin (Module.finrank ℝ F + 1) → F)) in nhds (x, p), SmoothAt' (Function.uncurry W) yq ∧ SurroundingPts yq.1 yq.2 (W yq.1 yq.2)

source

theorem surroundingPts_evalBarycentricCoords_iff {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (q : F) (v : Fin (Module.finrank ℝ F + 1) → F) [DecidablePred fun (x : Fin (Module.finrank ℝ F + 1) → F) => x ∈ affineBases (Fin (Module.finrank ℝ F + 1)) ℝ F] :

SurroundingPts q v (evalBarycentricCoords (Fin (Module.finrank ℝ F + 1)) ℝ F q v) ↔ ∀ (i : Fin (Module.finrank ℝ F + 1)), 0 < evalBarycentricCoords (Fin (Module.finrank ℝ F + 1)) ℝ F q v i

source

theorem eventually_surroundingPts_of_tendsto_of_tendsto {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {X : Type u_3} {Y : Type u_4} [FiniteDimensional ℝ F] {l : Filter X} {m : Filter Y} {v : Fin (Module.finrank ℝ F + 1) → F} {q : F} {p : Fin (Module.finrank ℝ F + 1) → X → F} {f : Y → F} (hq : ∃ (w : Fin (Module.finrank ℝ F + 1) → ℝ), SurroundingPts q v w) (hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), Filter.Tendsto (p i) l (nhds (v i))) (hf : Filter.Tendsto f m (nhds q)) :

∀ᶠ (z : X × Y) in l ×ˢ m, ∃ (w : Fin (Module.finrank ℝ F + 1) → ℝ), SurroundingPts (f z.2) (fun (i : Fin (Module.finrank ℝ F + 1)) => p i z.1) w

source

theorem eventually_surroundingPts_of_tendsto_of_tendsto' {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {X : Type u_3} [FiniteDimensional ℝ F] {v : Fin (Module.finrank ℝ F + 1) → F} {q : F} {p : Fin (Module.finrank ℝ F + 1) → X → F} {l : Filter X} {f : X → F} (hq : ∃ (w : Fin (Module.finrank ℝ F + 1) → ℝ), SurroundingPts q v w) (hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), Filter.Tendsto (p i) l (nhds (v i))) (hf : Filter.Tendsto f l (nhds q)) :

∀ᶠ (y : X) in l, ∃ (w : Fin (Module.finrank ℝ F + 1) → ℝ), SurroundingPts (f y) (fun (i : Fin (Module.finrank ℝ F + 1)) => p i y) w

source

def Loop.Surrounds {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (γ : Loop F) (x : F) :

Prop

A loop γ surrounds a point x if x is surrounded by values of γ.

Equations

γ.Surrounds x = ∃ (t : Fin (Module.finrank ℝ F + 1) → ℝ) (w : Fin (Module.finrank ℝ F + 1) → ℝ), SurroundingPts x (↑γ ∘ t) w

Instances For

source

theorem Loop.surrounds_iff_range_subset_range {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : Loop F} {x : F} :

γ.Surrounds x ↔ ∃ (p : Fin (Module.finrank ℝ F + 1) → F) (w : Fin (Module.finrank ℝ F + 1) → ℝ), SurroundingPts x p w ∧ Set.range p ⊆ Set.range ↑γ

source

theorem Loop.affineEquiv_surrounds_iff {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : Loop F} {x : F} (e : F ≃ᵃ[ℝ ] F) :

γ.Surrounds x ↔ (γ.transform ⇑e).Surrounds (e x)

source

@[simp]

theorem Loop.zero_vadd {F : Type u_2} [NormedAddCommGroup F] {γ : Loop F} :

0 +ᵥ γ = γ

source

theorem Loop.vadd_surrounds {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : Loop F} {x y : F} :

γ.Surrounds x ↔ (y +ᵥ γ).Surrounds (y + x)

source

theorem Loop.Surrounds.vadd {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : Loop F} {x y : F} (h : γ.Surrounds x) :

(y +ᵥ γ).Surrounds (y + x)

source

theorem Loop.Surrounds.vadd0 {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : Loop F} {y : F} (h : γ.Surrounds 0) :

(y +ᵥ γ).Surrounds y

source

theorem Loop.Surrounds.smul0 {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : Loop F} {t : ℝ} (h : γ.Surrounds 0) (ht : t ≠ 0) :

(t • γ).Surrounds 0

source

theorem Loop.Surrounds.mono {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ γ' : Loop F} {x : F} (h : γ.Surrounds x) (h2 : Set.range ↑γ ⊆ Set.range ↑γ') :

γ'.Surrounds x

source

theorem Loop.Surrounds.reparam {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : Loop F} {x : F} (h : γ.Surrounds x) {φ : EquivariantMap} (hφ : Continuous φ.toFun) :

(γ.reparam φ).Surrounds x

source

theorem Loop.Surrounds.eventually_surrounds {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : Loop F} {x : F} [FiniteDimensional ℝ F] (h : γ.Surrounds x) :

∃ ε > 0, ∀ (γ' : Loop F) (y : F), (∀ (z : ℝ), dist (↑γ' z) (↑γ z) < ε) → dist y x < ε → γ'.Surrounds y

This is only a stepping stone potentially useful for SurroundingFamily.surrounds_of_close, but not needed by itself.

source

def surroundingLoop {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {O : Set F} {b : F} {p : Fin (Module.finrank ℝ F + 1) → F} (O_conn : IsPathConnected O) (hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ O) (hb : b ∈ O) :

ℝ → Loop F

witness of surrounding_loop_of_convexHull

Equations

surroundingLoop O_conn hp hb = Loop.roundTripFamily ((O_conn.somePath hb ⋯).trans (O_conn.pathThrough hp (Module.finrank ℝ F)))

Instances For

source

theorem continuous_surroundingLoop {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {O : Set F} {b : F} {p : Fin (Module.finrank ℝ F + 1) → F} {O_conn : IsPathConnected O} {hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ O} {hb : b ∈ O} :

Continuous ↿(surroundingLoop O_conn hp hb)

TODO: continuity note

source

@[simp]

theorem surroundingLoop_zero_right {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {O : Set F} {b : F} {p : Fin (Module.finrank ℝ F + 1) → F} {O_conn : IsPathConnected O} {hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ O} {hb : b ∈ O} (t : ℝ) :

↑(surroundingLoop O_conn hp hb t) 0 = b

source

@[simp]

theorem surroundingLoop_zero_left {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {O : Set F} {b : F} {p : Fin (Module.finrank ℝ F + 1) → F} {O_conn : IsPathConnected O} {hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ O} {hb : b ∈ O} (s : ℝ) :

↑(surroundingLoop O_conn hp hb 0) s = b

source

theorem surroundingLoop_mem {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {O : Set F} {b : F} {p : Fin (Module.finrank ℝ F + 1) → F} {O_conn : IsPathConnected O} {hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ O} {hb : b ∈ O} (t s : ℝ) :

↑(surroundingLoop O_conn hp hb t) s ∈ O

source

theorem surroundingLoop_surrounds {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {O : Set F} {b : F} {p : Fin (Module.finrank ℝ F + 1) → F} {O_conn : IsPathConnected O} {hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ O} {hb : b ∈ O} {f : F} {w : Fin (Module.finrank ℝ F + 1) → ℝ} (h : SurroundingPts f p w) :

(surroundingLoop O_conn hp hb 1).Surrounds f

source

theorem surroundingLoop_projI {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {O : Set F} {b : F} {p : Fin (Module.finrank ℝ F + 1) → F} {O_conn : IsPathConnected O} {hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ O} {hb : b ∈ O} (t : ℝ) :

surroundingLoop O_conn hp hb (projI t) = surroundingLoop O_conn hp hb t

source

theorem surroundingLoop_of_le_zero {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {O : Set F} {b : F} {p : Fin (Module.finrank ℝ F + 1) → F} {O_conn : IsPathConnected O} {hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ O} {hb : b ∈ O} (s : ℝ) {t : ℝ} (ht : t ≤ 0) :

↑(surroundingLoop O_conn hp hb t) s = b

source

theorem surroundingLoop_of_ge_one {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {O : Set F} {b : F} {p : Fin (Module.finrank ℝ F + 1) → F} {O_conn : IsPathConnected O} {hp : ∀ (i : Fin (Module.finrank ℝ F + 1)), p i ∈ O} {hb : b ∈ O} (s : ℝ) {t : ℝ} (ht : 1 ≤ t) :

↑(surroundingLoop O_conn hp hb t) s = ↑(surroundingLoop O_conn hp hb 1) s

source

theorem surrounding_loop_of_convexHull {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f b : F} {O : Set F} (O_op : IsOpen O) (O_conn : IsConnected O) (hsf : f ∈ hull O) (hb : b ∈ O) :

∃ (γ : ℝ → Loop F), Continuous ↿γ ∧ (∀ (t : ℝ), ↑(γ t) 0 = b) ∧ (∀ (s : ℝ), ↑(γ 0) s = b) ∧ (∀ (s t : ℝ), ↑(γ (projI t)) s = ↑(γ t) s) ∧ (∀ (t s : ℝ), ↑(γ t) s ∈ O) ∧ (γ 1).Surrounds f

source

structure SurroundingFamily {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (g b : E → F) (γ : E → ℝ → Loop F) (U : Set E) :

Prop

γ forms a family of loops surrounding g with base b. In contrast to the notes we assume that base and t₀ hold universally.

base (x : E) (t : ℝ) : ↑(γ x t) 0 = b x
t₀ (x : E) (s : ℝ) : ↑(γ x 0) s = b x
projI (x : E) (t s : ℝ) : ↑(γ x (projI t)) s = ↑(γ x t) s
surrounds (x : E) : x ∈ U → (γ x 1).Surrounds (g x)
cont : Continuous ↿γ

Instances For

source

structure SurroundingFamilyIn {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (g b : E → F) (γ : E → ℝ → Loop F) (U : Set E) (Ω : Set (E × F)) extends SurroundingFamily g b γ U :

Prop

γ forms a family of loops surrounding g with base b in Ω.

base (x : E) (t : ℝ) : ↑(γ x t) 0 = b x
t₀ (x : E) (s : ℝ) : ↑(γ x 0) s = b x
projI (x : E) (t s : ℝ) : ↑(γ x (projI t)) s = ↑(γ x t) s
surrounds (x : E) : x ∈ U → (γ x 1).Surrounds (g x)
cont : Continuous ↿γ
val_in' (x : E) : x ∈ U → ∀ t ∈ unitInterval, ∀ s ∈ unitInterval, (x, ↑(γ x t) s) ∈ Ω

Instances For

source

theorem SurroundingFamily.one {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) (x : E) (t : ℝ) :

↑(γ x t) 1 = b x

source

theorem SurroundingFamily.t_le_zero {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) (x : E) (s : ℝ) {t : ℝ} (ht : t ≤ 0) :

↑(γ x t) s = ↑(γ x 0) s

source

theorem SurroundingFamily.t_le_zero_eq_b {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) (x : E) (s : ℝ) {t : ℝ} (ht : t ≤ 0) :

↑(γ x t) s = b x

source

theorem SurroundingFamily.t_ge_one {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) (x : E) (s : ℝ) {t : ℝ} (ht : 1 ≤ t) :

↑(γ x t) s = ↑(γ x 1) s

source

theorem SurroundingFamily.mono {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) {V : Set E} (hVU : V ⊆ U) :

SurroundingFamily g b γ V

source

theorem SurroundingFamily.surrounds_of_close_univ {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} [NormedSpace ℝ E] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (hg : Continuous g) (h : SurroundingFamily g b γ Set.univ) :

∃ (ε : E → ℝ), (∀ (x : E), 0 < ε x) ∧ Continuous ε ∧ ∀ (x : E) (γ' : Loop F), (∀ (z : ℝ), dist (↑γ' z) (↑(γ x 1) z) < ε x) → γ'.Surrounds (g x)

source

def SurroundingFamily.path {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) (x : E) (t : ℝ) :

Path (b x) (b x)

A surrounding family induces a family of paths from b x to b x. We defined the concatenation we need on path, so we need to turn a surrounding family into the family of paths.

Equations

h.path x t = { toFun := fun (s : ↑unitInterval) => ↑(γ x t) ↑s, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

Instances For

source

@[simp]

theorem SurroundingFamily.path_apply {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) (x : E) (t : ℝ) (s : ↑unitInterval) :

(h.path x t) s = ↑(γ x t) ↑s

source

theorem SurroundingFamily.continuous_path {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} {X : Type u_3} [TopologicalSpace X] (h : SurroundingFamily g b γ U) {t : X → ℝ} {f : X → E} {s : X → ↑unitInterval} (hf : Continuous f) (ht : Continuous t) (hs : Continuous s) :

Continuous fun (x : X) => (h.path (f x) (t x)) (s x)

source

@[simp]

theorem SurroundingFamily.path_extend_fract {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) (t s : ℝ) (x : E) :

(h.path x t).extend (Int.fract s) = ↑(γ x t) s

source

@[simp]

theorem SurroundingFamily.range_path {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) (x : E) (t : ℝ) :

Set.range ⇑(h.path x t) = Set.range ↑(γ x t)

source

@[simp]

theorem SurroundingFamily.path_t₀ {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} (h : SurroundingFamily g b γ U) (x : E) :

h.path x 0 = Path.refl (b x)

source

theorem SurroundingFamilyIn.to_sf {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {Ω : Set (E × F)} {γ : E → ℝ → Loop F} (h : SurroundingFamilyIn g b γ U Ω) :

SurroundingFamily g b γ U

Abbreviation for toSurroundingFamily

source

theorem SurroundingFamilyIn.val_in {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {Ω : Set (E × F)} {γ : E → ℝ → Loop F} (h : SurroundingFamilyIn g b γ U Ω) {x : E} (hx : x ∈ U) {t s : ℝ} :

(x, ↑(γ x t) s) ∈ Ω

source

theorem SurroundingFamilyIn.mono {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {Ω : Set (E × F)} {γ : E → ℝ → Loop F} (h : SurroundingFamilyIn g b γ U Ω) {V : Set E} (hVU : V ⊆ U) :

SurroundingFamilyIn g b γ V Ω

source

theorem SurroundingFamilyIn.reparam {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {Ω : Set (E × F)} {γ : E → ℝ → Loop F} (h : SurroundingFamilyIn g b γ U Ω) :

SurroundingFamilyIn g b (fun (x : E) (t : ℝ) => (γ x (linearReparam.toFun t)).reparam linearReparam) U Ω

Continuously reparameterize a surroundingFamilyIn so that it is constant near s ∈ {0,1} and t ∈ {0,1}

source

theorem local_loops {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {Ω : Set (E × F)} [FiniteDimensional ℝ F] {x₀ : E} (hΩ_op : ∃ U ∈ nhds x₀, IsOpen (Ω ∩ Prod.fst ⁻¹' U)) (hg : ContinuousAt g x₀) (hb : Continuous b) (hconv : g x₀ ∈ hull (connectedComponentIn (Prod.mk x₀ ⁻¹' Ω) (b x₀))) :

∃ (γ : E → ℝ → Loop F), ∃ U ∈ nhds x₀, SurroundingFamilyIn g b γ U Ω

Note: The conditions in this lemma are currently a bit weaker than the ones mentioned in the blueprint. TODO: use local_loops_def

source

theorem local_loops_open {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {Ω : Set (E × F)} [FiniteDimensional ℝ F] {x₀ : E} (hΩ_op : ∃ U ∈ nhds x₀, IsOpen (Ω ∩ Prod.fst ⁻¹' U)) (hg : ContinuousAt g x₀) (hb : Continuous b) (hconv : g x₀ ∈ hull (connectedComponentIn (Prod.mk x₀ ⁻¹' Ω) (b x₀))) :

∃ (γ : E → ℝ → Loop F) (U : Set E), IsOpen U ∧ x₀ ∈ U ∧ SurroundingFamilyIn g b γ U Ω

A tiny reformulation of local_loops where the existing U is open.

source

def ρ (t : ℝ) :

ℝ

Function used in satisfied_or_refund. Rename.

Equations

ρ t = projI (2 * (1 - t))

Instances For

source

theorem continuous_ρ :

Continuous ρ

source

@[simp]

theorem ρ_eq_one {x : ℝ} :

ρ x = 1 ↔ x ≤ 1 / 2

source

@[simp]

theorem ρ_eq_one_of_le {x : ℝ} (h : x ≤ 1 / 2) :

ρ x = 1

source

@[simp]

theorem ρ_eq_one_of_nonpos {x : ℝ} (h : x ≤ 0) :

ρ x = 1

source

@[simp]

theorem ρ_eq_zero {x : ℝ} :

ρ x = 0 ↔ 1 ≤ x

source

@[simp]

theorem ρ_eq_zero_of_le {x : ℝ} (h : 1 ≤ x) :

ρ x = 0

source

theorem ρ_mem_I {x : ℝ} :

ρ x ∈ unitInterval

source

def sfHomotopy {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {γ₀ γ₁ : E → ℝ → Loop F} (h₀ : SurroundingFamily g b γ₀ U) (h₁ : SurroundingFamily g b γ₁ U) (τ : ℝ) (x : E) (t : ℝ) :

Loop F

The homotopy of surrounding families of loops used in lemma satisfied_or_refund. Having this as a separate definition is useful, because the construction actually gives some more information about the homotopy than the theorem satisfied_or_refund gives.

Equations

sfHomotopy h₀ h₁ τ x t = Loop.ofPath ((h₀.path x (ρ τ * projI t)).strans (h₁.path x (ρ (1 - τ) * projI t)) (Set.projIcc 0 1 sfHomotopy.proof_1 (1 - τ)))

Instances For

source

@[simp]

theorem sfHomotopy_zero {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {γ₀ γ₁ : E → ℝ → Loop F} {h₀ : SurroundingFamily g b γ₀ U} {h₁ : SurroundingFamily g b γ₁ U} :

sfHomotopy h₀ h₁ 0 = γ₀

source

@[simp]

theorem sfHomotopy_one {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {γ₀ γ₁ : E → ℝ → Loop F} {h₀ : SurroundingFamily g b γ₀ U} {h₁ : SurroundingFamily g b γ₁ U} :

sfHomotopy h₀ h₁ 1 = γ₁

source

theorem Continuous.sfHomotopy {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {γ₀ γ₁ : E → ℝ → Loop F} {h₀ : SurroundingFamily g b γ₀ U} {h₁ : SurroundingFamily g b γ₁ U} {X : Type u_3} [UniformSpace X] [LocallyCompactSpace X] {τ t s : X → ℝ} {f : X → E} (hτ : Continuous τ) (hf : Continuous f) (ht : Continuous t) (hs : Continuous s) :

Continuous fun (x : X) => ↑(_root_.sfHomotopy h₀ h₁ (τ x) (f x) (t x)) (s x)

source

theorem continuous_sfHomotopy {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {γ₀ γ₁ : E → ℝ → Loop F} {h₀ : SurroundingFamily g b γ₀ U} {h₁ : SurroundingFamily g b γ₁ U} [NormedSpace ℝ E] [FiniteDimensional ℝ E] :

Continuous ↿(sfHomotopy h₀ h₁)

In this lemmas and the lemmas below we add FiniteDimensional ℝ E so that we can conclude LocallyCompactSpace E.

source

theorem surroundingFamily_sfHomotopy {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {γ₀ γ₁ : E → ℝ → Loop F} {h₀ : SurroundingFamily g b γ₀ U} {h₁ : SurroundingFamily g b γ₁ U} [NormedSpace ℝ E] [FiniteDimensional ℝ E] (τ : ℝ) :

SurroundingFamily g b (sfHomotopy h₀ h₁ τ) U

source

theorem sfHomotopy_in' {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {Ω : Set (E × F)} {γ₀ γ₁ : E → ℝ → Loop F} {ι : Sort u_3} (h₀ : SurroundingFamily g b γ₀ U) (h₁ : SurroundingFamily g b γ₁ U) (τ : ι → ℝ) (x : ι → E) (i : ι) {V : Set E} (hx : x i ∈ V) {t : ℝ} (ht : t ∈ unitInterval) {s : ℝ} (h_in₀ : ∀ (i : ι), x i ∈ V → ∀ t ∈ unitInterval, ∀ (s : ℝ), τ i ≠ 1 → (x i, ↑(γ₀ (x i) t) s) ∈ Ω) (h_in₁ : ∀ (i : ι), x i ∈ V → ∀ t ∈ unitInterval, ∀ (s : ℝ), τ i ≠ 0 → (x i, ↑(γ₁ (x i) t) s) ∈ Ω) :

(x i, ↑(sfHomotopy h₀ h₁ (τ i) (x i) t) s) ∈ Ω

A more precise version of sfHomotopy_in.

source

theorem sfHomotopy_in {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {Ω : Set (E × F)} {γ₀ γ₁ : E → ℝ → Loop F} (h₀ : SurroundingFamilyIn g b γ₀ U Ω) (h₁ : SurroundingFamilyIn g b γ₁ U Ω) (τ : ℝ) ⦃x : E⦄ (hx : x ∈ U) {t : ℝ} (ht : t ∈ unitInterval) {s : ℝ} :

(x, ↑(sfHomotopy ⋯ ⋯ τ x t) s) ∈ Ω

source

theorem surroundingFamilyIn_sfHomotopy {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {Ω : Set (E × F)} {γ₀ γ₁ : E → ℝ → Loop F} [NormedSpace ℝ E] [FiniteDimensional ℝ E] (h₀ : SurroundingFamilyIn g b γ₀ U Ω) (h₁ : SurroundingFamilyIn g b γ₁ U Ω) (τ : ℝ) :

SurroundingFamilyIn g b (sfHomotopy ⋯ ⋯ τ) U Ω

source

theorem satisfied_or_refund {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {U : Set E} {Ω : Set (E × F)} [NormedSpace ℝ E] [FiniteDimensional ℝ E] {γ₀ γ₁ : E → ℝ → Loop F} (h₀ : SurroundingFamilyIn g b γ₀ U Ω) (h₁ : SurroundingFamilyIn g b γ₁ U Ω) :

∃ (γ : ℝ → E → ℝ → Loop F), (∀ (τ : ℝ), SurroundingFamilyIn g b (γ τ) U Ω) ∧ γ 0 = γ₀ ∧ γ 1 = γ₁ ∧ Continuous ↿γ

source

theorem extend_loops {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {Ω : Set (E × F)} [FiniteDimensional ℝ E] {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁ : IsOpen U₁) (hK₀ : IsClosed K₀) (hK₁ : IsClosed K₁) (hKU₀ : K₀ ⊆ U₀) (hKU₁ : K₁ ⊆ U₁) {γ₀ γ₁ : E → ℝ → Loop F} (h₀ : SurroundingFamilyIn g b γ₀ U₀ Ω) (h₁ : SurroundingFamilyIn g b γ₁ U₁ Ω) :

∃ U ∈ nhdsSet (K₀ ∪ K₁), ∃ (γ : E → ℝ → Loop F), SurroundingFamilyIn g b γ U Ω ∧ (∀ᶠ (x : E) in nhdsSet K₀, γ x = γ₀ x) ∧ ∀ᶠ (x : E) in nhdsSet U₁ᶜ, γ x = γ₀ x

source

def ContinuousGerm {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] {x : E} (φ : (nhds x).Germ (ℝ → Loop F)) :

Prop

Equations

ContinuousGerm φ = Quotient.liftOn' φ (fun (γ : E → ℝ → Loop F) => ∀ (t s : ℝ), ContinuousAt (fun (p : E × ℝ × ℝ) => ↑(γ p.1 p.2.1) p.2.2) (x, t, s)) ⋯

Instances For

source

structure LoopFamilyGerm {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] (b : E → F) (x : E) (φ : (nhds x).Germ (ℝ → Loop F)) :

Prop

base (t : ℝ) : ↑(φ.value t) 0 = b x
t₀ (s : ℝ) : ↑(φ.value 0) s = b x
projI (t s : ℝ) : ↑(φ.value (_root_.projI t)) s = ↑(φ.value t) s
cont : ContinuousGerm φ

Instances For

source

structure SurroundingFamilyGerm {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (g : E → F) (Ω : Set (E × F)) (x : E) (φ : (nhds x).Germ (ℝ → Loop F)) :

Prop

Surrounds : (φ.value 1).Surrounds (g x)
val_in' (t : ℝ) : t ∈ unitInterval → ∀ s ∈ unitInterval, (x, ↑(φ.value t) s) ∈ Ω

Instances For

source

theorem surroundingFamilyIn_iff_germ {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {C : Set E} {Ω : Set (E × F)} {γ : E → ℝ → Loop F} :

SurroundingFamilyIn g b γ C Ω ↔ (∀ (x : E), LoopFamilyGerm b x ↑γ) ∧ ∀ x ∈ C, SurroundingFamilyGerm g Ω x ↑γ

source

theorem exists_surrounding_loops {E : Type u_1} [NormedAddCommGroup E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g b : E → F} {K : Set E} {Ω : Set (E × F)} [NormedSpace ℝ E] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [SecondCountableTopology E] (hK : IsClosed K) (hΩ_op : IsOpen Ω) (hg : ∀ (x : E), ContinuousAt g x) (hb : Continuous b) (hconv : ∀ (x : E), g x ∈ hull (connectedComponentIn (Prod.mk x ⁻¹' Ω) (b x))) {γ₀ : E → ℝ → Loop F} (hγ₀_surr : ∃ V ∈ nhdsSet K, SurroundingFamilyIn g b γ₀ V Ω) :

∃ (γ : E → ℝ → Loop F), SurroundingFamilyIn g b γ Set.univ Ω ∧ ∀ᶠ (x : E) in nhdsSet K, γ x = γ₀ x

Documentation

SphereEversion.Loops.Surrounding

Surrounding families of loops #