Graph Pullback

noncomputable def EulerGraphPullback.graphMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (k : ℝ) (m : E) : E →L[ℝ] E × ℝ

The linear graph carrying the oscillating phase.

Equations

• EulerGraphPullback.graphMap k m = (ContinuousLinearMap.id ℝ E).prod (k • (InnerProductSpace.toDual ℝ E) m)

noncomputable def EulerGraphPullback.liftedDirection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (κ : ℝ) (m : E) : E →L[ℝ] E × ℝ

The constant lifted differential direction associated with a spatial vector.

Equations

• EulerGraphPullback.liftedDirection κ m = (κ • ContinuousLinearMap.id ℝ E).prod ((InnerProductSpace.toDual ℝ E) m)

theorem EulerGraphPullback.graphMap_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (k : ℝ) (m v : E) : (graphMap k m) v = (v, k * inner ℝ m v)

theorem EulerGraphPullback.liftedDirection_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (κ : ℝ) (m v : E) : (liftedDirection κ m) v = (κ • v, inner ℝ m v)

theorem EulerGraphPullback.graph_direction_identity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (k κ : ℝ) (hκ : k * κ = 1) (m v : E) : (graphMap k m) v = k • (liftedDirection κ m) v

theorem EulerGraphPullback.graph_fderiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E × ℝ → F) (k κ : ℝ) (hκ : k * κ = 1) (m x v : E) (hf : DifferentiableAt ℝ f ((graphMap k m) x)) : (fderiv ℝ (fun (y : E) => f ((graphMap k m) y)) x) v = k • (fderiv ℝ f ((graphMap k m) x)) ((liftedDirection κ m) v)

theorem EulerGraphPullback.smooth_gradient_potential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (v : E → E) (hv : ContDiff ℝ (↑⊤) v) (hsymm : ∀ (x a b : E), inner ℝ ((fderiv ℝ v x) a) b = inner ℝ ((fderiv ℝ v x) b) a) : ∃ (p : E → ℝ), ContDiff ℝ (↑⊤) p ∧ ∀ (x : E), gradient p x = v x

A smooth vector field with symmetric derivative has a genuine smooth scalar potential.

theorem EulerGraphPullback.lifted_closed_field_has_graph_potential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : E × ℝ → E) (hp : ContDiff ℝ (↑⊤) p) (k κ : ℝ) (hκ : k * κ = 1) (m : E) (hclosed : ∀ (z : E × ℝ) (a b : E), inner ℝ ((fderiv ℝ p z) ((liftedDirection κ m) a)) b = inner ℝ ((fderiv ℝ p z) ((liftedDirection κ m) b)) a) : ∃ (q : E → ℝ), ContDiff ℝ (↑⊤) q ∧ ∀ (x : E), gradient q x = κ • p ((graphMap k m) x)

Closedness for the lifted derivatives becomes a scalar pressure potential on the graph.