Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Closed second-order semijets

This file contains closed superjets, closed subjets, and closure-induction principles for the closed semijet graph.

def ViscositySolns.SuperjetGraph {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) : Set ((Point n × ℝ) × Jet n)

The graph whose closure defines the closed superjet.

Equations

• ViscositySolns.SuperjetGraph C u = {z : (ViscositySolns.Point n × ℝ) × ViscositySolns.Jet n | z.1.1 ∈ C ∧ z.1.2 = u z.1.1 ∧ z.2 ∈ ViscositySolns.Superjet C u z.1.1}

def ViscositySolns.SubjetGraph {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) : Set ((Point n × ℝ) × Jet n)

The graph whose closure defines the closed subjet.

Equations

• ViscositySolns.SubjetGraph C u = {z : (ViscositySolns.Point n × ℝ) × ViscositySolns.Jet n | z.1.1 ∈ C ∧ z.1.2 = u z.1.1 ∧ z.2 ∈ ViscositySolns.Subjet C u z.1.1}

theorem ViscositySolns.mem_superjetGraph_of_mem_of_nhdsWithin_eq {n : ℕ} {K C : Set (Point n)} {u : Point n → ℝ} {z : (Point n × ℝ) × Jet n} (hKC : K ⊆ C) (hnhds : nhdsWithin z.1.1 K = nhdsWithin z.1.1 C) (hz : z ∈ SuperjetGraph K u) : z ∈ SuperjetGraph C u

A superjet graph point over a smaller set is a superjet graph point over a larger set when the two domains have the same germ at the base point.

theorem ViscositySolns.mem_subjetGraph_of_mem_of_nhdsWithin_eq {n : ℕ} {K C : Set (Point n)} {u : Point n → ℝ} {z : (Point n × ℝ) × Jet n} (hKC : K ⊆ C) (hnhds : nhdsWithin z.1.1 K = nhdsWithin z.1.1 C) (hz : z ∈ SubjetGraph K u) : z ∈ SubjetGraph C u

A subjet graph point over a smaller set is a subjet graph point over a larger set when the two domains have the same germ at the base point.

def ViscositySolns.ClosedSuperjet {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x : Point n) : Set (Jet n)

The closed superjet \bar J^{2,+}_C u(x).

Following CIL, the graph being closed records triples (x, u x, J), so the extra convergence condition on the values of u is part of the definition.

Equations

• ViscositySolns.ClosedSuperjet C u x = {J : ViscositySolns.Jet n | ((x, u x), J) ∈ closure (ViscositySolns.SuperjetGraph C u)}

def ViscositySolns.ClosedSubjet {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x : Point n) : Set (Jet n)

The closed subjet \bar J^{2,-}_C u(x).

As for ClosedSuperjet, closing the graph of (x, u x, J) encodes the convergence of both base points and function values.

Equations

• ViscositySolns.ClosedSubjet C u x = {J : ViscositySolns.Jet n | ((x, u x), J) ∈ closure (ViscositySolns.SubjetGraph C u)}

theorem ViscositySolns.closedSuperjet_of_closedSuperjet_of_mem_nhdsWithin {n : ℕ} {K C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hJ : J ∈ ClosedSuperjet K u x) : J ∈ ClosedSuperjet C u x

Closed superjets on a relative neighborhood are closed superjets on the ambient domain.

In quantified mathematical form, if K ⊆ C, K ∈ nhdsWithin x C, and J ∈ \overline J^{2,+}_K u(x), then J ∈ \overline J^{2,+}_C u(x).

theorem ViscositySolns.closedSubjet_of_closedSubjet_of_mem_nhdsWithin {n : ℕ} {K C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hJ : J ∈ ClosedSubjet K u x) : J ∈ ClosedSubjet C u x

Closed subjets on a relative neighborhood are closed subjets on the ambient domain.

In quantified mathematical form, if K ⊆ C, K ∈ nhdsWithin x C, and J ∈ \overline J^{2,-}_K u(x), then J ∈ \overline J^{2,-}_C u(x).

theorem ViscositySolns.superjet_subset_closedSuperjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} (hx : x ∈ C) : Superjet C u x ⊆ ClosedSuperjet C u x

theorem ViscositySolns.subjet_subset_closedSubjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} (hx : x ∈ C) : Subjet C u x ⊆ ClosedSubjet C u x

theorem ViscositySolns.superjet_translate_add_left {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {x0 x : Point n} {J : Jet n} (hJ : J ∈ Superjet K (fun (y : Point n) => u (x0 + y)) x) : J ∈ Superjet ((fun (y : Point n) => x0 + y) '' K) u (x0 + x)

Ordinary superjets are preserved by translating the domain.

In quantified mathematical form, if (p, X) ∈ J^{2,+}_K (x ↦ u(x0+x))(x), then (p, X) ∈ J^{2,+}_{x0+K} u(x0+x), where x0+K = {x0 + z | z ∈ K}.

theorem ViscositySolns.subjet_translate_add_left {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {x0 x : Point n} {J : Jet n} (hJ : J ∈ Subjet K (fun (y : Point n) => u (x0 + y)) x) : J ∈ Subjet ((fun (y : Point n) => x0 + y) '' K) u (x0 + x)

Ordinary subjets are preserved by translating the domain.

In quantified mathematical form, if (p, X) ∈ J^{2,-}_K (x ↦ u(x0+x))(x), then (p, X) ∈ J^{2,-}_{x0+K} u(x0+x), where x0+K = {x0 + z | z ∈ K}.

theorem ViscositySolns.closedSuperjet_translate_add_left {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {x0 x : Point n} {J : Jet n} (hJ : J ∈ ClosedSuperjet K (fun (y : Point n) => u (x0 + y)) x) : J ∈ ClosedSuperjet ((fun (y : Point n) => x0 + y) '' K) u (x0 + x)

Closed superjets are preserved by translating the domain.

In quantified mathematical form, if (p, X) ∈ \overline J^{2,+}_K (x ↦ u(x0+x))(x), then (p, X) ∈ \overline J^{2,+}_{x0+K} u(x0+x).

theorem ViscositySolns.closedSubjet_translate_add_left {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {x0 x : Point n} {J : Jet n} (hJ : J ∈ ClosedSubjet K (fun (y : Point n) => u (x0 + y)) x) : J ∈ ClosedSubjet ((fun (y : Point n) => x0 + y) '' K) u (x0 + x)

Closed subjets are preserved by translating the domain.

In quantified mathematical form, if (p, X) ∈ \overline J^{2,-}_K (x ↦ u(x0+x))(x), then (p, X) ∈ \overline J^{2,-}_{x0+K} u(x0+x).

theorem ViscositySolns.isClosed_closedSuperjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} : IsClosed (ClosedSuperjet C u x)

For fixed base point, the closed superjet fiber is topologically closed.

theorem ViscositySolns.isClosed_closedSubjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} : IsClosed (ClosedSubjet C u x)

For fixed base point, the closed subjet fiber is topologically closed.

theorem ViscositySolns.closedSuperjet_of_tendsto_closedSuperjet {n : ℕ} {α : Type u_1} {C : Set (Point n)} {u : Point n → ℝ} {l : Filter α} [l.NeBot] {x : Point n} {J : Jet n} {xᵢ : α → Point n} {Jᵢ : α → Jet n} (hx : Filter.Tendsto xᵢ l (nhds x)) (hu : Filter.Tendsto (fun (i : α) => u (xᵢ i)) l (nhds (u x))) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hmem : ∀ᶠ (i : α) in l, Jᵢ i ∈ ClosedSuperjet C u (xᵢ i)) : J ∈ ClosedSuperjet C u x

A limit of closed-superjet graph points is again in the closed-superjet graph.

In quantified mathematical form, suppose xᵢ -> x, u xᵢ -> u x, and Jᵢ -> J along a nontrivial filter. If for all indices in a set belonging to that filter one has Jᵢ ∈ \overline J^{2,+}_C u(xᵢ), then J ∈ \overline J^{2,+}_C u(x).

theorem ViscositySolns.closedSubjet_of_tendsto_closedSubjet {n : ℕ} {α : Type u_1} {C : Set (Point n)} {u : Point n → ℝ} {l : Filter α} [l.NeBot] {x : Point n} {J : Jet n} {xᵢ : α → Point n} {Jᵢ : α → Jet n} (hx : Filter.Tendsto xᵢ l (nhds x)) (hu : Filter.Tendsto (fun (i : α) => u (xᵢ i)) l (nhds (u x))) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hmem : ∀ᶠ (i : α) in l, Jᵢ i ∈ ClosedSubjet C u (xᵢ i)) : J ∈ ClosedSubjet C u x

A limit of closed-subjet graph points is again in the closed-subjet graph.

In quantified mathematical form, suppose xᵢ -> x, u xᵢ -> u x, and Jᵢ -> J along a nontrivial filter. If for all indices in a set belonging to that filter one has Jᵢ ∈ \overline J^{2,-}_C u(xᵢ), then J ∈ \overline J^{2,-}_C u(x).

theorem ViscositySolns.closedSuperjet_sub_const_of_closedSuperjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {δ : ℝ} (hJ : J ∈ ClosedSuperjet C u x) : J ∈ ClosedSuperjet C (fun (y : Point n) => u y - δ) x

Subtracting a constant from a function preserves closed superjet membership.

In quantified mathematical form, for every real number δ, if J ∈ \bar J^{2,+}_C u(x), then J ∈ \bar J^{2,+}_C (u - δ)(x).

theorem ViscositySolns.closedSuperjet_sub_const_iff {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {δ : ℝ} : J ∈ ClosedSuperjet C (fun (y : Point n) => u y - δ) x ↔ J ∈ ClosedSuperjet C u x

Subtracting a constant from a function does not change its closed superjet fibers.

In quantified mathematical form, for every real number δ, J ∈ \bar J^{2,+}_C (u - δ)(x) if and only if J ∈ \bar J^{2,+}_C u(x).

theorem ViscositySolns.closedSuperjet_sub_of_add_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} {A : Point n → Jet n} (hφ : ∀ y ∈ C, HasSecondOrderExpansionWithin C φ y (A y)) (hφ_cont : Continuous φ) (hA_cont : Continuous A) (hJ : J ∈ ClosedSuperjet C (fun (y : Point n) => u y + φ y) x) : J - A x ∈ ClosedSuperjet C u x

Subtracting a function with a second-order expansion at every point of C pulls back closed superjets of u + φ to closed superjets of u.

In quantified mathematical form, suppose that for every y ∈ C, the function φ has second-order expansion within C at y with jet A y, and suppose that φ and A are continuous. If J ∈ \bar J^{2,+}_C (u + φ)(x), then J - A x ∈ \bar J^{2,+}_C u(x).

theorem ViscositySolns.closedSubjet_sub_const_of_closedSubjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {δ : ℝ} (hJ : J ∈ ClosedSubjet C u x) : J ∈ ClosedSubjet C (fun (y : Point n) => u y - δ) x

Subtracting a constant from a function preserves closed subjet membership.

In quantified mathematical form, for every real number δ, if J ∈ \bar J^{2,-}_C u(x), then J ∈ \bar J^{2,-}_C (u - δ)(x).

theorem ViscositySolns.closedSubjet_sub_const_iff {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {δ : ℝ} : J ∈ ClosedSubjet C (fun (y : Point n) => u y - δ) x ↔ J ∈ ClosedSubjet C u x

Subtracting a constant from a function does not change its closed subjet fibers.

In quantified mathematical form, for every real number δ, J ∈ \bar J^{2,-}_C (u - δ)(x) if and only if J ∈ \bar J^{2,-}_C u(x).

theorem ViscositySolns.closedSubjet_sub_of_add_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J : Jet n} {A : Point n → Jet n} (hφ : ∀ y ∈ C, HasSecondOrderExpansionWithin C φ y (A y)) (hφ_cont : Continuous φ) (hA_cont : Continuous A) (hJ : J ∈ ClosedSubjet C (fun (y : Point n) => u y + φ y) x) : J - A x ∈ ClosedSubjet C u x

Subtracting a function with a second-order expansion at every point of C pulls back closed subjets of u + φ to closed subjets of u.

In quantified mathematical form, suppose that for every y ∈ C, the function φ has second-order expansion within C at y with jet A y, and suppose that φ and A are continuous. If J ∈ \bar J^{2,-}_C (u + φ)(x), then J - A x ∈ \bar J^{2,-}_C u(x).

theorem ViscositySolns.closedSubjet_neg_to_closedSuperjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ ClosedSubjet C u x) : J.neg ∈ ClosedSuperjet C (fun (y : Point n) => -u y) x

Closed subjets are dual to closed superjets under negation.

In standard mathematical terms, (p, X) ∈ \bar J^{2,-}_C u(x) implies (-p, -X) ∈ \bar J^{2,+}_C (-u)(x).

theorem ViscositySolns.closedSuperjet_neg_to_closedSubjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ ClosedSuperjet C u x) : J.neg ∈ ClosedSubjet C (fun (y : Point n) => -u y) x

Closed superjets are dual to closed subjets under negation.

In standard mathematical terms, (p, X) ∈ \bar J^{2,+}_C u(x) implies (-p, -X) ∈ \bar J^{2,-}_C (-u)(x).

theorem ViscositySolns.closedSubjet_neg_iff_closedSuperjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} : J ∈ ClosedSubjet C u x ↔ J.neg ∈ ClosedSuperjet C (fun (y : Point n) => -u y) x

Closed subjet membership is equivalent to closed superjet membership for the negated function and negated jet.

theorem ViscositySolns.closedSuperjet_neg_iff_closedSubjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} : J ∈ ClosedSuperjet C u x ↔ J.neg ∈ ClosedSubjet C (fun (y : Point n) => -u y) x

Closed superjet membership is equivalent to closed subjet membership for the negated function and negated jet.

theorem ViscositySolns.closedSuperjet_induction {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {S : Set ((Point n × ℝ) × Jet n)} (hclosed : IsClosed S) (hgraph : ∀ y ∈ C, ∀ K ∈ Superjet C u y, ((y, u y), K) ∈ S) (hJ : J ∈ ClosedSuperjet C u x) : ((x, u x), J) ∈ S

theorem ViscositySolns.closedSubjet_induction {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {S : Set ((Point n × ℝ) × Jet n)} (hclosed : IsClosed S) (hgraph : ∀ y ∈ C, ∀ K ∈ Subjet C u y, ((y, u y), K) ∈ S) (hJ : J ∈ ClosedSubjet C u x) : ((x, u x), J) ∈ S