Local h-principle for open and ample relations

This file proves lem:h_principle_open_ample_loc from the blueprint. This is the local version of the h-principle for open and ample relations. The proof brings together the main result exist_loops from the loop folder (Chapter 1 in the blueprint) and the corrugation technique.

One formalization issue is that the whole construction carries around a lot of data. On paper it is easy to state one lemma listing once all this data and proving many properties. Here it is more convenient to give each property its own lemma so carrying around data, assumptions and constructions requires some planning. Our way to mitigate this issue is to use two ad-hoc structures Landscape and StepLandscape which partly bundle all this.

The Landscape structure record three sets in a vector space, a closed set C and two nested compact sets K₀ and K₁. This is the ambient data for the local h-principle result. We call this partly bundled because it doesn't include the data of the formal solution we want to improve. Instead we have a Prop-valued structure Landscape.accepts that takes a landscape and a formal solution and assert some compatibility conditions. There are four conditions, which is already enough motivation to introduce a structure instead of one definition using the logical conjunction operator that would lead to awkward and error prone access to the individual conditions.

The proof of this proposition involves an induction on a flag of subspaces (nested subspaces of increasing dimensions). For the purpose of this induction we use a second structure StepLandscape that extends Landscape with two more pieces of data, a subspace and a dual pair, and a compatibility condition, namely the subspace has to be in the hyperplane defined by the dual pair.

In this setup, given (L : StepLandscape E) {𝓕 : FormalSol R} (h : L.accepts R 𝓕), the loop family constructed by Chapter 2 is L.loop h. Together with corrugation, it is used to build L.improveStep h which is the homotopy of 1-jet sections improving the formal solution 𝓕 in that step of the main inductive proof. A rather long series of lemmas prove all the required properties of that homotopy, corresponding to lemma lem:integration_step from the blueprint.

The inductive proof itself is the proof of RelLoc.FormalSol.improve. Here all conclusions are stated at once this the induction requires to know about each of them to proceed to the next step. We could have introduced one more ad-hoc structure to record those conclusion but this isn't needed (at least in that Chapter) since we need to access its components only once.

structure Landscape (E : Type u_1) [NormedAddCommGroup E] : Type u_1

The setup for local h-principle is two compact subsets K₀ ⊆ K₁ in E with K₀ ⊆ interior K₁ and a closed subset C.

• C : Set E
• K₀ : Set E
• K₁ : Set E
• hC : IsClosed self.C
• hK₀ : IsCompact self.K₀
• hK₁ : IsCompact self.K₁
• h₀₁ : self.K₀ ⊆ interior self.K₁

Improvement step

This section proves lem:integration_step.

structure StepLandscape (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] extends Landscape E : Type u_1

The setup for a one-step improvement towards a local h-principle is two compact subsets K₀ ⊆ K₁ in E with K₀ ⊆ interior K₁ and a closed subset C together with a dual pair p and a subspace E' of the corresponding hyperplane ker p.π.

• C : Set E
• K₀ : Set E
• K₁ : Set E
• hC : IsClosed self.C
• hK₀ : IsCompact self.K₀
• hK₁ : IsCompact self.K₁
• h₀₁ : self.K₀ ⊆ interior self.K₁
• E' : Submodule ℝ E
• p : DualPair E
• hEp : self.E' ≤ LinearMap.ker self.p.π

structure StepLandscape.Accepts {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) (L : StepLandscape E) (𝓕 : JetSec E F) : Prop

A one-step improvement landscape accepts a formal solution if it can improve it.

• h_op : IsOpen R
• hK₀ : ∀ᶠ (x : E) in nhdsSet L.K₀, 𝓕.IsPartHolonomicAt L.E' x
• hShort (x : E) : 𝓕.IsShortAt R L.p x
• hC : ∀ᶠ (x : E) in nhdsSet L.C, 𝓕.IsHolonomicAt x

def StepLandscape.Ω {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) (L : StepLandscape E) (𝓕 : JetSec E F) : Set (E × F)

The union of all slices of R corresponding to 𝓕.

Equations

• StepLandscape.Ω R L 𝓕 = {p : E × F | p.2 ∈ 𝓕.sliceAt R L.p p.1}

def StepLandscape.π {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : StepLandscape E) : E →L[ℝ] ℝ

The linear form in a StepLandscape, coming from the underlying dual pair.

Equations

• L.π = L.p.π

def StepLandscape.v {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : StepLandscape E) : E

The vector in a StepLandscape, coming from the underlying dual pair.

Equations

• L.v = L.p.v

def StepLandscape.K {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : StepLandscape E) : Set E

One more compact set in the landscape: K₁ ∩ C, needed as an input to the loop construction.

Equations

• L.K = L.K₁ ∩ L.C

def StepLandscape.b {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : StepLandscape E) (𝓕 : JetSec E F) : E → F

The base function for the loop family associated in any jet section in a step landscape.

Equations

• L.b 𝓕 x = (𝓕.φ x) L.v

def StepLandscape.g {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : StepLandscape E) (𝓕 : JetSec E F) : E → F

The desired average for the loop family associated in any jet section in a step landscape.

Equations

• L.g 𝓕 x = (D 𝓕.f x) L.v

theorem StepLandscape.isCompact_K {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : StepLandscape E) : IsCompact L.K

theorem StepLandscape.Accepts.open {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] {L : StepLandscape E} {𝓕 : JetSec E F} (h : Accepts R L 𝓕) : IsOpen (Ω R L 𝓕)

theorem StepLandscape.smooth_b {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : StepLandscape E) (𝓕 : JetSec E F) : 𝒞 (↑⊤) (L.b 𝓕)

theorem StepLandscape.smooth_g {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : StepLandscape E) (𝓕 : JetSec E F) : 𝒞 (↑⊤) (L.g 𝓕)

theorem StepLandscape.Accepts.rel {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} {L : StepLandscape E} {𝓕 : JetSec E F} (h : Accepts R L 𝓕) : ∀ᶠ (x : E) in nhdsSet L.K, L.g 𝓕 x = L.b 𝓕 x

def StepLandscape.loop {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : StepLandscape E) {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) : ℝ → E → Loop F

The loop family to use in some landscape to improve a formal solution.

Equations

• L.loop h = Classical.choose ⋯

theorem StepLandscape.nice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : StepLandscape E) {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) : NiceLoop (L.g ↑𝓕) (L.b ↑𝓕) (Ω R L ↑𝓕) L.K (L.loop h)

theorem StepLandscape.update_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : StepLandscape E) {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (x : E) (s : ℝ) : L.p.update ((↑𝓕).φ x) (↑(L.loop h 0 x) s) = (↑𝓕).φ x

theorem StepLandscape.loop_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : StepLandscape E) {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) : 𝒞 ↑⊤ ↿(L.loop h)

theorem StepLandscape.loop_smooth' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : StepLandscape E) {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) {t : G → ℝ} (ht : 𝒞 (↑⊤) t) {s : G → ℝ} (hs : 𝒞 (↑⊤) s) {x : G → E} (hx : 𝒞 (↑⊤) x) : 𝒞 ↑⊤ fun (g : G) => ↑(L.loop h (t g) (x g)) (s g)

theorem StepLandscape.loop_C1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : StepLandscape E) {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (t : ℝ) : 𝒞 1 ↿(L.loop h t)

def StepLandscape.ρ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : StepLandscape E) : E → ℝ

The cut-off function associated to a step landscape, equal to one near K₀ and zero outside K₁.

Equations

• L.ρ = ⋯.choose

theorem StepLandscape.ρ_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : StepLandscape E) : 𝒞 (↑⊤) L.ρ

theorem StepLandscape.ρ_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : StepLandscape E) (x : E) : L.ρ x ∈ unitInterval

theorem StepLandscape.ρ_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : StepLandscape E) (x : E) : |L.ρ x| ≤ 1

theorem StepLandscape.hρ₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : StepLandscape E) : ∀ᶠ (x : E) in nhdsSet L.K₀, L.ρ x = 1

theorem StepLandscape.hρ_compl_K₁ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : StepLandscape E) {x : E} : x ∉ L.K₁ → L.ρ x = 0

def StepLandscape.improveStep {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : StepLandscape E) {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (N : ℝ) : HtpyJetSec E F

Homotopy of formal solutions obtained by corrugation in the direction of p : dualPair E in some landscape to improve a formal solution 𝓕 from being L.E'-holonomic to L.E' ⊔ span {p.v}-holonomic near L.K₀.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem StepLandscape.improveStep_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (N t : ℝ) (x : E) : ((L.improveStep h N) t) x = ((↑𝓕).f x + (smoothStep t * L.ρ x) • corrugation L.π N (L.loop h t) x, L.p.update ((↑𝓕).φ x) (↑(L.loop h (smoothStep t * L.ρ x) x) (N * L.π x)) + (smoothStep t * L.ρ x) • corrugation.remainder (⇑L.p.π) N (L.loop h 1) x)

@[simp]

theorem StepLandscape.improveStep_apply_f {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (N t : ℝ) (x : E) : ((L.improveStep h N) t).f x = (↑𝓕).f x + (smoothStep t * L.ρ x) • corrugation L.π N (L.loop h t) x

@[simp]

theorem StepLandscape.improveStep_apply_φ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (N t : ℝ) (x : E) : ((L.improveStep h N) t).φ x = L.p.update ((↑𝓕).φ x) (↑(L.loop h (smoothStep t * L.ρ x) x) (N * L.π x)) + (smoothStep t * L.ρ x) • corrugation.remainder (⇑L.p.π) N (L.loop h 1) x

theorem StepLandscape.improveStep_of_support {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} {h : Accepts R L ↑𝓕} {N t : ℝ} {x : E} (H : ∀ (t : ℝ), x ∉ Loop.support (L.loop h t)) : ((L.improveStep h N) t) x = 𝓕 x

theorem StepLandscape.improveStep_rel_t_eq_0 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (N : ℝ) : (L.improveStep h N) 0 = ↑𝓕

theorem StepLandscape.improveStep_rel_compl_K₁ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (N : ℝ) {x : E} (hx : x ∉ L.K₁) (t : ℝ) : ((L.improveStep h N) t) x = 𝓕 x

theorem StepLandscape.improveStep_rel_K {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (N : ℝ) : ∀ᶠ (x : E) in nhdsSet L.K, ∀ (t : ℝ), ((L.improveStep h N) t) x = 𝓕 x

theorem StepLandscape.improveStep_rel_C {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) (N : ℝ) : ∀ᶠ (x : E) in nhdsSet L.C, ∀ (t : ℝ), ((L.improveStep h N) t) x = 𝓕 x

theorem StepLandscape.bu_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : StepLandscape E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (t : ℝ) (x : E) {v : F} {ε : ℝ} (hv : ‖v‖ < ε) : ‖(smoothStep t * L.ρ x) • v‖ < ε

theorem StepLandscape.improveStep_c0_close {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) {ε : ℝ} (ε_pos : 0 < ε) : ∀ᶠ (N : ℝ) in Filter.atTop, ∀ (x : E) (t : ℝ), ‖((L.improveStep h N) t).f x - (↑𝓕).f x‖ ≤ ε

theorem StepLandscape.improveStep_part_hol {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) {N : ℝ} (hN : N ≠ 0) : ∀ᶠ (x : E) in nhdsSet L.K₀, ((L.improveStep h N) 1).IsPartHolonomicAt (L.p.spanV ⊔ L.E') x

theorem StepLandscape.improveStep_formalSol {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {L : StepLandscape E} {𝓕 : R.FormalSol} (h : Accepts R L ↑𝓕) : ∀ᶠ (N : ℝ) in Filter.atTop, ∀ (t : ℝ), ((L.improveStep h N) t).IsFormalSol R

Full improvement

This section proves lem:h_principle_open_ample_loc.

theorem RelLoc.FormalSol.improve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {R : RelLoc E F} (h_op : IsOpen R) (h_ample : R.IsAmple) (L : Landscape E) {ε : ℝ} (ε_pos : 0 < ε) (𝓕 : R.FormalSol) (h_hol : ∀ᶠ (x : E) in nhdsSet L.C, 𝓕.IsHolonomicAt x) : ∃ (H : HtpyJetSec E F), (∀ᶠ (t : ℝ) in nhdsSet (Set.Iic 0), H t = ↑𝓕) ∧ (∀ᶠ (t : ℝ) in nhdsSet (Set.Ici 1), H t = H 1) ∧ (∀ᶠ (x : E) in nhdsSet L.C, ∀ (t : ℝ), (H t) x = 𝓕 x) ∧ (∀ x ∉ L.K₁, ∀ (t : ℝ), (H t) x = 𝓕 x) ∧ (∀ (x : E) (t : ℝ), ‖(H t).f x - (↑𝓕).f x‖ ≤ ε) ∧ (∀ (t : ℝ), (H t).IsFormalSol R) ∧ ∀ᶠ (x : E) in nhdsSet L.K₀, (H 1).IsHolonomicAt x

Homotopy of formal solutions obtained by successive corrugations in some landscape L to improve a formal solution 𝓕 until it becomes holonomic near L.K₀.

theorem RelLoc.FormalSol.improve_htpy' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {R : RelLoc E F} (h_op : IsOpen R) (h_ample : R.IsAmple) (L : Landscape E) {ε : ℝ} (ε_pos : 0 < ε) (𝓕 : R.FormalSol) (h_hol : ∀ᶠ (x : E) in nhdsSet L.C, 𝓕.IsHolonomicAt x) : ∃ (H : R.HtpyFormalSol), (∀ᶠ (t : ℝ) in nhdsSet (Set.Iic 0), H t = ↑𝓕) ∧ (∀ᶠ (t : ℝ) in nhdsSet (Set.Ici 1), H t = H 1) ∧ (∀ᶠ (x : E) in nhdsSet L.C, ∀ (t : ℝ), (H t) x = 𝓕 x) ∧ (∀ x ∉ L.K₁, ∀ (t : ℝ), (H t) x = 𝓕 x) ∧ (∀ (x : E) (t : ℝ), ‖(H t).f x - (↑𝓕).f x‖ < ε) ∧ ∀ᶠ (x : E) in nhdsSet L.K₀, (H 1).IsHolonomicAt x

A repackaging of RelLoc.FormalSol.improve for convenience.