Actual differential calculus of a single harmonic

All directional operators below are evaluations of the Fréchet derivative. The direction fields may vary with the point, so their derivatives are included in the iterated operators. The cylindrical formulas use the unscaled angular direction, with its factors of R⁻¹ and R⁻² displayed explicitly.

Exact differential calculus on the auxiliary graph

The physical variables are (r,t) and the auxiliary variable is in ℝ². The graph is Y(r,t) = r^d • vr + t • vt, as in Definition 8.1 of the candidate manuscript. The radial formulas below are stated away from r = 0. All differential operators use Mathlib's actual Fréchet derivatives.

@[reducible, inline]

abbrev NavierStokes.GraphCalculus.Plane : Type

Plane: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.GraphCalculus.Plane = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.GraphCalculus.Lift : Type

Lift: an abbreviation for Plane × Plane.

Equations

• NavierStokes.GraphCalculus.Lift = (NavierStokes.GraphCalculus.Plane × NavierStokes.GraphCalculus.Plane)

noncomputable def NavierStokes.GraphCalculus.radialSpeed (d r : ℝ) : ℝ

The radial coefficient in the exact graph derivative.

Equations

• NavierStokes.GraphCalculus.radialSpeed d r = d * r ^ (d - 1)

noncomputable def NavierStokes.GraphCalculus.graph (d : ℝ) (vr vt q : Plane) : Lift

Embed physical radial/time coordinates in the auxiliary lift.

Equations

• NavierStokes.GraphCalculus.graph d vr vt q = (q, q.1 ^ d • vr + q.2 • vt)

noncomputable def NavierStokes.GraphCalculus.pullback (d : ℝ) (vr vt : Plane) (F : Lift → ℝ) : Plane → ℝ

Pullback, defined pointwise by F (graph d vr vt q).

Equations

• NavierStokes.GraphCalculus.pullback d vr vt F q = F (NavierStokes.GraphCalculus.graph d vr vt q)

noncomputable def NavierStokes.GraphCalculus.radialVector (d : ℝ) (vr : Plane) (p : Lift) : Lift

Radial vector, given by ((1, 0), radialSpeed d p.1.1 • vr).

Equations

• NavierStokes.GraphCalculus.radialVector d vr p = ((1, 0), NavierStokes.GraphCalculus.radialSpeed d p.1.1 • vr)

def NavierStokes.GraphCalculus.timeVector (vt : Plane) : Lift

Time vector, given by ((0, 1), vt).

Equations

• NavierStokes.GraphCalculus.timeVector vt = ((0, 1), vt)

noncomputable def NavierStokes.GraphCalculus.along (V : Lift → Lift) (F : Lift → ℝ) (p : Lift) : ℝ

Differentiation along a vector field, defined by the genuine derivative.

Equations

• NavierStokes.GraphCalculus.along V F p = (fderiv ℝ F p) (V p)

noncomputable def NavierStokes.GraphCalculus.radialOp (d : ℝ) (vr : Plane) (F : Lift → ℝ) : Lift → ℝ

Radial op, given by along (radialVector d vr) F.

Equations

• NavierStokes.GraphCalculus.radialOp d vr F = NavierStokes.GraphCalculus.along (NavierStokes.GraphCalculus.radialVector d vr) F

noncomputable def NavierStokes.GraphCalculus.timeOp (vt : Plane) (F : Lift → ℝ) : Lift → ℝ

Time op, given by along (fun _ => timeVector vt) F.

Equations

• NavierStokes.GraphCalculus.timeOp vt F = NavierStokes.GraphCalculus.along (fun (x : NavierStokes.GraphCalculus.Lift) => NavierStokes.GraphCalculus.timeVector vt) F

noncomputable def NavierStokes.GraphCalculus.partialR (u : Plane → ℝ) (q : Plane) : ℝ

Partial R, given by deriv (fun r => u (r, q.2)) q.1.

Equations

• NavierStokes.GraphCalculus.partialR u q = deriv (fun (r : ℝ) => u (r, q.2)) q.1

noncomputable def NavierStokes.GraphCalculus.partialT (u : Plane → ℝ) (q : Plane) : ℝ

Partial T, given by deriv (fun t => u (q.1, t)) q.2.

Equations

• NavierStokes.GraphCalculus.partialT u q = deriv (fun (t : ℝ) => u (q.1, t)) q.2

theorem NavierStokes.GraphCalculus.along_comm_of_cross_zero (F : Lift → ℝ) (V W : Lift → Lift) (p : Lift) (hF : ContDiffAt ℝ 2 F p) (hV : DifferentiableAt ℝ V p) (hW : DifferentiableAt ℝ W p) (hVW : (fderiv ℝ V p) (W p) = 0) (hWV : (fderiv ℝ W p) (V p) = 0) : along V (along W F) p = along W (along V F) p

A general commutator identity when both cross derivatives of the vector fields vanish. The regularity assumption is ordinary C² regularity.

theorem NavierStokes.GraphCalculus.hasDerivAt_graph_radial (d : ℝ) (vr vt : Plane) (r t : ℝ) (hr : r ≠ 0) : HasDerivAt (fun (s : ℝ) => graph d vr vt (s, t)) (radialVector d vr (graph d vr vt (r, t))) r

Exact derivative of the graph along a radial coordinate line.

theorem NavierStokes.GraphCalculus.hasDerivAt_graph_time (d : ℝ) (vr vt : Plane) (r t : ℝ) : HasDerivAt (fun (s : ℝ) => graph d vr vt (r, s)) (timeVector vt) t

The time direction has constant graph velocity.

theorem NavierStokes.GraphCalculus.partialR_pullback (d : ℝ) (vr vt : Plane) (F : Lift → ℝ) (q : Plane) (hr : q.1 ≠ 0) (hF : DifferentiableAt ℝ F (graph d vr vt q)) : partialR (pullback d vr vt F) q = radialOp d vr F (graph d vr vt q)

First radial derivative of the physical pullback equals the exact graph operator.

theorem NavierStokes.GraphCalculus.partialT_pullback (d : ℝ) (vr vt : Plane) (F : Lift → ℝ) (q : Plane) (hF : DifferentiableAt ℝ F (graph d vr vt q)) : partialT (pullback d vr vt F) q = timeOp vt F (graph d vr vt q)

First time derivative of the physical pullback equals the exact graph operator.

theorem NavierStokes.GraphCalculus.contDiffAt_graph {n : WithTop ℕ∞} (d : ℝ) (vr vt q : Plane) (hr : q.1 ≠ 0) : ContDiffAt ℝ n (graph d vr vt) q

The coordinate map is smooth to every order away from the axis.

noncomputable def NavierStokes.GraphCalculus.radialAcceleration (d r : ℝ) : ℝ

This form keeps the exponent arithmetic of the derivative explicit.

Equations

• NavierStokes.GraphCalculus.radialAcceleration d r = d * ((d - 1) * r ^ (d - 1 - 1))

theorem NavierStokes.GraphCalculus.differentiableAt_radialVector (d : ℝ) (vr : Plane) (p : Lift) (hr : p.1.1 ≠ 0) : DifferentiableAt ℝ (radialVector d vr) p

theorem NavierStokes.GraphCalculus.fderiv_radialVector_timeVector (d : ℝ) (vr vt : Plane) (p : Lift) (hr : p.1.1 ≠ 0) : (fderiv ℝ (radialVector d vr) p) (timeVector vt) = 0

The radial graph coefficient is independent of both time and the auxiliary coordinates. Its derivative in the time graph direction is zero.

theorem NavierStokes.GraphCalculus.radialOp_timeOp_comm (d : ℝ) (vr vt : Plane) (F : Lift → ℝ) (p : Lift) (hr : p.1.1 ≠ 0) (hF : ContDiffAt ℝ 2 F p) : radialOp d vr (timeOp vt F) p = timeOp vt (radialOp d vr F) p

The actual radial and time graph operators commute on every C² lift, away from the radial axis. This proves the relevant assertion of §8.1.

theorem NavierStokes.GraphCalculus.differentiableAt_timeOp (vt : Plane) (F : Lift → ℝ) (p : Lift) (hF : ContDiffAt ℝ 2 F p) : DifferentiableAt ℝ (timeOp vt F) p

theorem NavierStokes.GraphCalculus.differentiableAt_radialOp (d : ℝ) (vr : Plane) (F : Lift → ℝ) (p : Lift) (hr : p.1.1 ≠ 0) (hF : ContDiffAt ℝ 2 F p) : DifferentiableAt ℝ (radialOp d vr F) p

theorem NavierStokes.GraphCalculus.contDiffAt_pullback {n : WithTop ℕ∞} (d : ℝ) (vr vt : Plane) (F : Lift → ℝ) (q : Plane) (hr : q.1 ≠ 0) (hF : ContDiffAt ℝ n F (graph d vr vt q)) : ContDiffAt ℝ n (pullback d vr vt F) q

Restriction to the graph preserves each differentiability order away from the axis, in particular C∞ when the order is ∞.

theorem NavierStokes.GraphCalculus.partialR_partialT_pullback (d : ℝ) (vr vt : Plane) (F : Lift → ℝ) (q : Plane) (hr : q.1 ≠ 0) (hF : ContDiff ℝ 2 F) : partialR (partialT (pullback d vr vt F)) q = radialOp d vr (timeOp vt F) (graph d vr vt q)

Differentiate the restricted time derivative in the radial direction.

theorem NavierStokes.GraphCalculus.partialT_partialR_pullback (d : ℝ) (vr vt : Plane) (F : Lift → ℝ) (q : Plane) (hr : q.1 ≠ 0) (hF : ContDiff ℝ 2 F) : partialT (partialR (pullback d vr vt F)) q = timeOp vt (radialOp d vr F) (graph d vr vt q)

Differentiate the restricted radial derivative in the time direction.

theorem NavierStokes.GraphCalculus.mixed_partial_pullback_comm (d : ℝ) (vr vt : Plane) (F : Lift → ℝ) (q : Plane) (hr : q.1 ≠ 0) (hF : ContDiff ℝ 2 F) : partialR (partialT (pullback d vr vt F)) q = partialT (partialR (pullback d vr vt F)) q

The mixed physical derivatives commute, and both orders coincide with the corresponding iterated exact graph operators.

theorem NavierStokes.GraphCalculus.auxiliary_directional_eq (F : Lift → ℝ) (p : Lift) (v : Plane) : (fderiv ℝ F p) ((0, 0), v) = v.1 * (fderiv ℝ F p) ((0, 0), 1, 0) + v.2 * (fderiv ℝ F p) ((0, 0), 0, 1)

A derivative in an auxiliary direction is the ordinary dot product with the two auxiliary partial derivatives.

theorem NavierStokes.GraphCalculus.radialOp_expanded (d : ℝ) (vr : Plane) (F : Lift → ℝ) (p : Lift) : radialOp d vr F p = (fderiv ℝ F p) ((1, 0), 0, 0) + radialSpeed d p.1.1 * (vr.1 * (fderiv ℝ F p) ((0, 0), 1, 0) + vr.2 * (fderiv ℝ F p) ((0, 0), 0, 1))

This is exactly ∂r + d r^(d-1) (vr · ∂Y).

theorem NavierStokes.GraphCalculus.timeOp_expanded (vt : Plane) (F : Lift → ℝ) (p : Lift) : timeOp vt F p = (fderiv ℝ F p) ((0, 1), 0, 0) + (vt.1 * (fderiv ℝ F p) ((0, 0), 1, 0) + vt.2 * (fderiv ℝ F p) ((0, 0), 0, 1))

This is exactly ∂t + vt · ∂Y.

noncomputable def NavierStokes.HarmonicCalculus.along {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (V : E → E) (f : E → F) (x : E) : F

The actual derivative in a prescribed, possibly varying direction field.

Equations

• NavierStokes.HarmonicCalculus.along V f x = (fderiv ℝ f x) (V x)

theorem NavierStokes.HarmonicCalculus.contDiffOn_along {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {U : Set E} {V : E → E} {f : E → F} (hU : IsOpen U) (hV : ContDiffOn ℝ (↑⊤) V U) (hf : ContDiffOn ℝ (↑⊤) f U) : ContDiffOn ℝ (↑⊤) (along V f) U

theorem NavierStokes.HarmonicCalculus.along_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {U : Set E} {V : E → E} {f g : E → F} {x : E} (hU : IsOpen U) (hfg : Set.EqOn f g U) (hx : x ∈ U) : along V f x = along V g x

theorem NavierStokes.HarmonicCalculus.along_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (V : E → E) {f g : E → F} {x : E} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : along V (fun (y : E) => f y + g y) x = along V f x + along V g x

theorem NavierStokes.HarmonicCalculus.along_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) {f g : E → ℂ} {x : E} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : along V (fun (y : E) => f y * g y) x = along V f x * g x + f x * along V g x

theorem NavierStokes.HarmonicCalculus.along_const_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (c : ℂ) {f : E → ℂ} {x : E} (hf : DifferentiableAt ℝ f x) : along V (fun (y : E) => c * f y) x = c * along V f x

theorem NavierStokes.HarmonicCalculus.along_ofReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) {f : E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) : along V (fun (y : E) => ↑(f y)) x = ↑(along V f x)

noncomputable def NavierStokes.HarmonicCalculus.phaseFactor (κ : ℝ) : ℂ

The imaginary frequency i κ.

Equations

• NavierStokes.HarmonicCalculus.phaseFactor κ = ↑κ * Complex.I

theorem NavierStokes.HarmonicCalculus.phaseFactor_sq (κ : ℝ) : phaseFactor κ ^ 2 = -↑κ ^ 2

@[simp]

theorem NavierStokes.HarmonicCalculus.norm_phaseFactor (κ : ℝ) : ‖phaseFactor κ‖ = |κ|

noncomputable def NavierStokes.HarmonicCalculus.carrier {E : Type u_1} (κ : ℝ) (Φ : E → ℝ) (x : E) : ℂ

κ = k*j gives the carrier in the manuscript.

Equations

• NavierStokes.HarmonicCalculus.carrier κ Φ x = Complex.exp (NavierStokes.HarmonicCalculus.phaseFactor κ * ↑(Φ x))

@[simp]

theorem NavierStokes.HarmonicCalculus.carrier_ne_zero {E : Type u_1} (κ : ℝ) (Φ : E → ℝ) (x : E) : carrier κ Φ x ≠ 0

@[simp]

theorem NavierStokes.HarmonicCalculus.norm_carrier {E : Type u_1} (κ : ℝ) (Φ : E → ℝ) (x : E) : ‖carrier κ Φ x‖ = 1

theorem NavierStokes.HarmonicCalculus.contDiffOn_carrier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (κ : ℝ) {Φ : E → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) : ContDiffOn ℝ (↑⊤) (carrier κ Φ) U

theorem NavierStokes.HarmonicCalculus.differentiableAt_carrier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (κ : ℝ) {Φ : E → ℝ} {x : E} (hΦ : DifferentiableAt ℝ Φ x) : DifferentiableAt ℝ (carrier κ Φ) x

theorem NavierStokes.HarmonicCalculus.along_carrier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (κ : ℝ) {Φ : E → ℝ} {x : E} (hΦ : DifferentiableAt ℝ Φ x) : along V (carrier κ Φ) x = phaseFactor κ * ↑(along V Φ x) * carrier κ Φ x

noncomputable def NavierStokes.HarmonicCalculus.mode {E : Type u_1} (κ : ℝ) (Φ : E → ℝ) (a : E → ℂ) (x : E) : ℂ

A coefficient multiplied by one actual complex harmonic.

Equations

• NavierStokes.HarmonicCalculus.mode κ Φ a x = a x * NavierStokes.HarmonicCalculus.carrier κ Φ x

theorem NavierStokes.HarmonicCalculus.contDiffOn_mode {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (κ : ℝ) {Φ : E → ℝ} {a : E → ℂ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) : ContDiffOn ℝ (↑⊤) (mode κ Φ a) U

theorem NavierStokes.HarmonicCalculus.along_mode {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : E → E) (κ : ℝ) {Φ : E → ℝ} {a : E → ℂ} {x : E} (hΦ : DifferentiableAt ℝ Φ x) (ha : DifferentiableAt ℝ a x) : along V (mode κ Φ a) x = (along V a x + phaseFactor κ * ↑(along V Φ x) * a x) * carrier κ Φ x

First product formula, with the phase derivative and the coefficient derivative separated.

theorem NavierStokes.HarmonicCalculus.along_along_mode {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {V : E → E} (κ : ℝ) {Φ : E → ℝ} {a : E → ℂ} {x : E} (hU : IsOpen U) (hV : ContDiffOn ℝ (↑⊤) V U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hx : x ∈ U) : along V (along V (mode κ Φ a)) x = (along V (along V a) x + 2 * phaseFactor κ * ↑(along V Φ x) * along V a x + (phaseFactor κ * ↑(along V (along V Φ) x) - ↑κ ^ 2 * ↑(along V Φ x) ^ 2) * a x) * carrier κ Φ x

Second product formula. Because the direction field is inside along, its derivative is present in both along V (along V a) and the second phase derivative; no constancy of the field is assumed.

Cylindrical scalar operators

noncomputable def NavierStokes.HarmonicCalculus.cylindricalLaplacian {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (R : E → ℝ) (Vr Vθ Vz : E → E) (f : E → F) (x : E) : F

The scalar cylindrical Laplacian, also valid on prescribed graph directions. Vθ is the unscaled angular direction.

Equations

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

noncomputable def NavierStokes.HarmonicCalculus.phaseNormal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (Φ : E → ℝ) (x : E) : EuclideanSpace ℝ (Fin 3)

The actual phase gradient in the orthonormal cylindrical frame.

Equations

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

noncomputable def NavierStokes.HarmonicCalculus.phaseSquare {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (Φ : E → ℝ) (x : E) : ℝ

The phase-square coefficient before rewriting it as a normal norm.

Equations

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

theorem NavierStokes.HarmonicCalculus.phaseSquare_eq_norm_sq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (Φ : E → ℝ) (x : E) : phaseSquare R Vr Vθ Vz Φ x = ‖phaseNormal R Vr Vθ Vz Φ x‖ ^ 2

noncomputable def NavierStokes.HarmonicCalculus.phaseCross {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (Φ : E → ℝ) (a : E → ℂ) (x : E) : ℂ

The phase/coefficient cross term in the scalar Laplacian.

Equations

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

theorem NavierStokes.HarmonicCalculus.cylindricalLaplacian_mode {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (R : E → ℝ) {Vr Vθ Vz : E → E} (κ : ℝ) {Φ : E → ℝ} {a : E → ℂ} {x : E} (hU : IsOpen U) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hx : x ∈ U) : cylindricalLaplacian R Vr Vθ Vz (mode κ Φ a) x = (cylindricalLaplacian R Vr Vθ Vz a x + 2 * phaseFactor κ * phaseCross R Vr Vθ Vz Φ a x + (phaseFactor κ * ↑(cylindricalLaplacian R Vr Vθ Vz Φ x) - ↑κ ^ 2 * ↑(phaseSquare R Vr Vθ Vz Φ x)) * a x) * carrier κ Φ x

Exact phase-square, cross, and phase-divergence decomposition.

theorem NavierStokes.HarmonicCalculus.cylindricalLaplacian_mode_normal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (R : E → ℝ) {Vr Vθ Vz : E → E} (κ : ℝ) {Φ : E → ℝ} {a : E → ℂ} {x : E} (hU : IsOpen U) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hx : x ∈ U) : cylindricalLaplacian R Vr Vθ Vz (mode κ Φ a) x = (cylindricalLaplacian R Vr Vθ Vz a x + 2 * phaseFactor κ * phaseCross R Vr Vθ Vz Φ a x + (phaseFactor κ * ↑(cylindricalLaplacian R Vr Vθ Vz Φ x) - ↑κ ^ 2 * ↑(‖phaseNormal R Vr Vθ Vz Φ x‖ ^ 2)) * a x) * carrier κ Φ x

Equivalent formulation using the squared Euclidean length of the actual normal.

theorem NavierStokes.HarmonicCalculus.along_along_eq_zero_of_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {U : Set E} {V : E → E} {f : E → F} {c : F} {x : E} (hU : IsOpen U) (hf : Set.EqOn (along V f) (fun (x : E) => c) U) (hx : x ∈ U) : along V (along V f) x = 0

An angular derivative which is constant near the point has zero next angular derivative. This applies to the affine angular phase and to angularly independent stripped coefficients.

theorem NavierStokes.HarmonicCalculus.cylindricalLaplacian_angular_independent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {U : Set E} (R : E → ℝ) (Vr Vθ Vz : E → E) {f : E → F} {x : E} (hU : IsOpen U) (hf : Set.EqOn (along Vθ f) (fun (x : E) => 0) U) (hx : x ∈ U) : cylindricalLaplacian R Vr Vθ Vz f x = along Vr (along Vr f) x + (R x)⁻¹ • along Vr f x + along Vz (along Vz f) x

With no angular coefficient dependence, its scalar Laplacian contains only radial and axial coefficient derivatives.

theorem NavierStokes.HarmonicCalculus.cylindricalLaplacian_phase {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (R : E → ℝ) (Vr Vθ Vz : E → E) {Φ : E → ℝ} {p : ℝ} {x : E} (hU : IsOpen U) (hΦθ : Set.EqOn (along Vθ Φ) (fun (x : E) => p) U) (hx : x ∈ U) : cylindricalLaplacian R Vr Vθ Vz Φ x = along Vr (fun (y : E) => (phaseNormal R Vr Vθ Vz Φ y).ofLp 0) x + (phaseNormal R Vr Vθ Vz Φ x).ofLp 0 / R x + along Vz (fun (y : E) => (phaseNormal R Vr Vθ Vz Φ y).ofLp 2) x

For an affine angular phase, the phase-divergence term is exactly Dr n_r + n_r/R + Dz n_z.

theorem NavierStokes.HarmonicCalculus.cylindricalLaplacian_mode_angular_independent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (R : E → ℝ) {Vr Vθ Vz : E → E} (κ : ℝ) {Φ : E → ℝ} {a : E → ℂ} {p : ℝ} {x : E} (hU : IsOpen U) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (haθ : Set.EqOn (along Vθ a) (fun (x : E) => 0) U) (hΦθ : Set.EqOn (along Vθ Φ) (fun (x : E) => p) U) (hx : x ∈ U) : cylindricalLaplacian R Vr Vθ Vz (mode κ Φ a) x = (along Vr (along Vr a) x + (R x)⁻¹ • along Vr a x + along Vz (along Vz a) x + 2 * phaseFactor κ * (↑((phaseNormal R Vr Vθ Vz Φ x).ofLp 0) * along Vr a x + ↑((phaseNormal R Vr Vθ Vz Φ x).ofLp 2) * along Vz a x) + (phaseFactor κ * ↑(along Vr (fun (y : E) => (phaseNormal R Vr Vθ Vz Φ y).ofLp 0) x + (phaseNormal R Vr Vθ Vz Φ x).ofLp 0 / R x + along Vz (fun (y : E) => (phaseNormal R Vr Vθ Vz Φ y).ofLp 2) x) - ↑κ ^ 2 * ↑(‖phaseNormal R Vr Vθ Vz Φ x‖ ^ 2)) * a x) * carrier κ Φ x

The scalar part of the manuscript's no-slow-angular-dependence formula. Both the absent angular coefficient derivative and the affine angular phase are hypotheses on actual derivatives on an open set.

Divergence and the longitudinal gain

@[reducible, inline]

abbrev NavierStokes.HarmonicCalculus.ComplexVector : Type

Complex vector: an abbreviation for Fin 3 → ℂ.

Equations

• NavierStokes.HarmonicCalculus.ComplexVector = (Fin 3 → ℂ)

noncomputable def NavierStokes.HarmonicCalculus.normalDot (n : EuclideanSpace ℝ (Fin 3)) (a : ComplexVector) : ℂ

Complex-bilinear contraction with a real normal.

Equations

• NavierStokes.HarmonicCalculus.normalDot n a = ↑(n.ofLp 0) * a 0 + ↑(n.ofLp 1) * a 1 + ↑(n.ofLp 2) * a 2

noncomputable def NavierStokes.HarmonicCalculus.vectorMode {E : Type u_1} (κ : ℝ) (Φ : E → ℝ) (a : E → ComplexVector) (x : E) : ComplexVector

Vector mode, defined pointwise by mode κ Φ (fun y => a y i) x.

Equations

• NavierStokes.HarmonicCalculus.vectorMode κ Φ a x i = NavierStokes.HarmonicCalculus.mode κ Φ (fun (y : E) => a y i) x

noncomputable def NavierStokes.HarmonicCalculus.angularGenerator (a : ComplexVector) : ComplexVector

The derivative of the cylindrical frame with respect to angle.

Equations

• NavierStokes.HarmonicCalculus.angularGenerator a = ![-a 1, a 0, 0]

theorem NavierStokes.HarmonicCalculus.angularGenerator_sq (a : ComplexVector) : angularGenerator (angularGenerator a) = ![-a 0, -a 1, 0]

noncomputable def NavierStokes.HarmonicCalculus.cylindricalVectorLaplacian {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (a : E → ComplexVector) (x : E) : ComplexVector

The scalar component Laplacians plus the two cylindrical frame connections. Its identification with Cartesian vector Laplacian belongs to the cylindrical coordinate calculus.

Equations

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

theorem NavierStokes.HarmonicCalculus.cylindricalVectorLaplacian_vectorMode {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (R : E → ℝ) {Vr Vθ Vz : E → E} (κ : ℝ) {Φ : E → ℝ} {a : E → ComplexVector} {x : E} (hU : IsOpen U) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ∀ (i : Fin 3), ContDiffOn ℝ (↑⊤) (fun (y : E) => a y i) U) (hx : x ∈ U) : cylindricalVectorLaplacian R Vr Vθ Vz (vectorMode κ Φ a) x = fun (i : Fin 3) => (cylindricalVectorLaplacian R Vr Vθ Vz a x i + 2 * phaseFactor κ * phaseCross R Vr Vθ Vz Φ (fun (y : E) => a y i) x + (phaseFactor κ * ↑(cylindricalLaplacian R Vr Vθ Vz Φ x) - ↑κ ^ 2 * ↑(‖phaseNormal R Vr Vθ Vz Φ x‖ ^ 2)) * a x i + 2 * phaseFactor κ * ↑((phaseNormal R Vr Vθ Vz Φ x).ofLp 1 / R x) * angularGenerator (a x) i) * carrier κ Φ x

Harmonic vector Laplacian, including the additional angular frame term 2 i κ (n_θ/R) J a. All coefficient and phase derivatives remain actual directional Fréchet derivatives.

theorem NavierStokes.HarmonicCalculus.cylindricalVectorLaplacian_angular_independent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (R : E → ℝ) (Vr Vθ Vz : E → E) {a : E → ComplexVector} {x : E} (hU : IsOpen U) (haθ : ∀ (i : Fin 3), Set.EqOn (along Vθ fun (y : E) => a y i) (fun (x : E) => 0) U) (hx : x ∈ U) : cylindricalVectorLaplacian R Vr Vθ Vz a x = fun (i : Fin 3) => along Vr (along Vr fun (y : E) => a y i) x + (R x)⁻¹ • along Vr (fun (y : E) => a y i) x + along Vz (along Vz fun (y : E) => a y i) x + (R x ^ 2)⁻¹ • angularGenerator (angularGenerator (a x)) i

Angularly independent coefficients retain only the J² a/R² connection, namely -(a_r,a_θ,0)/R².

noncomputable def NavierStokes.HarmonicCalculus.cylindricalDivergence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (a : E → ComplexVector) (x : E) : ℂ

Divergence of physical cylindrical components in prescribed directions.

Equations

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

noncomputable def NavierStokes.HarmonicCalculus.strippedDivergence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vz : E → E) (a : E → ComplexVector) (x : E) : ℂ

The divergence of a coefficient with no angular dependence.

Equations

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

theorem NavierStokes.HarmonicCalculus.cylindricalDivergence_vectorMode {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) {Φ : E → ℝ} {a : E → ComplexVector} {x : E} (hΦ : DifferentiableAt ℝ Φ x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) : cylindricalDivergence R Vr Vθ Vz (vectorMode κ Φ a) x = (cylindricalDivergence R Vr Vθ Vz a x + phaseFactor κ * normalDot (phaseNormal R Vr Vθ Vz Φ x) (a x)) * carrier κ Φ x

theorem NavierStokes.HarmonicCalculus.longitudinal_identity {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) {Φ : E → ℝ} {a : E → ComplexVector} {x : E} (hΦ : DifferentiableAt ℝ Φ x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (haθ : along Vθ (fun (y : E) => a y 1) x = 0) (hdiv : cylindricalDivergence R Vr Vθ Vz (vectorMode κ Φ a) x = 0) : phaseFactor κ * normalDot (phaseNormal R Vr Vθ Vz Φ x) (a x) = -strippedDivergence R Vr Vz a x

Exact harmonic divergence forces the longitudinal identity. The only coefficient angular derivative used by divergence is that of a_θ.

noncomputable def NavierStokes.HarmonicCalculus.longitudinalCoefficient (n : EuclideanSpace ℝ (Fin 3)) (a : ComplexVector) : ℂ

The complex coefficient in the direction of the unit real normal.

Equations

• NavierStokes.HarmonicCalculus.longitudinalCoefficient n a = NavierStokes.HarmonicCalculus.normalDot n a / ↑‖n‖

@[simp]

theorem NavierStokes.HarmonicCalculus.norm_longitudinalCoefficient (n : EuclideanSpace ℝ (Fin 3)) (a : ComplexVector) : ‖longitudinalCoefficient n a‖ = ‖normalDot n a‖ / ‖n‖

theorem NavierStokes.HarmonicCalculus.norm_strippedDivergence_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vz : E → E) (a : E → ComplexVector) (x : E) : ‖strippedDivergence R Vr Vz a x‖ ≤ ‖along Vr (fun (y : E) => a y 0) x‖ + ‖a x 0‖ / |R x| + ‖along Vz (fun (y : E) => a y 2) x‖

theorem NavierStokes.HarmonicCalculus.normalDot_norm_eq_div {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) {Φ : E → ℝ} {a : E → ComplexVector} {x : E} (hκ : κ ≠ 0) (hΦ : DifferentiableAt ℝ Φ x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (haθ : along Vθ (fun (y : E) => a y 1) x = 0) (hdiv : cylindricalDivergence R Vr Vθ Vz (vectorMode κ Φ a) x = 0) : ‖normalDot (phaseNormal R Vr Vθ Vz Φ x) (a x)‖ = ‖strippedDivergence R Vr Vz a x‖ / |κ|

Exact divergence supplies the frequency gain; the identity is proved above from the actual harmonic derivative, not assumed here.

theorem NavierStokes.HarmonicCalculus.longitudinalCoefficient_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) {Φ : E → ℝ} {a : E → ComplexVector} {x : E} (hκ : κ ≠ 0) (hΦ : DifferentiableAt ℝ Φ x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (haθ : along Vθ (fun (y : E) => a y 1) x = 0) (hdiv : cylindricalDivergence R Vr Vθ Vz (vectorMode κ Φ a) x = 0) : ‖longitudinalCoefficient (phaseNormal R Vr Vθ Vz Φ x) (a x)‖ ≤ (‖along Vr (fun (y : E) => a y 0) x‖ + ‖a x 0‖ / |R x| + ‖along Vz (fun (y : E) => a y 2) x‖) / (|κ| * ‖phaseNormal R Vr Vθ Vz Φ x‖)

Quantitative pointwise gain using actual radial and axial derivatives of the coefficient.

theorem NavierStokes.HarmonicCalculus.longitudinal_gain_frequency {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) {Φ : E → ℝ} {a : E → ComplexVector} {x : E} {r₀ n₀ A Ar Az : ℝ} (hκ : κ ≠ 0) (hΦ : DifferentiableAt ℝ Φ x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (haθ : along Vθ (fun (y : E) => a y 1) x = 0) (hdiv : cylindricalDivergence R Vr Vθ Vz (vectorMode κ Φ a) x = 0) (hr₀ : 0 < r₀) (hr : r₀ ≤ R x) (hn₀ : 0 < n₀) (hn : n₀ ≤ ‖phaseNormal R Vr Vθ Vz Φ x‖) (hA : ‖a x 0‖ ≤ A) (hAr : ‖along Vr (fun (y : E) => a y 0) x‖ ≤ Ar) (hAz : ‖along Vz (fun (y : E) => a y 2) x‖ ≤ Az) : ‖longitudinalCoefficient (phaseNormal R Vr Vθ Vz Φ x) (a x)‖ ≤ (Ar + A / r₀ + Az) / (|κ| * n₀)

A lower bound on radius and normal, together with bounds on the actual coefficient derivatives, yields the uniform inverse-frequency gain.

theorem NavierStokes.HarmonicCalculus.longitudinal_gain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (R : E → ℝ) (Vr Vθ Vz : E → E) (k : ℝ) (j : ℤ) {Φ : E → ℝ} {a : E → ComplexVector} {x : E} {r₀ n₀ A Ar Az : ℝ} (hk : k ≠ 0) (hj : j ≠ 0) (hΦ : DifferentiableAt ℝ Φ x) (ha : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : E) => a y i) x) (haθ : along Vθ (fun (y : E) => a y 1) x = 0) (hdiv : cylindricalDivergence R Vr Vθ Vz (vectorMode (k * ↑j) Φ a) x = 0) (hr₀ : 0 < r₀) (hr : r₀ ≤ R x) (hn₀ : 0 < n₀) (hn : n₀ ≤ ‖phaseNormal R Vr Vθ Vz Φ x‖) (hA : ‖a x 0‖ ≤ A) (hAr : ‖along Vr (fun (y : E) => a y 0) x‖ ≤ Ar) (hAz : ‖along Vz (fun (y : E) => a y 2) x‖ ≤ Az) : ‖longitudinalCoefficient (phaseNormal R Vr Vθ Vz Φ x) (a x)‖ ≤ (Ar + A / r₀ + Az) / (|k| * |↑j| * n₀)

The manuscript frequency is κ = k*j, with a nonzero integer harmonic.

theorem NavierStokes.HarmonicCalculus.norm_along_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (V : E → E) (f : E → F) (x : E) : ‖along V f x‖ ≤ ‖fderiv ℝ f x‖ * ‖V x‖

Operator norms of the actual full coefficient derivatives can be used to supply the directional derivative bounds above.

Finite jets of the longitudinal contraction

theorem NavierStokes.HarmonicCalculus.contDiffOn_strippedDivergence {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {R : E → ℝ} {Vr Vz : E → E} {a : E → ComplexVector} (hU : IsOpen U) (hR : ContDiffOn ℝ (↑⊤) R U) (hRne : ∀ x ∈ U, R x ≠ 0) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (ha₀ : ContDiffOn ℝ (↑⊤) (fun (y : E) => a y 0) U) (ha₂ : ContDiffOn ℝ (↑⊤) (fun (y : E) => a y 2) U) : ContDiffOn ℝ (↑⊤) (strippedDivergence R Vr Vz a) U

theorem NavierStokes.HarmonicCalculus.normalDot_jet_norm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (R : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) {Φ : E → ℝ} {a : E → ComplexVector} {x : E} (m : ℕ) (hκ : κ ≠ 0) (hU : IsOpen U) (hΦ : DifferentiableOn ℝ Φ U) (ha : ∀ (i : Fin 3), DifferentiableOn ℝ (fun (y : E) => a y i) U) (haθ : ∀ y ∈ U, along Vθ (fun (z : E) => a z 1) y = 0) (hdiv : ∀ y ∈ U, cylindricalDivergence R Vr Vθ Vz (vectorMode κ Φ a) y = 0) (hS : ContDiffOn ℝ (↑⊤) (strippedDivergence R Vr Vz a) U) (hx : x ∈ U) : ‖iteratedFDeriv ℝ m (fun (y : E) => normalDot (phaseNormal R Vr Vθ Vz Φ y) (a y)) x‖ = ‖iteratedFDeriv ℝ m (strippedDivergence R Vr Vz a) x‖ / |κ|

At every derivative order, the contraction n·a has the same inverse-frequency factor. Derivatives of the normal are included on the left, and derivatives of the full coefficient divergence on the right.

theorem NavierStokes.HarmonicCalculus.normalDot_finiteJetBound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} (R : E → ℝ) (Vr Vθ Vz : E → E) (κ : ℝ) {Φ : E → ℝ} {a : E → ComplexVector} {m : ℕ} {C : ℝ} (hκ : κ ≠ 0) (hU : IsOpen U) (hΦ : DifferentiableOn ℝ Φ U) (ha : ∀ (i : Fin 3), DifferentiableOn ℝ (fun (y : E) => a y i) U) (haθ : ∀ y ∈ U, along Vθ (fun (z : E) => a z 1) y = 0) (hdiv : ∀ y ∈ U, cylindricalDivergence R Vr Vθ Vz (vectorMode κ Φ a) y = 0) (hS : ContDiffOn ℝ (↑⊤) (strippedDivergence R Vr Vz a) U) (hJ : JetBounds.FiniteJetBound m (strippedDivergence R Vr Vz a) U C) : JetBounds.FiniteJetBound m (fun (y : E) => normalDot (phaseNormal R Vr Vθ Vz Φ y) (a y)) U (C / |κ|)

Uniform finite-jet version of the exact contraction estimate.

theorem NavierStokes.HarmonicCalculus.strippedDivergence_finiteJetBound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {R : E → ℝ} {Vr Vz : E → E} {a : E → ComplexVector} {m : ℕ} {Ar Az Cr Cz CI : ℝ} (hU : IsOpen U) (hR : ContDiffOn ℝ (↑⊤) R U) (hRne : ∀ x ∈ U, R x ≠ 0) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (ha₀ : ContDiffOn ℝ (↑⊤) (fun (y : E) => a y 0) U) (ha₂ : ContDiffOn ℝ (↑⊤) (fun (y : E) => a y 2) U) (hAr : JetBounds.FiniteJetBound (m + 1) (fun (y : E) => a y 0) U Ar) (hAz : JetBounds.FiniteJetBound (m + 1) (fun (y : E) => a y 2) U Az) (hCr : JetBounds.FiniteJetBound m Vr U Cr) (hCz : JetBounds.FiniteJetBound m Vz U Cz) (hCI : JetBounds.FiniteJetBound m (fun (y : E) => (R y)⁻¹) U CI) : JetBounds.FiniteJetBound m (strippedDivergence R Vr Vz a) U (2 ^ m * Ar * Cr + ‖ContinuousLinearMap.lsmul ℝ ℝ‖ * 2 ^ m * CI * Ar + 2 ^ m * Az * Cz)

The coefficient divergence bound is derived from actual coefficient jets through order m+1, and graph-direction and inverse-radius jets through order m.

Compatibility with the phase and graph already formalized

theorem NavierStokes.HarmonicCalculus.carrier_eq_slot_harmonic (k : ℝ) (j : ℤ) (ε p pz x₀ : ℝ) (F G : PhaseCalculus.Slow → ℝ) : carrier (k * ↑j) (PhaseCalculus.phase ε p pz x₀ F G) = PhaseCalculus.harmonic k j ε p pz x₀ F G

This carrier is the previously formalized slot harmonic, including its integer-harmonic and angular-period conventions.

theorem NavierStokes.HarmonicCalculus.phaseNormal_eq_slot_normal (ε p pz x₀ : ℝ) (F G : PhaseCalculus.Slow → ℝ) (q : PhaseCalculus.Slot) : phaseNormal (fun (y : PhaseCalculus.Slot) => y.1.1) (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eR) (fun (x : PhaseCalculus.Slot) => PhaseCalculus.eTheta) (fun (x : PhaseCalculus.Slot) => ε • PhaseCalculus.eZ) (PhaseCalculus.phase ε p pz x₀ F G) q = PhaseCalculus.phaseNormal ε p pz x₀ F G q

The graph direction in the axial slot is ε ∂Z; after that rescaling the normal here is exactly the normal used in the phase module.

theorem NavierStokes.HarmonicCalculus.graph_deriv_radial_mode (d : ℝ) (vr vt : GraphCalculus.Plane) (κ : ℝ) {Φ : GraphCalculus.Lift → ℝ} {a : GraphCalculus.Lift → ℂ} {r t : ℝ} (hr : r ≠ 0) (hΦ : DifferentiableAt ℝ Φ (GraphCalculus.graph d vr vt (r, t))) (ha : DifferentiableAt ℝ a (GraphCalculus.graph d vr vt (r, t))) : deriv (fun (s : ℝ) => mode κ Φ a (GraphCalculus.graph d vr vt (s, t))) r = (along (GraphCalculus.radialVector d vr) a (GraphCalculus.graph d vr vt (r, t)) + phaseFactor κ * ↑(along (GraphCalculus.radialVector d vr) Φ (GraphCalculus.graph d vr vt (r, t))) * a (GraphCalculus.graph d vr vt (r, t))) * carrier κ Φ (GraphCalculus.graph d vr vt (r, t))

Restricting a complex harmonic to the actual auxiliary graph gives the radial product formula with the genuine radial graph vector field.

theorem NavierStokes.HarmonicCalculus.graph_deriv_time_mode (d : ℝ) (vr vt : GraphCalculus.Plane) (κ : ℝ) {Φ : GraphCalculus.Lift → ℝ} {a : GraphCalculus.Lift → ℂ} {r t : ℝ} (hΦ : DifferentiableAt ℝ Φ (GraphCalculus.graph d vr vt (r, t))) (ha : DifferentiableAt ℝ a (GraphCalculus.graph d vr vt (r, t))) : deriv (fun (s : ℝ) => mode κ Φ a (GraphCalculus.graph d vr vt (r, s))) t = (along (fun (x : GraphCalculus.Lift) => GraphCalculus.timeVector vt) a (GraphCalculus.graph d vr vt (r, t)) + phaseFactor κ * ↑(along (fun (x : GraphCalculus.Lift) => GraphCalculus.timeVector vt) Φ (GraphCalculus.graph d vr vt (r, t))) * a (GraphCalculus.graph d vr vt (r, t))) * carrier κ Φ (GraphCalculus.graph d vr vt (r, t))

The analogous actual graph pullback identity in its time direction.