The actual slot phase and its material defect

This module uses the phase in equation (26), with independent slot coordinates ((R,(Z,T)),(θ,v)). The base frequencies F,G depend on the slow coordinates (R,Z,T). All derivatives of these functions below are actual Fréchet derivatives. The primary material operator uses the manuscript's backward-time convention ∂v - ε ∂T from equation (25).

@[reducible, inline]

abbrev NavierStokes.PhaseCalculus.Slow : Type

Slow: an abbreviation for ℝ × (ℝ × ℝ).

Equations

• NavierStokes.PhaseCalculus.Slow = (ℝ × ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.PhaseCalculus.Slot : Type

Slot: an abbreviation for Slow × (ℝ × ℝ).

Equations

• NavierStokes.PhaseCalculus.Slot = (NavierStokes.PhaseCalculus.Slow × ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.PhaseCalculus.Vec3 : Type

Vec3: an abbreviation for EuclideanSpace ℝ (Fin 3).

Equations

• NavierStokes.PhaseCalculus.Vec3 = EuclideanSpace ℝ (Fin 3)

def NavierStokes.PhaseCalculus.eR : Slot

E R, given by ((1, (0, 0)), (0, 0)).

Equations

• NavierStokes.PhaseCalculus.eR = ((1, 0, 0), 0, 0)

def NavierStokes.PhaseCalculus.eZ : Slot

E Z, given by ((0, (1, 0)), (0, 0)).

Equations

• NavierStokes.PhaseCalculus.eZ = ((0, 1, 0), 0, 0)

def NavierStokes.PhaseCalculus.eT : Slot

E T, given by ((0, (0, 1)), (0, 0)).

Equations

• NavierStokes.PhaseCalculus.eT = ((0, 0, 1), 0, 0)

def NavierStokes.PhaseCalculus.eTheta : Slot

E theta, given by ((0, (0, 0)), (1, 0)).

Equations

• NavierStokes.PhaseCalculus.eTheta = ((0, 0, 0), 1, 0)

def NavierStokes.PhaseCalculus.eV : Slot

E V, given by ((0, (0, 0)), (0, 1)).

Equations

• NavierStokes.PhaseCalculus.eV = ((0, 0, 0), 0, 1)

noncomputable def NavierStokes.PhaseCalculus.slowR (F : Slow → ℝ) (s : Slow) : ℝ

Slow R, given by fderiv ℝ F s (1, (0, 0)).

Equations

• NavierStokes.PhaseCalculus.slowR F s = (fderiv ℝ F s) (1, 0, 0)

noncomputable def NavierStokes.PhaseCalculus.slowZ (F : Slow → ℝ) (s : Slow) : ℝ

Slow Z, given by fderiv ℝ F s (0, (1, 0)).

Equations

• NavierStokes.PhaseCalculus.slowZ F s = (fderiv ℝ F s) (0, 1, 0)

noncomputable def NavierStokes.PhaseCalculus.slowT (F : Slow → ℝ) (s : Slow) : ℝ

Slow T, given by fderiv ℝ F s (0, (0, 1)).

Equations

• NavierStokes.PhaseCalculus.slowT F s = (fderiv ℝ F s) (0, 0, 1)

noncomputable def NavierStokes.PhaseCalculus.phase (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) : ℝ

Equation (26). The axial term (pz/ε)*Z equals pz*Z/ε.

Equations

• NavierStokes.PhaseCalculus.phase ε p pz x0 F G q = p * q.2.1 + pz / ε * q.1.2.1 + x0 * q.1.1 - q.2.2 * (p * F q.1 + pz * G q.1)

theorem NavierStokes.PhaseCalculus.fderiv_phase_apply (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q w : Slot) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : (fderiv ℝ (phase ε p pz x0 F G) q) w = p * w.2.1 + pz / ε * w.1.2.1 + x0 * w.1.1 - (w.2.2 * (p * F q.1 + pz * G q.1) + q.2.2 * (p * (fderiv ℝ F q.1) w.1 + pz * (fderiv ℝ G q.1) w.1))

The full differential of the phase, with no abstract derivative variables.

theorem NavierStokes.PhaseCalculus.phase_dR (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : (fderiv ℝ (phase ε p pz x0 F G) q) eR = x0 - q.2.2 * (p * slowR F q.1 + pz * slowR G q.1)

theorem NavierStokes.PhaseCalculus.phase_dTheta (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : (fderiv ℝ (phase ε p pz x0 F G) q) eTheta = p

theorem NavierStokes.PhaseCalculus.phase_dZ (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : (fderiv ℝ (phase ε p pz x0 F G) q) eZ = pz / ε - q.2.2 * (p * slowZ F q.1 + pz * slowZ G q.1)

theorem NavierStokes.PhaseCalculus.phase_dT (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : (fderiv ℝ (phase ε p pz x0 F G) q) eT = -q.2.2 * (p * slowT F q.1 + pz * slowT G q.1)

theorem NavierStokes.PhaseCalculus.phase_dV (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : (fderiv ℝ (phase ε p pz x0 F G) q) eV = -(p * F q.1 + pz * G q.1)

noncomputable def NavierStokes.PhaseCalculus.phaseNormal (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) : Vec3

The cylindrical chart gradient (∂R Φ, R⁻¹∂θ Φ, ε∂Z Φ).

Equations

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

theorem NavierStokes.PhaseCalculus.phaseNormal_formula (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) (hε : ε ≠ 0) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : phaseNormal ε p pz x0 F G q = !₂[x0 - q.2.2 * (p * slowR F q.1 + pz * slowR G q.1), p / q.1.1, pz - ε * q.2.2 * (p * slowZ F q.1 + pz * slowZ G q.1)]

The exact normal vector in equation (26), derived from the actual phase.

theorem NavierStokes.PhaseCalculus.contDiff_phase {n : WithTop ℕ∞} (ε p pz x0 : ℝ) (F G : Slow → ℝ) (hF : ContDiff ℝ n F) (hG : ContDiff ℝ n G) : ContDiff ℝ n (phase ε p pz x0 F G)

Joint regularity in every slot coordinate, at any differentiability order.

def NavierStokes.PhaseCalculus.baseV (F : Slow → ℝ) (s : Slow) : ℝ

The chart angular velocity is V = R F.

Equations

• NavierStokes.PhaseCalculus.baseV F s = s.1 * F s

noncomputable def NavierStokes.PhaseCalculus.signedMaterialOp (σ ε : ℝ) (b F G : Slow → ℝ) (f : Slot → ℝ) (q : Slot) : ℝ

σ=-1 is the backward slow-time convention of (25); σ=1 describes the forward slow-time convention. The differential operators are real ones.

Equations

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

noncomputable def NavierStokes.PhaseCalculus.backwardMaterialOp (ε : ℝ) (b F G : Slow → ℝ) (f : Slot → ℝ) (q : Slot) : ℝ

Backward material op, given by signedMaterialOp (-1) ε b F G f q.

Equations

• NavierStokes.PhaseCalculus.backwardMaterialOp ε b F G f q = NavierStokes.PhaseCalculus.signedMaterialOp (-1) ε b F G f q

theorem NavierStokes.PhaseCalculus.signedMaterialOp_phase (σ ε p pz x0 : ℝ) (b F G : Slow → ℝ) (q : Slot) (hε : ε ≠ 0) (hR : 0 < q.1.1) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : signedMaterialOp σ ε b F G (phase ε p pz x0 F G) q = b q.1 * x0 - q.2.2 * (b q.1 * (p * slowR F q.1 + pz * slowR G q.1) + σ * ε * (p * slowT F q.1 + pz * slowT G q.1) + ε * G q.1 * (p * slowZ F q.1 + pz * slowZ G q.1))

Exact cancellation of the fast-time and leading angular/axial terms.

theorem NavierStokes.PhaseCalculus.backwardMaterialOp_phase (ε p pz x0 : ℝ) (b F G : Slow → ℝ) (q : Slot) (hε : ε ≠ 0) (hR : 0 < q.1.1) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) : backwardMaterialOp ε b F G (phase ε p pz x0 F G) q = b q.1 * x0 - q.2.2 * (b q.1 * (p * slowR F q.1 + pz * slowR G q.1) - ε * (p * slowT F q.1 + pz * slowT G q.1) + ε * G q.1 * (p * slowZ F q.1 + pz * slowZ G q.1))

The manuscript convention t* = ∂v - ε∂T gives the MINUS sign inside the slow-time part of the bracket (equivalently a positive term + ε v (p F_T + pz G_T) after expansion).

def NavierStokes.PhaseCalculus.angularShift (h : ℝ) (q : Slot) : Slot

Angular shift, given by (q.1, (q.2.1 + h, q.2.2)).

Equations

• NavierStokes.PhaseCalculus.angularShift h q = (q.1, q.2.1 + h, q.2.2)

theorem NavierStokes.PhaseCalculus.phase_angularShift (ε p pz x0 h : ℝ) (F G : Slow → ℝ) (q : Slot) : phase ε p pz x0 F G (angularShift h q) = phase ε p pz x0 F G q + p * h

noncomputable def NavierStokes.PhaseCalculus.harmonic (k : ℝ) (j : ℤ) (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) : ℂ

The actual complex carrier exp(i k j Φ), with integer harmonic j.

Equations

• NavierStokes.PhaseCalculus.harmonic k j ε p pz x0 F G q = Complex.exp (↑(k * ↑j * NavierStokes.PhaseCalculus.phase ε p pz x0 F G q) * Complex.I)

theorem NavierStokes.PhaseCalculus.harmonic_angularShift_two_pi (k : ℝ) (j m : ℤ) (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) (hkp : k * p = ↑m) : harmonic k j ε p pz x0 F G (angularShift (2 * Real.pi) q) = harmonic k j ε p pz x0 F G q

Rounding k*p to an integer makes every integer harmonic single-valued under one full turn of the angular coordinate.

theorem NavierStokes.PhaseCalculus.harmonic_theta_periodic (k : ℝ) (j m : ℤ) (ε p pz x0 : ℝ) (F G : Slow → ℝ) (s : Slow) (v : ℝ) (hkp : k * p = ↑m) : Function.Periodic (fun (θ : ℝ) => harmonic k j ε p pz x0 F G (s, θ, v)) (2 * Real.pi)

theorem NavierStokes.PhaseCalculus.contDiff_harmonic {n : WithTop ℕ∞} (k : ℝ) (j : ℤ) (ε p pz x0 : ℝ) (F G : Slow → ℝ) (hF : ContDiff ℝ n F) (hG : ContDiff ℝ n G) : ContDiff ℝ n (harmonic k j ε p pz x0 F G)

The complex harmonic is jointly smooth whenever the base frequencies are.

theorem NavierStokes.PhaseCalculus.contDiffAt_phaseNormal (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : Slot) (hR : q.1.1 ≠ 0) (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) : ContDiffAt ℝ (↑⊤) (phaseNormal ε p pz x0 F G) q

The actual cylindrical normal is jointly C∞ away from the axis.

noncomputable def NavierStokes.PhaseCalculus.normalSlotDerivative (ε p pz : ℝ) (F G : Slow → ℝ) (s : Slow) : Vec3

The exact fast-slot derivative of nΦ used by the tangent ODE.

Equations

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

theorem NavierStokes.PhaseCalculus.hasDerivAt_phaseNormal_slot (ε p pz x0 θ v : ℝ) (F G : Slow → ℝ) (s : Slow) (hε : ε ≠ 0) (hF : DifferentiableAt ℝ F s) (hG : DifferentiableAt ℝ G s) : HasDerivAt (fun (w : ℝ) => phaseNormal ε p pz x0 F G (s, θ, w)) (normalSlotDerivative ε p pz F G s) v

def NavierStokes.PhaseCalculus.referenceNormal (B s Kθ Kz : ℝ) : Vec3

The comparison vector B (s,K) used after equation (26).

Equations

• NavierStokes.PhaseCalculus.referenceNormal B s Kθ Kz = !₂[B * s, B * Kθ, B * Kz]

theorem NavierStokes.PhaseCalculus.vec3_norm_sq (w : Vec3) : ‖w‖ ^ 2 = w.ofLp 0 ^ 2 + w.ofLp 1 ^ 2 + w.ofLp 2 ^ 2

theorem NavierStokes.PhaseCalculus.referenceNormal_norm_ge (B s Kθ Kz : ℝ) (hK : Kθ ^ 2 + Kz ^ 2 = 1) : B ≤ ‖referenceNormal B s Kθ Kz‖

A unit tangential direction forces the reference vector to have norm at least B.

theorem NavierStokes.PhaseCalculus.phaseNormal_norm_lower (ε p pz x0 B s Kθ Kz δ : ℝ) (F G : Slow → ℝ) (q : Slot) (hK : Kθ ^ 2 + Kz ^ 2 = 1) (hclose : ‖phaseNormal ε p pz x0 F G q - referenceNormal B s Kθ Kz‖ ≤ δ) : B - δ ≤ ‖phaseNormal ε p pz x0 F G q‖

An explicit reference-vector error bound gives a quantitative lower bound for the actual phase normal. The comparison estimate itself is a hypothesis.

theorem NavierStokes.PhaseCalculus.phaseNormal_ne_zero_of_close (ε p pz x0 B s Kθ Kz : ℝ) (F G : Slow → ℝ) (q : Slot) (hB : 0 < B) (hK : Kθ ^ 2 + Kz ^ 2 = 1) (hclose : ‖phaseNormal ε p pz x0 F G q - referenceNormal B s Kθ Kz‖ ≤ B / 2) : phaseNormal ε p pz x0 F G q ≠ 0

Half-scale closeness ensures the denominator in the projected pulse equation is nonzero for this actual phase normal.