Dual pairs

Convex integration improves maps by successively modify their derivative in a direction of a vector field (almost) without changing their derivative along some complementary hyperplace.

In this file we introduce the linear algebra part of the story of such modifications. The main gadget here are dual pairs on a real topological vector space E. Each p : DualPair E is made of a (continuous) linear form p.π : E →L[ℝ] ℝ and a vector p.v : E such that p.π p.v = 1.

Those pairs are used to build the updating operation turning φ : E →L[ℝ] F into p.update φ w which equals φ on ker p.π and sends v to the given w : F.

After formalizing the above definitions, we first record a number of trivial algebraic lemmas. Then we prove a lemma which is geometrically obvious but not so easy to formalize: injective_update_iff states, starting with an injective φ, that the updated map p.update φ w is injective if and only if w isn't in the image of ker p.π under φ. This is crucial in order to apply convex integration to immersions.

Then we prove continuity and smoothness lemmas for this operation.

General theory

structure DualPair (E : Type u_1) [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] : Type u_1

A continuous linear form π and a vector v that pair to one. In particular ker π is a hyperplane and v spans a complement of this hyperplane.

• π : E →L[ℝ] ℝ
• v : E
• pairing : self.π self.v = 1

theorem DualPair.pi_ne_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (p : DualPair E) : p.π ≠ 0

theorem DualPair.ker_pi_ne_top {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (p : DualPair E) : LinearMap.ker p.π ≠ ⊤

theorem DualPair.v_ne_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (p : DualPair E) : p.v ≠ 0

def DualPair.spanV {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (p : DualPair E) : Submodule ℝ E

Given a dual pair p, p.span_v is the line spanned by p.v.

Equations

• p.spanV = Submodule.span ℝ {p.v}

theorem DualPair.mem_spanV {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (p : DualPair E) {u : E} : u ∈ p.spanV ↔ ∃ (t : ℝ), u = t • p.v

def DualPair.update {E : Type u_1} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (p : DualPair E) (φ : E →L[ℝ] F) (w : F) : E →L[ℝ] F

Update a continuous linear map φ : E →L[ℝ] F using a dual pair p on E and a vector w : F. The new map coincides with φ on ker p.π and sends p.v to w.

Equations

• p.update φ w = φ + (w - φ p.v) ⬝ p.π

@[simp]

theorem DualPair.update_ker_pi {E : Type u_1} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (p : DualPair E) (φ : E →L[ℝ] F) (w : F) {u : E} (hu : u ∈ LinearMap.ker p.π) : (p.update φ w) u = φ u

@[simp]

theorem DualPair.update_v {E : Type u_1} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (p : DualPair E) (φ : E →L[ℝ] F) (w : F) : (p.update φ w) p.v = w

@[simp]

theorem DualPair.update_self {E : Type u_1} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (p : DualPair E) (φ : E →L[ℝ] F) : p.update φ (φ p.v) = φ

@[simp]

theorem DualPair.update_update {E : Type u_1} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (p : DualPair E) (φ : E →L[ℝ] F) (w w' : F) : p.update (p.update φ w') w = p.update φ w

theorem DualPair.inf_eq_bot {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (p : DualPair E) : LinearMap.ker p.π ⊓ p.spanV = ⊥

theorem DualPair.sup_eq_top {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (p : DualPair E) : LinearMap.ker p.π ⊔ p.spanV = ⊤

theorem DualPair.decomp {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (p : DualPair E) (e : E) : ∃ u ∈ LinearMap.ker p.π, ∃ (t : ℝ), e = u + t • p.v

theorem DualPair.update_apply {E : Type u_1} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (p : DualPair E) (φ : E →L[ℝ] F) {w : F} {t : ℝ} {u : E} (hu : u ∈ LinearMap.ker p.π) : (p.update φ w) (u + t • p.v) = φ u + t • w

def DualPair.map {E : Type u_1} {E' : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup E'] [Module ℝ E'] [TopologicalSpace E'] (p : DualPair E) (L : E ≃L[ℝ] E') : DualPair E'

Map a dual pair under a linear equivalence.

Equations

• p.map L = { π := p.π.comp ↑L.symm, v := L p.v, pairing := ⋯ }

@[simp]

theorem DualPair.map_π {E : Type u_1} {E' : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup E'] [Module ℝ E'] [TopologicalSpace E'] (p : DualPair E) (L : E ≃L[ℝ] E') : (p.map L).π = p.π.comp ↑L.symm

@[simp]

theorem DualPair.map_v {E : Type u_1} {E' : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup E'] [Module ℝ E'] [TopologicalSpace E'] (p : DualPair E) (L : E ≃L[ℝ] E') : (p.map L).v = L p.v

theorem DualPair.update_comp_left {E : Type u_1} {F : Type u_3} {G : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (p : DualPair E) (ψ' : F →L[ℝ] G) (φ : E →L[ℝ] F) (w : F) : p.update (ψ'.comp φ) (ψ' w) = ψ'.comp (p.update φ w)

theorem DualPair.map_update_comp_right {E : Type u_1} {E' : Type u_2} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup E'] [Module ℝ E'] [TopologicalSpace E'] [NormedAddCommGroup F] [NormedSpace ℝ F] (p : DualPair E) (ψ' : E →L[ℝ] F) (φ : E ≃L[ℝ] E') (w : F) : (p.map φ).update (ψ'.comp ↑φ.symm) w = (p.update ψ' w).comp ↑φ.symm

Injectivity criterion

@[simp]

theorem DualPair.injective_update_iff {E : Type u_1} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (p : DualPair E) {φ : E →L[ℝ] F} (hφ : Function.Injective ⇑φ) {w : F} : Function.Injective ⇑(p.update φ w) ↔ w ∉ Submodule.map φ (LinearMap.ker p.π)

Smoothness and continuity

theorem DualPair.smooth_update {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] (p : DualPair E) {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {φ : G → E →L[ℝ] F} (hφ : 𝒞 (↑⊤) φ) {w : G → F} (hw : 𝒞 (↑⊤) w) : 𝒞 ↑⊤ fun (g : G) => p.update (φ g) (w g)

theorem DualPair.continuous_update {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] (p : DualPair E) {X : Type u_3} [TopologicalSpace X] {φ : X → E →L[ℝ] F} (hφ : Continuous φ) {w : X → F} (hw : Continuous w) : Continuous fun (g : X) => p.update (φ g) (w g)

def Basis.dualPair {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (e : Basis ι ℝ E) (i : ι) : DualPair E

Given a finite basis e : basis ι ℝ E, and i : ι, e.DualPair i is given by the ith basis element and its dual.

Equations

• e.dualPair i = { π := LinearMap.toContinuousLinearMap (e.dualBasis i), v := e i, pairing := ⋯ }