Slices of first order relations

Recal that a first order partial differential relation for maps between real normed vector spaces E and F is a set R in OneJet E F := E × F × (E →L[ℝ] F). In this file we study slices of such relations. The word slice is meant to convey the idea of intersecting with an affine subspace. Here we fix (x, y, φ) : OneJet E F and some hyperplane H in E. The points x and y are fixed and we will take a slice in E →L[ℝ] F by intersecting R with the affine subspace of linear maps that coincide with φ on H.

It will be convenient for convex integration purposes to identify this slice with F. There is no natural identification but we can build one by fixing more data that a hyperplane in E. Namely we fix p : DualPair E (where ker p.π is the relevant hyperplane) and reformulate "linear map that coincides with φ on H" as p.update φ w for some w : F.

This slice definition allows to define RelLoc.isAmple, the ampleness condition for first order relations: a relation is ample if all its slices are ample sets.

At the end of the file we consider 1-jet sections and slices corresponding to points in their image.

Slices and ampleness

def RelLoc.slice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) (p : DualPair E) (θ : E × F × (E →L[ℝ] F)) : Set F

The slice of a local relation R : RelLoc E F for a dual pair p at a jet θ is the set of w in F such that updating θ using p and w leads to a jet in R.

Equations

• R.slice p θ = {w : F | (θ.1, θ.2.1, p.update θ.2.2 w) ∈ R}

theorem RelLoc.mem_slice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) {p : DualPair E} {θ : E × F × (E →L[ℝ] F)} {w : F} : w ∈ R.slice p θ ↔ (θ.1, θ.2.1, p.update θ.2.2 w) ∈ R

def RelLoc.IsAmple {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) : Prop

A relation is ample if all its slices are ample.

Equations

• R.IsAmple = ∀ (p : DualPair E) (θ : E × F × (E →L[ℝ] F)), AmpleSet (R.slice p θ)

theorem RelLoc.IsAmple.mem_hull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (h : R.IsAmple) {θ : E × F × (E →L[ℝ] F)} (hθ : θ ∈ R) (v : F) (p : DualPair E) : v ∈ hull (connectedComponentIn (R.slice p θ) (θ.2.2 p.v))

theorem RelLoc.slice_update {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} {θ : E × F × (E →L[ℝ] F)} {p : DualPair E} (x : F) : R.slice p (θ.1, θ.2.1, p.update θ.2.2 x) = R.slice p θ

theorem RelLoc.isAmple_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} : R.IsAmple ↔ ∀ ⦃θ : OneJet E F⦄ (p : DualPair E), θ ∈ R → AmpleSet (R.slice p θ)

In order to check ampleness, it suffices to consider slices through elements of the relation.

theorem RelLoc.slice_of_ker_eq_ker {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} {θ : OneJet E F} {p p' : DualPair E} (hpp' : p.π = p'.π) : R.slice p θ = θ.2.2 (p.v - p'.v) +ᵥ R.slice p' θ

theorem RelLoc.ample_slice_of_ample_slice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} {θ : OneJet E F} {p p' : DualPair E} (hpp' : p.π = p'.π) (h : AmpleSet (R.slice p θ)) : AmpleSet (R.slice p' θ)

theorem RelLoc.ample_slice_of_forall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : RelLoc E F) {x : E} {y : F} {φ : E →L[ℝ] F} (p : DualPair E) (h : ∀ (w : F), (x, y, p.update φ w) ∈ R) : AmpleSet (R.slice p (x, y, φ))

Slices for 1-jet sections and formal solutions.

def JetSec.sliceAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) (R : RelLoc E F) (p : DualPair E) (x : E) : Set F

The slice associated to a jet section and a dual pair at some point.

Equations

• 𝓕.sliceAt R p x = R.slice p (x, 𝓕.f x, 𝓕.φ x)

def JetSec.IsShortAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) (R : RelLoc E F) (p : DualPair E) (x : E) : Prop

A 1-jet section 𝓕 is short for a dual pair p at a point x if the derivative of the function 𝓕.f at x is in the convex hull of the relevant connected component of the corresponding slice.

Equations

• 𝓕.IsShortAt R p x = ((D 𝓕.f x) p.v ∈ hull (connectedComponentIn (𝓕.sliceAt R p x) ((𝓕.φ x) p.v)))

def RelLoc.FormalSol.sliceAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (𝓕 : R.FormalSol) (p : DualPair E) (x : E) : Set F

The slice associated to a formal solution and a dual pair at some point.

Equations

• 𝓕.sliceAt p x = R.slice p (x, (↑𝓕).f x, (↑𝓕).φ x)

def RelLoc.FormalSol.IsShortAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (𝓕 : R.FormalSol) (p : DualPair E) (x : E) : Prop

A formal solution 𝓕 is short for a dual pair p at a point x if the derivative of the function 𝓕.f at x is in the convex hull of the relevant connected component of the corresponding slice.

Equations

• 𝓕.IsShortAt p x = ((D (↑𝓕).f x) p.v ∈ hull (connectedComponentIn (𝓕.sliceAt p x) (((↑𝓕).φ x) p.v)))

theorem RelLoc.IsAmple.isShortAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {R : RelLoc E F} (hR : R.IsAmple) (𝓕 : R.FormalSol) (p : DualPair E) (x : E) : 𝓕.IsShortAt p x