Weighted classes of actual cylindrical curl corrections

All differential operators act on the actual coefficient functions. The oscillatory carrier is removed only after applying the product rule. The radial graph derivative and every cylindrical connection are retained.

Real oscillatory curl realization

The potential and curl below use actual Euclidean spatial derivatives. The oscillatory carrier is kept separate from the stripped remainder coefficient.

Algebra of the curl realization in Lemma 8.8

The dot product below is bilinear, including over ℂ: for a real phase normal its self-product is the real squared length. These results check the principal symbol and the algebraic divergence cancellation. They do not establish regularity, bounds for the differentiated amplitude, or descent from the lift.

@[reducible, inline]

abbrev NavierStokes.CurlGeometry.Vec3 (R : Type u_1) : Type u_1

Vec3: an abbreviation for Fin 3 → R.

Equations

• NavierStokes.CurlGeometry.Vec3 R = (Fin 3 → R)

def NavierStokes.CurlGeometry.dot {R : Type u_1} [CommRing R] (u v : Vec3 R) : R

Dot, given by u 0 * v 0 + u 1 * v 1 + u 2 * v 2.

Equations

• NavierStokes.CurlGeometry.dot u v = u 0 * v 0 + u 1 * v 1 + u 2 * v 2

def NavierStokes.CurlGeometry.cross {R : Type u_1} [CommRing R] (u v : Vec3 R) : Vec3 R

Cross, given by ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0].

Equations

• NavierStokes.CurlGeometry.cross u v = ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0]

theorem NavierStokes.CurlGeometry.cross_perpendicular_left {R : Type u_1} [CommRing R] (u v : Vec3 R) : dot u (cross u v) = 0

theorem NavierStokes.CurlGeometry.cross_perpendicular_right {R : Type u_1} [CommRing R] (u v : Vec3 R) : dot v (cross u v) = 0

theorem NavierStokes.CurlGeometry.triple_product {R : Type u_1} [CommRing R] (n a : Vec3 R) : cross n (cross n a) = dot n a • n - dot n n • a

The vector triple-product identity, before imposing tangency.

theorem NavierStokes.CurlGeometry.tangent_double_cross {R : Type u_1} [CommRing R] (n a : Vec3 R) (ha : dot n a = 0) : cross n (cross n a) = -(dot n n • a)

Tangency is exactly the hypothesis eliminating the longitudinal term.

theorem NavierStokes.CurlGeometry.cross_smul {R : Type u_1} [CommRing R] (s t : R) (u v : Vec3 R) : cross (s • u) (t • v) = (s * t) • cross u v

theorem NavierStokes.CurlGeometry.real_dot_self_ne_zero {n : Vec3 ℝ} (hn : n ≠ 0) : dot n n ≠ 0

A nonzero real normal has nonzero squared length, as required in (30).

theorem NavierStokes.CurlGeometry.normalized_double_cross {R : Type u_1} [Field R] (n a : Vec3 R) (hn : dot n n ≠ 0) (ha : dot n a = 0) : (-1 / dot n n) • cross n (cross n a) = a

The normalized double cross product displayed in Lemma 8.8.

noncomputable def NavierStokes.CurlGeometry.curlSymbol (ξ A : Vec3 ℂ) : Vec3 ℂ

Curl symbol, given by cross (Complex.I • ξ) A.

Equations

• NavierStokes.CurlGeometry.curlSymbol ξ A = NavierStokes.CurlGeometry.cross (Complex.I • ξ) A

noncomputable def NavierStokes.CurlGeometry.potentialCoefficient (k : ℂ) (n a : Vec3 ℂ) : Vec3 ℂ

The coefficient of the potential (30), with the oscillatory exponential factored out. k is its nonzero frequency and n its phase normal.

Equations

• NavierStokes.CurlGeometry.potentialCoefficient k n a = (Complex.I / (k * NavierStokes.CurlGeometry.dot n n)) • NavierStokes.CurlGeometry.cross n a

theorem NavierStokes.CurlGeometry.principal_symbol_realizes (k : ℂ) (n a : Vec3 ℂ) (hk : k ≠ 0) (hn : dot n n ≠ 0) (ha : dot n a = 0) : curlSymbol (k • n) (potentialCoefficient k n a) = a

The two factors of i and the vector triple product give the amplitude with the positive sign claimed in (30).

def NavierStokes.CurlGeometry.complexify (n : Vec3 ℝ) : Vec3 ℂ

Complexify, defined pointwise by (n j : ℂ).

Equations

• NavierStokes.CurlGeometry.complexify n j = ↑(n j)

theorem NavierStokes.CurlGeometry.complexify_dot_self (n : Vec3 ℝ) : dot (complexify n) (complexify n) = ↑(dot n n)

theorem NavierStokes.CurlGeometry.real_normal_principal_symbol (k : ℝ) (n : Vec3 ℝ) (a : Vec3 ℂ) (hk : k ≠ 0) (hn : n ≠ 0) (ha : dot (complexify n) a = 0) : curlSymbol (↑k • complexify n) (potentialCoefficient (↑k) (complexify n) a) = a

Specialization to the manuscript's real, nonzero phase normal and real, nonzero frequency. The only amplitude condition is complex tangency.

theorem NavierStokes.CurlGeometry.curl_symbol_transverse (ξ A : Vec3 ℂ) : dot ξ (curlSymbol ξ A) = 0

Cylindrical differential cancellation

This is a conditional identity for three additive differential operators on a commutative ring of coefficient functions. In the application q = 1/R. The assumptions state pairwise commutation and precisely the radial/axial product rules for multiplication by q used by the calculation. They must still be established for the manuscript's graph derivatives.

def NavierStokes.CurlGeometry.cylindricalCurl {F : Type u_1} [CommRing F] (Dr Dθ Dz : F →+ F) (q : F) (A : Vec3 F) : Vec3 F

Cylindrical curl, given by ![q * Dθ (A 2) - Dz (A 1), Dz (A 0) - Dr (A 2), Dr (A 1) + q * A 1 - q * Dθ (A 0)].

Equations

• NavierStokes.CurlGeometry.cylindricalCurl Dr Dθ Dz q A = ![q * Dθ (A 2) - Dz (A 1), Dz (A 0) - Dr (A 2), Dr (A 1) + q * A 1 - q * Dθ (A 0)]

def NavierStokes.CurlGeometry.cylindricalDiv {F : Type u_1} [CommRing F] (Dr Dθ Dz : F →+ F) (q : F) (v : Vec3 F) : F

Cylindrical div, given by Dr (v 0) + q * v 0 + q * Dθ (v 1) + Dz (v 2).

Equations

• NavierStokes.CurlGeometry.cylindricalDiv Dr Dθ Dz q v = Dr (v 0) + q * v 0 + q * Dθ (v 1) + Dz (v 2)

theorem NavierStokes.CurlGeometry.cylindrical_div_curl {F : Type u_1} [CommRing F] (Dr Dθ Dz : F →+ F) (q : F) (hrr : ∀ (f : F), Dr (q * f) = q * Dr f - q ^ 2 * f) (hzq : ∀ (f : F), Dz (q * f) = q * Dz f) (hrθ : ∀ (f : F), Dr (Dθ f) = Dθ (Dr f)) (hrz : ∀ (f : F), Dr (Dz f) = Dz (Dr f)) (hθz : ∀ (f : F), Dθ (Dz f) = Dz (Dθ f)) (A : Vec3 F) : cylindricalDiv Dr Dθ Dz q (cylindricalCurl Dr Dθ Dz q A) = 0

Divergence of the full cylindrical curl, including both 1/R terms. No conclusion about analytic regularity is hidden in the algebraic statement.

noncomputable def NavierStokes.OscillatoryCurl.crossLinear : ProblemStatement.Space →L[ℝ] ProblemStatement.Space →L[ℝ] ProblemStatement.Space

Cross product on the same Euclidean space as the PDE target, as a bounded bilinear map.

Equations

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

noncomputable def NavierStokes.OscillatoryCurl.cross (u v : ProblemStatement.Space) : ProblemStatement.Space

Cross, given by crossLinear u v.

Equations

• NavierStokes.OscillatoryCurl.cross u v = (NavierStokes.OscillatoryCurl.crossLinear u) v

theorem NavierStokes.OscillatoryCurl.cross_apply (u v : ProblemStatement.Space) : cross u v = u.ofLp 1 • v.ofLp 2 • ProblemStatement.coordinateVector 0 - u.ofLp 2 • v.ofLp 1 • ProblemStatement.coordinateVector 0 + u.ofLp 2 • v.ofLp 0 • ProblemStatement.coordinateVector 1 - u.ofLp 0 • v.ofLp 2 • ProblemStatement.coordinateVector 1 + u.ofLp 0 • v.ofLp 1 • ProblemStatement.coordinateVector 2 - u.ofLp 1 • v.ofLp 0 • ProblemStatement.coordinateVector 2

@[simp]

theorem NavierStokes.OscillatoryCurl.cross_zero (u v : ProblemStatement.Space) : (cross u v).ofLp 0 = u.ofLp 1 * v.ofLp 2 - u.ofLp 2 * v.ofLp 1

@[simp]

theorem NavierStokes.OscillatoryCurl.cross_one (u v : ProblemStatement.Space) : (cross u v).ofLp 1 = u.ofLp 2 * v.ofLp 0 - u.ofLp 0 * v.ofLp 2

@[simp]

theorem NavierStokes.OscillatoryCurl.cross_two (u v : ProblemStatement.Space) : (cross u v).ofLp 2 = u.ofLp 0 * v.ofLp 1 - u.ofLp 1 * v.ofLp 0

@[simp]

theorem NavierStokes.OscillatoryCurl.cross_smul_left (c : ℝ) (u v : ProblemStatement.Space) : cross (c • u) v = c • cross u v

@[simp]

theorem NavierStokes.OscillatoryCurl.cross_smul_right (c : ℝ) (u v : ProblemStatement.Space) : cross u (c • v) = c • cross u v

@[simp]

theorem NavierStokes.OscillatoryCurl.cross_zero_right (u : ProblemStatement.Space) : cross u 0 = 0

theorem NavierStokes.OscillatoryCurl.inner_coordinates (u v : ProblemStatement.Space) : inner ℝ u v = u.ofLp 0 * v.ofLp 0 + u.ofLp 1 * v.ofLp 1 + u.ofLp 2 * v.ofLp 2

theorem NavierStokes.OscillatoryCurl.cross_coordinates (u v : ProblemStatement.Space) : (fun (i : Fin 3) => (cross u v).ofLp i) = CurlGeometry.cross (fun (i : Fin 3) => u.ofLp i) fun (i : Fin 3) => v.ofLp i

The Euclidean cross product agrees coordinatewise with the previously checked symbol algebra.

theorem NavierStokes.OscillatoryCurl.cross_triple (n a : ProblemStatement.Space) : cross n (cross n a) = inner ℝ n a • n - ‖n‖ ^ 2 • a

noncomputable def NavierStokes.OscillatoryCurl.normalCoefficient (n a : ProblemStatement.Space) : ProblemStatement.Space

The inverse-square-normal coefficient used by the real potential.

Equations

• NavierStokes.OscillatoryCurl.normalCoefficient n a = (‖n‖ ^ 2)⁻¹ • NavierStokes.OscillatoryCurl.cross n a

theorem NavierStokes.OscillatoryCurl.cross_normalCoefficient {n a : ProblemStatement.Space} (hn : n ≠ 0) (ha : inner ℝ n a = 0) : cross n (normalCoefficient n a) = -a

noncomputable def NavierStokes.OscillatoryCurl.gradientLinear : (ProblemStatement.Space →L[ℝ] ℝ) →L[ℝ] ProblemStatement.Space

The actual Euclidean gradient map applied to a scalar derivative.

Equations

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

@[simp]

theorem NavierStokes.OscillatoryCurl.gradientLinear_apply (L : ProblemStatement.Space →L[ℝ] ℝ) (i : Fin 3) : (gradientLinear L).ofLp i = L (ProblemStatement.coordinateVector i)

theorem NavierStokes.OscillatoryCurl.curlLinear_smulRight (L : ProblemStatement.Space →L[ℝ] ℝ) (a : ProblemStatement.Space) : SpatialCurl.curlLinear (L.smulRight a) = cross (gradientLinear L) a

theorem NavierStokes.OscillatoryCurl.curl_smul {f : ProblemStatement.Space → ℝ} {B : ProblemStatement.Space → ProblemStatement.Space} {x : ProblemStatement.Space} (hf : DifferentiableAt ℝ f x) (hB : DifferentiableAt ℝ B x) : SpatialCurl.curl (fun (y : ProblemStatement.Space) => f y • B y) x = cross (gradientLinear (fderiv ℝ f x)) (B x) + f x • SpatialCurl.curl B x

The genuine spatial curl product rule.

noncomputable def NavierStokes.OscillatoryCurl.carrier (k s : ℝ) : ℝ

Carrier, given by -Real.sin (k * s) / k.

Equations

• NavierStokes.OscillatoryCurl.carrier k s = -Real.sin (k * s) / k

theorem NavierStokes.OscillatoryCurl.carrier_hasDerivAt {k : ℝ} (hk : k ≠ 0) (s : ℝ) : HasDerivAt (carrier k) (-Real.cos (k * s)) s

theorem NavierStokes.OscillatoryCurl.carrier_contDiff (k : ℝ) : ContDiff ℝ (↑⊤) (carrier k)

noncomputable def NavierStokes.OscillatoryCurl.phaseNormal (Φ : ProblemStatement.PressureField) : ProblemStatement.VelocityField

Physical spatial phase normal, with time held fixed.

Equations

• NavierStokes.OscillatoryCurl.phaseNormal Φ z = NavierStokes.OscillatoryCurl.gradientLinear (fderiv ℝ (fun (y : NavierStokes.ProblemStatement.Space) => Φ (z.1, y)) z.2)

theorem NavierStokes.OscillatoryCurl.phaseNormal_eq_pressureGradient (Φ : ProblemStatement.PressureField) (z : ProblemStatement.SpaceTime) : phaseNormal Φ z = ProblemStatement.pressureGradient Φ z.1 z.2

noncomputable def NavierStokes.OscillatoryCurl.coefficient (Φ : ProblemStatement.PressureField) (a : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Coefficient, defined pointwise by normalCoefficient (phaseNormal Φ z) (a z).

Equations

• NavierStokes.OscillatoryCurl.coefficient Φ a z = NavierStokes.OscillatoryCurl.normalCoefficient (NavierStokes.OscillatoryCurl.phaseNormal Φ z) (a z)

noncomputable def NavierStokes.OscillatoryCurl.potential (k : ℝ) (Φ : ProblemStatement.PressureField) (a : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

-sin(k Φ) (n × a)/(k |n|²), expressed by scalar multiplication.

Equations

• NavierStokes.OscillatoryCurl.potential k Φ a z = NavierStokes.OscillatoryCurl.carrier k (Φ z) • NavierStokes.OscillatoryCurl.coefficient Φ a z

noncomputable def NavierStokes.OscillatoryCurl.wave (k : ℝ) (Φ : ProblemStatement.PressureField) (a : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Wave, given by SpatialCurl.spatialCurl (potential k Φ a).

Equations

• NavierStokes.OscillatoryCurl.wave k Φ a = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.OscillatoryCurl.potential k Φ a)

theorem NavierStokes.OscillatoryCurl.phaseNormal_contDiffOn {U : Set ProblemStatement.SpaceTime} {Φ : ProblemStatement.PressureField} (hU : IsOpen U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) : ContDiffOn ℝ (↑⊤) (phaseNormal Φ) U

theorem NavierStokes.OscillatoryCurl.coefficient_contDiffOn {U : Set ProblemStatement.SpaceTime} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} (hU : IsOpen U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ z ∈ U, phaseNormal Φ z ≠ 0) : ContDiffOn ℝ (↑⊤) (coefficient Φ a) U

theorem NavierStokes.OscillatoryCurl.potential_contDiffOn {U : Set ProblemStatement.SpaceTime} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} (k : ℝ) (hU : IsOpen U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ z ∈ U, phaseNormal Φ z ≠ 0) : ContDiffOn ℝ (↑⊤) (potential k Φ a) U

theorem NavierStokes.OscillatoryCurl.wave_eq {U : Set ProblemStatement.SpaceTime} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} {k : ℝ} (hk : k ≠ 0) (hU : IsOpen U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ z ∈ U, phaseNormal Φ z ≠ 0) (htangent : ∀ z ∈ U, inner ℝ (phaseNormal Φ z) (a z) = 0) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : wave k Φ a z = Real.cos (k * Φ z) • a z - (Real.sin (k * Φ z) / k) • SpatialCurl.spatialCurl (coefficient Φ a) z

Exact real realization: the derivative of the carrier yields the tangent cosine wave; every coefficient derivative remains in the displayed curl.

theorem NavierStokes.OscillatoryCurl.wave_contDiffOn {U : Set ProblemStatement.SpaceTime} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} (k : ℝ) (hU : IsOpen U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ z ∈ U, phaseNormal Φ z ≠ 0) : ContDiffOn ℝ (↑⊤) (wave k Φ a) U

theorem NavierStokes.OscillatoryCurl.wave_divergence_free {U : Set ProblemStatement.SpaceTime} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} (k : ℝ) (hU : IsOpen U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ z ∈ U, phaseNormal Φ z ≠ 0) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : ProblemStatement.spatialDivergence (wave k Φ a) z.1 z.2 = 0

Divergence vanishes for the full realized wave, including its remainder.

theorem NavierStokes.OscillatoryCurl.coefficient_support_subset (Φ : ProblemStatement.PressureField) (a : ProblemStatement.VelocityField) : Function.support (coefficient Φ a) ⊆ Function.support a

theorem NavierStokes.OscillatoryCurl.potential_tsupport_subset (k : ℝ) (Φ : ProblemStatement.PressureField) (a : ProblemStatement.VelocityField) : tsupport (potential k Φ a) ⊆ tsupport a

theorem NavierStokes.OscillatoryCurl.spatialCurl_tsupport_subset (A : ProblemStatement.VelocityField) : tsupport (SpatialCurl.spatialCurl A) ⊆ tsupport A

Spatial differentiation cannot create support outside the closed joint spacetime support, since vanishing on a joint neighborhood implies vanishing on the spatial slice.

theorem NavierStokes.OscillatoryCurl.wave_tsupport_subset (k : ℝ) (Φ : ProblemStatement.PressureField) (a : ProblemStatement.VelocityField) : tsupport (wave k Φ a) ⊆ tsupport a

theorem NavierStokes.OscillatoryCurl.wave_hasCompactSupport (k : ℝ) (Φ : ProblemStatement.PressureField) {a : ProblemStatement.VelocityField} (ha : HasCompactSupport a) : HasCompactSupport (wave k Φ a)

theorem NavierStokes.OscillatoryCurl.phaseNormal_periodic {times : Set ℝ} {Φ : ProblemStatement.PressureField} (hΦ : ProblemStatement.UnitSpatialPeriodsOn times Φ) : ProblemStatement.UnitSpatialPeriodsOn times (phaseNormal Φ)

theorem NavierStokes.OscillatoryCurl.coefficient_periodic {times : Set ℝ} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} (hn : ProblemStatement.UnitSpatialPeriodsOn times (phaseNormal Φ)) (ha : ProblemStatement.UnitSpatialPeriodsOn times a) : ProblemStatement.UnitSpatialPeriodsOn times (coefficient Φ a)

theorem NavierStokes.OscillatoryCurl.potential_periodic {times : Set ℝ} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} (k : ℝ) (hcarrier : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => Real.sin (k * Φ z)) (hn : ProblemStatement.UnitSpatialPeriodsOn times (phaseNormal Φ)) (ha : ProblemStatement.UnitSpatialPeriodsOn times a) : ProblemStatement.UnitSpatialPeriodsOn times (potential k Φ a)

It suffices for the sine carrier and the normal/amplitude data to be periodic; a real-valued phase itself may have nonzero winding.

theorem NavierStokes.OscillatoryCurl.wave_periodic {times : Set ℝ} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} (k : ℝ) (hcarrier : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => Real.sin (k * Φ z)) (hn : ProblemStatement.UnitSpatialPeriodsOn times (phaseNormal Φ)) (ha : ProblemStatement.UnitSpatialPeriodsOn times a) : ProblemStatement.UnitSpatialPeriodsOn times (wave k Φ a)

theorem NavierStokes.OscillatoryCurl.wave_periodic_of_phase {times : Set ℝ} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} (k : ℝ) (hΦ : ProblemStatement.UnitSpatialPeriodsOn times Φ) (ha : ProblemStatement.UnitSpatialPeriodsOn times a) : ProblemStatement.UnitSpatialPeriodsOn times (wave k Φ a)

noncomputable def NavierStokes.OscillatoryCurl.strippedRemainder (k : ℝ) (B : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

The coefficient remaining after removing the sine oscillation.

Equations

• NavierStokes.OscillatoryCurl.strippedRemainder k B z = (1 / k) • NavierStokes.SpatialCurl.spatialCurl B z

theorem NavierStokes.OscillatoryCurl.wave_eq_stripped {U : Set ProblemStatement.SpaceTime} {Φ : ProblemStatement.PressureField} {a : ProblemStatement.VelocityField} {k : ℝ} (hk : k ≠ 0) (hU : IsOpen U) (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ z ∈ U, phaseNormal Φ z ≠ 0) (htangent : ∀ z ∈ U, inner ℝ (phaseNormal Φ z) (a z) = 0) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) : wave k Φ a z = Real.cos (k * Φ z) • a z - Real.sin (k * Φ z) • strippedRemainder k (coefficient Φ a) z

theorem NavierStokes.OscillatoryCurl.strippedRemainder_jet_bound {U : Set ProblemStatement.SpaceTime} {B : ProblemStatement.VelocityField} (k : ℝ) (hU : IsOpen U) (hB : ContDiffOn ℝ (↑⊤) B U) {z : ProblemStatement.SpaceTime} (hz : z ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (strippedRemainder k B) z‖ ≤ ‖SpatialCurl.curlLinear ∘SL ResidualStability.spaceRestriction ProblemStatement.Space‖ / |k| * ‖iteratedFDeriv ℝ (m + 1) B z‖

One additional coefficient derivative and one inverse frequency, with no derivative of the oscillatory carrier hidden in the bound.

theorem NavierStokes.OscillatoryCurl.strippedRemainder_finiteJetBound {U : Set ProblemStatement.SpaceTime} {B : ProblemStatement.VelocityField} (k : ℝ) (hU : IsOpen U) (hB : ContDiffOn ℝ (↑⊤) B U) {m : ℕ} {C : ℝ} (hjet : JetBounds.FiniteJetBound (m + 1) B U C) : JetBounds.FiniteJetBound m (strippedRemainder k B) U (‖SpatialCurl.curlLinear ∘SL ResidualStability.spaceRestriction ProblemStatement.Space‖ / |k| * C)

Uniform slow jets of the actual phase geometry

The index type below carries the band, representative, and rounded frequency. It is not a differentiation variable. All derivatives are actual Fréchet derivatives in the slow variables (and, when present, the slot variable).

structure NavierStokes.PhaseJetBounds.Domain (ι : Type u_1) (E : Type u_2) [NormedAddCommGroup E] : Type (max u_1 u_2)

A family of open chart domains, with a slow scale at least one.

• scale : ι → ℝ

  Scale of Domain, of type ι → ℝ.

• carrier : ι → Set E

  Carrier of Domain, of type ι → Set E.

• isOpen (i : ι) : IsOpen (self.carrier i)
• one_le_scale (i : ι) : 1 ≤ self.scale i

structure NavierStokes.PhaseJetBounds.PolynomialJets {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (D : Domain ι E) (f : ι → E → F) : Prop

Every fixed finite collection of actual derivatives has one polynomial bound, uniform over all bands and charts in the index type.

• smooth (i : ι) : ContDiffOn ℝ (↑⊤) (f i) (D.carrier i)
• bound (N : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (m : ℕ), ∀ (i : ι), JetBounds.FiniteJetBound N (f i) (D.carrier i) (C * D.scale i ^ m)

theorem NavierStokes.PhaseJetBounds.PolynomialJets.congr {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} {f g : ι → E → F} (hf : PolynomialJets D f) (hfg : ∀ (i : ι), Set.EqOn (f i) (g i) (D.carrier i)) : PolynomialJets D g

theorem NavierStokes.PhaseJetBounds.PolynomialJets.const {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} (c : ι → F) {C : ℝ} {m : ℕ} (hC : 1 ≤ C) (hc : ∀ (i : ι), ‖c i‖ ≤ C * D.scale i ^ m) : PolynomialJets D fun (i : ι) (x : E) => c i

theorem NavierStokes.PhaseJetBounds.PolynomialJets.const_uniform {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} (c : ι → F) {C : ℝ} (hC : 1 ≤ C) (hc : ∀ (i : ι), ‖c i‖ ≤ C) : PolynomialJets D fun (i : ι) (x : E) => c i

theorem NavierStokes.PhaseJetBounds.PolynomialJets.const_fixed {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} (c : F) : PolynomialJets D fun (x : ι) (x_1 : E) => c

theorem NavierStokes.PhaseJetBounds.PolynomialJets.clm {ι : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : Domain ι E} {f : ι → E → F} (hf : PolynomialJets D f) (L : F →L[ℝ] G) : PolynomialJets D fun (i : ι) (x : E) => L (f i x)

theorem NavierStokes.PhaseJetBounds.PolynomialJets.add {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} {f g : ι → E → F} (hf : PolynomialJets D f) (hg : PolynomialJets D g) : PolynomialJets D fun (i : ι) (x : E) => f i x + g i x

theorem NavierStokes.PhaseJetBounds.PolynomialJets.neg {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} {f : ι → E → F} (hf : PolynomialJets D f) : PolynomialJets D fun (i : ι) (x : E) => -f i x

theorem NavierStokes.PhaseJetBounds.PolynomialJets.sub {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} {f g : ι → E → F} (hf : PolynomialJets D f) (hg : PolynomialJets D g) : PolynomialJets D fun (i : ι) (x : E) => f i x - g i x

theorem NavierStokes.PhaseJetBounds.PolynomialJets.pair {ι : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : Domain ι E} {f : ι → E → F} {g : ι → E → G} (hf : PolynomialJets D f) (hg : PolynomialJets D g) : PolynomialJets D fun (i : ι) (x : E) => (f i x, g i x)

theorem NavierStokes.PhaseJetBounds.PolynomialJets.bilinear {ι : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {D : Domain ι E} {f : ι → E → F} {g : ι → E → G} (hf : PolynomialJets D f) (hg : PolynomialJets D g) (B : F →L[ℝ] G →L[ℝ] H) : PolynomialJets D fun (i : ι) (x : E) => (B (f i x)) (g i x)

theorem NavierStokes.PhaseJetBounds.PolynomialJets.mul {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {f g : ι → E → ℝ} (hf : PolynomialJets D f) (hg : PolynomialJets D g) : PolynomialJets D fun (i : ι) (x : E) => f i x * g i x

theorem NavierStokes.PhaseJetBounds.PolynomialJets.smul {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} {f : ι → E → ℝ} {g : ι → E → F} (hf : PolynomialJets D f) (hg : PolynomialJets D g) : PolynomialJets D fun (i : ι) (x : E) => f i x • g i x

theorem NavierStokes.PhaseJetBounds.PolynomialJets.fderiv {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} {f : ι → E → F} (hf : PolynomialJets D f) : PolynomialJets D fun (i : ι) => _root_.fderiv ℝ (f i)

theorem NavierStokes.PhaseJetBounds.PolynomialJets.directional {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} {f : ι → E → F} (hf : PolynomialJets D f) (v : E) : PolynomialJets D fun (i : ι) (x : E) => (_root_.fderiv ℝ (f i) x) v

theorem NavierStokes.PhaseJetBounds.PolynomialJets.affine {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} (L : E →L[ℝ] F) (c : ι → F) {C : ℝ} {m : ℕ} (hC : 1 ≤ C) (hv : ∀ (i : ι), ∀ x ∈ D.carrier i, ‖L x + c i‖ ≤ C * D.scale i ^ m) : PolynomialJets D fun (i : ι) (x : E) => L x + c i

Affine coordinates have only a zeroth and first derivative.

theorem NavierStokes.PhaseJetBounds.norm_jet_comp_linear {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : F → G} {U : Set F} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (L : E →L[ℝ] F) {x : E} (hx : L x ∈ U) (n : ℕ) : ‖iteratedFDeriv ℝ n (f ∘ ⇑L) x‖ ≤ ‖iteratedFDeriv ℝ n f (L x)‖ * ‖L‖ ^ n

theorem NavierStokes.PhaseJetBounds.norm_jet_comp_affine {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : F → G} {U : Set F} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑⊤) f U) (L : E →L[ℝ] F) (c : F) {x : E} (hx : L x + c ∈ U) (n : ℕ) : ‖iteratedFDeriv ℝ n (fun (y : E) => f (L y + c)) x‖ ≤ ‖iteratedFDeriv ℝ n f (L x + c)‖ * ‖L‖ ^ n

Translations introduce no growth in higher-derivative norms.

theorem NavierStokes.PhaseJetBounds.PolynomialJets.precomp_affine {ι : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : Domain ι E} {D' : Domain ι F} {f : ι → F → G} (hf : PolynomialJets D' f) (L : E →L[ℝ] F) (c : ι → F) (hscale : ∀ (i : ι), D'.scale i = D.scale i) (hmap : ∀ (i : ι), ∀ x ∈ D.carrier i, L x + c i ∈ D'.carrier i) : PolynomialJets D fun (i : ι) (x : E) => f i (L x + c i)

theorem NavierStokes.PhaseJetBounds.compact_jet_bound {F : Type u_3} {G : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {g : F → G} {U K : Set F} (hU : IsOpen U) (hg : ContDiffOn ℝ (↑⊤) g U) (hK : IsCompact K) (hKU : K ⊆ U) (N : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ JetBounds.FiniteJetBound N g K C

theorem NavierStokes.PhaseJetBounds.PolynomialJets.compact_comp {ι : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {D : Domain ι E} {f : ι → E → F} (hf : PolynomialJets D f) {g : F → G} {U K : Set F} (hU : IsOpen U) (hg : ContDiffOn ℝ (↑⊤) g U) (hK : IsCompact K) (hKU : K ⊆ U) (hmap : ∀ (i : ι), Set.MapsTo (f i) (D.carrier i) K) : PolynomialJets D fun (i : ι) (x : E) => g (f i x)

The higher chain rule is quantitative: compactness is applied only to the fixed outer function, never to the varying band or to its derivatives.

theorem NavierStokes.PhaseJetBounds.PolynomialJets.inner {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {D : Domain ι E} {f g : ι → E → F} (hf : PolynomialJets D f) (hg : PolynomialJets D g) : PolynomialJets D fun (i : ι) (x : E) => Inner.inner ℝ (f i x) (g i x)

theorem NavierStokes.PhaseJetBounds.PolynomialJets.norm_sq {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {D : Domain ι E} {f : ι → E → F} (hf : PolynomialJets D f) : PolynomialJets D fun (i : ι) (x : E) => ‖f i x‖ ^ 2

theorem NavierStokes.PhaseJetBounds.PolynomialJets.pow {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {f : ι → E → ℝ} (hf : PolynomialJets D f) (n : ℕ) : PolynomialJets D fun (i : ι) (x : E) => f i x ^ n

theorem NavierStokes.PhaseJetBounds.PolynomialJets.div_const {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {f : ι → E → ℝ} (hf : PolynomialJets D f) (c : ℝ) : PolynomialJets D fun (i : ι) (x : E) => f i x / c

theorem NavierStokes.PhaseJetBounds.PolynomialJets.inv {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {f : ι → E → ℝ} (hf : PolynomialJets D f) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (i : ι), ∀ x ∈ D.carrier i, b ≤ |f i x|) (hupper : ∀ (i : ι), ∀ x ∈ D.carrier i, |f i x| ≤ M) : PolynomialJets D fun (i : ι) (x : E) => (f i x)⁻¹

Inversion is used only on a uniformly separated compact range.

@[reducible, inline]

abbrev NavierStokes.PhaseJetBounds.Plane : Type

Plane: an abbreviation for MovingFrameODE.Plane.

Equations

• NavierStokes.PhaseJetBounds.Plane = NavierStokes.MovingFrameODE.Plane

@[reducible, inline]

abbrev NavierStokes.PhaseJetBounds.Space : Type

Space: an abbreviation for MovingFrameODE.Space.

Equations

• NavierStokes.PhaseJetBounds.Space = NavierStokes.MovingFrameODE.Space

@[reducible, inline]

abbrev NavierStokes.PhaseJetBounds.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.PhaseJetBounds.Slow = NavierStokes.PhaseCalculus.Slow

def NavierStokes.PhaseJetBounds.regularNormals : Set Space

Regular normals, given by {n | MovingFrameODE.tail n ≠ 0}.

Equations

• NavierStokes.PhaseJetBounds.regularNormals = {n : NavierStokes.PhaseJetBounds.Space | NavierStokes.MovingFrameODE.tail n ≠ 0}

def NavierStokes.PhaseJetBounds.normalRange (b M : ℝ) : Set Space

Normal range, given by Metric.closedBall 0 M ∩ {n | b ≤ ‖MovingFrameODE.tail n‖}.

Equations

• NavierStokes.PhaseJetBounds.normalRange b M = Metric.closedBall 0 M ∩ {n : NavierStokes.PhaseJetBounds.Space | b ≤ ‖NavierStokes.MovingFrameODE.tail n‖}

theorem NavierStokes.PhaseJetBounds.regularNormals_isOpen : IsOpen regularNormals

theorem NavierStokes.PhaseJetBounds.normalRange_isCompact (b M : ℝ) : IsCompact (normalRange b M)

theorem NavierStokes.PhaseJetBounds.normalRange_regular {b M : ℝ} (hb : 0 < b) : normalRange b M ⊆ regularNormals

structure NavierStokes.PhaseJetBounds.NormalGeometryJets {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (D : Domain ι E) (n nDot : ι → E → Space) : Prop

All normalized geometric quantities needed in the moving-frame ODE. Their jets are conclusions of normalGeometry_jets, not assumptions there.

• scale : PolynomialJets D fun (i : ι) (x : E) => MovingFrameODE.normalScale (n i x)
• invScale : PolynomialJets D fun (i : ι) (x : E) => (MovingFrameODE.normalScale (n i x))⁻¹
• rho : PolynomialJets D fun (i : ι) (x : E) => MovingFrameODE.radialSlope (n i x)
• invDenom : PolynomialJets D fun (i : ι) (x : E) => (1 + MovingFrameODE.radialSlope (n i x) ^ 2)⁻¹
• K : PolynomialJets D fun (i : ι) (x : E) => MovingFrameODE.normalDirection (n i x)
• N : PolynomialJets D fun (i : ι) (x : E) => MovingFrameODE.quarterTurn (MovingFrameODE.normalDirection (n i x))
• betaDot : PolynomialJets D fun (i : ι) (x : E) => PhaseEstimates.scaleDerivative (n i x) (nDot i x)
• rhoDot : PolynomialJets D fun (i : ι) (x : E) => PhaseEstimates.slopeDerivative (n i x) (nDot i x)
• directionDot : PolynomialJets D fun (i : ι) (x : E) => PhaseEstimates.directionDerivative (n i x) (nDot i x)
• rotation : PolynomialJets D fun (i : ι) (x : E) => PhaseEstimates.angularVelocity (n i x) (nDot i x)

theorem NavierStokes.PhaseJetBounds.normalGeometry_jets {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {n nDot : ι → E → Space} (hn : PolynomialJets D n) (hd : PolynomialJets D nDot) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (i : ι), ∀ x ∈ D.carrier i, b ≤ ‖MovingFrameODE.tail (n i x)‖) (hupper : ∀ (i : ι), ∀ x ∈ D.carrier i, ‖n i x‖ ≤ M) : NormalGeometryJets D n nDot

theorem NavierStokes.PhaseJetBounds.polynomialJets_of_uniform {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι E} {f : ι → E → F} (hf : ∀ (i : ι), ContDiffOn ℝ (↑⊤) (f i) (D.carrier i)) (hbound : ∀ (N : ℕ), ∃ (C : ℝ), 1 ≤ C ∧ ∀ (i : ι), JetBounds.FiniteJetBound N (f i) (D.carrier i) C) : PolynomialJets D f

Uniform normalized base-field jets are a sufficient input. The bound is on the base field itself, before any normal or frame is constructed.

noncomputable def NavierStokes.PhaseJetBounds.Domain.slot {ι : Type u_1} (D : Domain ι Slow) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) : Domain ι (Slow × ℝ)

Slot, bundling scale, carrier, isOpen, one_le_scale.

Equations

• D.slot V hV = { scale := D.scale, carrier := fun (i : ι) => D.carrier i ×ˢ V i, isOpen := ⋯, one_le_scale := ⋯ }

theorem NavierStokes.PhaseJetBounds.PolynomialJets.lift_slot {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {D : Domain ι Slow} {f : ι → Slow → F} (hf : PolynomialJets D f) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) : PolynomialJets (D.slot V hV) fun (i : ι) (z : Slow × ℝ) => f i z.1

theorem NavierStokes.PhaseJetBounds.PolynomialJets.vec2 {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {f g : ι → E → ℝ} (hf : PolynomialJets D f) (hg : PolynomialJets D g) : PolynomialJets D fun (i : ι) (x : E) => !₂[f i x, g i x]

theorem NavierStokes.PhaseJetBounds.PolynomialJets.vec3 {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {f g h : ι → E → ℝ} (hf : PolynomialJets D f) (hg : PolynomialJets D g) (hh : PolynomialJets D h) : PolynomialJets D fun (i : ι) (x : E) => !₂[f i x, g i x, h i x]

theorem NavierStokes.PhaseJetBounds.explicitNormal_polynomial {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {ε p pz x0 R v FR GR FZ GZ : ι → E → ℝ} (hε : PolynomialJets D ε) (hp : PolynomialJets D p) (hpz : PolynomialJets D pz) (hx : PolynomialJets D x0) (hRi : PolynomialJets D fun (i : ι) (x : E) => (R i x)⁻¹) (hv : PolynomialJets D v) (hFR : PolynomialJets D FR) (hGR : PolynomialJets D GR) (hFZ : PolynomialJets D FZ) (hGZ : PolynomialJets D GZ) : PolynomialJets D fun (i : ι) (z : E) => PhaseEstimates.explicitNormal (ε i z) (p i z) (pz i z) (x0 i z) (R i z) (v i z) (FR i z) (GR i z) (FZ i z) (GZ i z)

The explicit normal has polynomial jets. No inverse power of epsilon occurs in this formula, although it occurs in the phase itself.

theorem NavierStokes.PhaseJetBounds.normalVelocity_polynomial {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {ε p pz FR GR FZ GZ : ι → E → ℝ} (hε : PolynomialJets D ε) (hp : PolynomialJets D p) (hpz : PolynomialJets D pz) (hFR : PolynomialJets D FR) (hGR : PolynomialJets D GR) (hFZ : PolynomialJets D FZ) (hGZ : PolynomialJets D GZ) : PolynomialJets D fun (i : ι) (z : E) => PhaseEstimates.normalVelocity (ε i z) (p i z) (pz i z) (FR i z) (GR i z) (FZ i z) (GZ i z)

structure NavierStokes.PhaseJetBounds.PhaseFamily (ι : Type u_2) : Type u_2

Discrete label data. In particular, p is held fixed when a jet is taken; it may be the nonzero rounded frequency from PhaseEstimates.

• epsilon : ι → ℝ

  Epsilon of PhaseFamily, of type ι → ℝ.

• p : ι → ℝ

  P of PhaseFamily, of type ι → ℝ.

• pz : ι → ℝ

  Pz of PhaseFamily, of type ι → ℝ.

• x0 : ι → ℝ

  X0 of PhaseFamily, of type ι → ℝ.

• theta : ι → ℝ

  Theta of PhaseFamily, of type ι → ℝ.

• F : ι → Slow → ℝ

  F of PhaseFamily, of type ι → Slow → ℝ.

• G : ι → Slow → ℝ

  Geometric data of PhaseFamily, of type ι → Slow → ℝ.

noncomputable def NavierStokes.PhaseJetBounds.PhaseFamily.normal {ι : Type u_1} (a : PhaseFamily ι) (i : ι) (z : Slow × ℝ) : Space

Normal, given by PhaseCalculus.phaseNormal (a.epsilon i) (a.p i) (a.pz i) (a.x0 i) (a.F i) (a.G i) (z.1, (a.theta i, z.2)).

Equations

• a.normal i z = NavierStokes.PhaseCalculus.phaseNormal (a.epsilon i) (a.p i) (a.pz i) (a.x0 i) (a.F i) (a.G i) (z.1, a.theta i, z.2)

noncomputable def NavierStokes.PhaseJetBounds.PhaseFamily.velocity {ι : Type u_1} (a : PhaseFamily ι) (i : ι) (z : Slow × ℝ) : Space

Velocity, given by PhaseCalculus.normalSlotDerivative (a.epsilon i) (a.p i) (a.pz i) (a.F i) (a.G i) z.1.

Equations

• a.velocity i z = NavierStokes.PhaseCalculus.normalSlotDerivative (a.epsilon i) (a.p i) (a.pz i) (a.F i) (a.G i) z.1

noncomputable def NavierStokes.PhaseJetBounds.PhaseFamily.shear {ι : Type u_1} (a : PhaseFamily ι) (i : ι) (z : Slow × ℝ) : Plane

Shear, given by PhaseEstimates.shearVector (a.F i) (a.G i) z.1.

Equations

• a.shear i z = NavierStokes.PhaseEstimates.shearVector (a.F i) (a.G i) z.1

theorem NavierStokes.PhaseJetBounds.PhaseFamily.polynomial_jets {ι : Type u_1} (a : PhaseFamily ι) (D : Domain ι Slow) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) (hF : PolynomialJets D a.F) (hG : PolynomialJets D a.G) {r M : ℝ} (hr : 0 < r) (hM : 1 ≤ M) (hconstant : ∀ (i : ι), |a.epsilon i| ≤ M ∧ |a.p i| ≤ M ∧ |a.pz i| ≤ M ∧ |a.x0 i| ≤ M) (heps : ∀ (i : ι), a.epsilon i ≠ 0) (hR : ∀ (i : ι), ∀ q ∈ D.carrier i, r ≤ |q.1| ∧ |q.1| ≤ M) (hslot : ∀ (i : ι), ∀ v ∈ V i, |v| ≤ M * D.scale i) : PolynomialJets (D.slot V hV) a.normal ∧ PolynomialJets (D.slot V hV) a.velocity ∧ PolynomialJets (D.slot V hV) a.shear

Actual phase-normal and shear jets derived from the base fields. The slot can have length of order S; the cylindrical radius stays in an annulus. No derivatives of the normal, frame, or ODE coefficients are inputs.

structure NavierStokes.PhaseJetBounds.FrameJets {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] (D : Domain ι (Q × ℝ)) (d : ι → PrimaryODE.FrameData Q) : Prop

Intermediate algebraic data used to assemble the defined modal coefficient. frameJets_ofNormalLocal proves these from phase-normal jets.

• beta : PolynomialJets D fun (i : ι) => (d i).beta
• betaDot : PolynomialJets D fun (i : ι) => (d i).betaDot
• rho : PolynomialJets D fun (i : ι) => (d i).rho
• rhoDot : PolynomialJets D fun (i : ι) => (d i).rhoDot
• rotation : PolynomialJets D fun (i : ι) => (d i).rotation
• F : PolynomialJets D fun (i : ι) => (d i).F
• shear : PolynomialJets D fun (i : ι) => (d i).shear
• K : PolynomialJets D fun (i : ι) (z : Q × ℝ) => ((d i).frame z) 0
• N : PolynomialJets D fun (i : ι) (z : Q × ℝ) => ((d i).frame z) 1
• invDenom : PolynomialJets D fun (i : ι) (z : Q × ℝ) => (1 + (d i).rho z ^ 2)⁻¹
• eigenvalue : PolynomialJets D fun (i : ι) => (d i).eigenvalue
• eigenvector : PolynomialJets D fun (i : ι) => (d i).eigenvector
• invEigenvector : PolynomialJets D fun (i : ι) (z : Q × ℝ) => ((d i).eigenvector z)⁻¹
• eigenRate : PolynomialJets D fun (i : ι) => (d i).eigenRate
• viscosity : PolynomialJets D fun (i : ι) => (d i).viscosity
• eigenvector_ne_zero (i : ι) (z : Q × ℝ) : z ∈ D.carrier i → (d i).eigenvector z ≠ 0

theorem NavierStokes.PhaseJetBounds.FrameJets.smoothOn {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : FrameJets D d) (i : ι) : (d i).SmoothOn (D.carrier i)

theorem NavierStokes.PhaseJetBounds.FrameJets.errorA {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : FrameJets D d) : PolynomialJets D fun (i : ι) => (d i).errorA

theorem NavierStokes.PhaseJetBounds.FrameJets.errorB {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : FrameJets D d) : PolynomialJets D fun (i : ι) => (d i).errorB

theorem NavierStokes.PhaseJetBounds.FrameJets.errorC {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : FrameJets D d) : PolynomialJets D fun (i : ι) => (d i).errorC

theorem NavierStokes.PhaseJetBounds.FrameJets.modal_errors {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : FrameJets D d) : (PolynomialJets D fun (i : ι) => (d i).error11) ∧ (PolynomialJets D fun (i : ι) => (d i).error12) ∧ (PolynomialJets D fun (i : ι) => (d i).error21) ∧ PolynomialJets D fun (i : ι) => (d i).error22

theorem NavierStokes.PhaseJetBounds.FrameJets.coefficient {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : FrameJets D d) (j : ℤ) : PolynomialJets D fun (i : ι) => (d i).coefficient j

theorem NavierStokes.PhaseJetBounds.FrameJets.forcing {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (h : FrameJets D d) {f : ι → Q × ℝ → Space} (hf : PolynomialJets D f) : PolynomialJets D fun (i : ι) => (d i).forcing (f i)

The actual projection and eigenbasis conversion of a supplied source preserve polynomial jets. A scalar weight on the source can be carried separately using linearity; no Gaussian source estimate is assumed here.

theorem NavierStokes.PhaseJetBounds.frameJets_ofNormalLocal {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {n nDot : ι → Q × ℝ → Space} {F : ι → Q × ℝ → ℝ} {g : ι → Q × ℝ → Plane} {lam h rate ν : ι → Q × ℝ → ℝ} (hn : PolynomialJets D n) (hd : PolynomialJets D nDot) (hF : PolynomialJets D F) (hg : PolynomialJets D g) (hlam : PolynomialJets D lam) (hh : PolynomialJets D h) (hrate : PolynomialJets D rate) (hν : PolynomialJets D ν) {b M bh H : ℝ} (hb : 0 < b) (hbh : 0 < bh) (hnlow : ∀ (i : ι), ∀ z ∈ D.carrier i, b ≤ ‖MovingFrameODE.tail (n i z)‖) (hnup : ∀ (i : ι), ∀ z ∈ D.carrier i, ‖n i z‖ ≤ M) (hhlow : ∀ (i : ι), ∀ z ∈ D.carrier i, bh ≤ |h i z|) (hhup : ∀ (i : ι), ∀ z ∈ D.carrier i, |h i z| ≤ H) : FrameJets D fun (i : ι) => PrimaryODE.FrameData.ofNormalLocal (n i) (nDot i) (F i) (g i) (lam i) (h i) (rate i) (ν i)

This theorem connects the proved normal estimates to the exact local frame used by PrimaryODE, including normal motion and viscosity.

theorem NavierStokes.PhaseJetBounds.PolynomialJets.parameter_bound {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ι → Q × ℝ → F} (hf : PolynomialJets D f) (N : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (m : ℕ), ∀ (i : ι) (p : Q) (v : ℝ), (p, v) ∈ D.carrier i → ∀ k ≤ N, ‖iteratedFDeriv ℝ k (fun (q : Q) => f i (q, v)) p‖ ≤ C * D.scale i ^ m

The form consumed by PrimaryODE.norm_iteratedFDeriv_solution_le_polynomial and WeightedODEJets: all parameter jets at fixed slot time share one constant and one power of S. The constant is independent of the slot time.

theorem NavierStokes.PhaseJetBounds.normal_range_of_reference_close {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {D : Domain ι E} {n : ι → E → Space} (B : ι → ℝ) (K : ι → Plane) (s δ : ι → E → ℝ) {b M : ℝ} (hb : 0 < b) (hM : 1 ≤ M) (hB : ∀ (i : ι), 2 * b ≤ B i ∧ B i ≤ M) (hK : ∀ (i : ι), ‖K i‖ = 1) (hs : ∀ (i : ι), ∀ z ∈ D.carrier i, |s i z| ≤ M) (hδ : ∀ (i : ι), ∀ z ∈ D.carrier i, δ i z ≤ B i / 2) (hclose : ∀ (i : ι), ∀ z ∈ D.carrier i, ‖n i z - MovingFrameODE.pack (B i * s i z) (B i • K i)‖ ≤ δ i z) : (∀ (i : ι), ∀ z ∈ D.carrier i, b ≤ ‖MovingFrameODE.tail (n i z)‖) ∧ ∀ (i : ι), ∀ z ∈ D.carrier i, ‖n i z‖ ≤ M ^ 2 + 3 * M

Quantitative compact-range inputs obtained from the actual normal comparison proved in PhaseEstimates, with no lower bound assumed on n.

theorem NavierStokes.PhaseJetBounds.PolynomialJets.radius {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} {s : ι → E → ℝ} (hs : PolynomialJets D s) {M : ℝ} (hbound : ∀ (i : ι), ∀ z ∈ D.carrier i, |s i z| ≤ M) : (PolynomialJets D fun (i : ι) (z : E) => √(1 + s i z ^ 2)) ∧ (PolynomialJets D fun (i : ι) (z : E) => (√(1 + s i z ^ 2))⁻¹) ∧ PolynomialJets D fun (i : ι) (z : E) => (1 + s i z ^ 2)⁻¹

theorem NavierStokes.PhaseJetBounds.radius_bounds (s : ℝ) : 1 ≤ √(1 + s ^ 2) ∧ √(1 + s ^ 2) ≤ 1 + |s|

theorem NavierStokes.PhaseJetBounds.reference_jets {ι : Type u_1} {Q : Type u_2} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} (lam c0 u ell : ι → ℝ) {M b : ℝ} (hM : 1 ≤ M) (hb : 0 < b) (hlam : ∀ (i : ι), |lam i| ≤ M) (hc : ∀ (i : ι), b ≤ |c0 i| ∧ |c0 i| ≤ M) (hu : ∀ (i : ι), |u i| ≤ M) (hrate : ∀ (i : ι), |u i / ell i| * D.scale i ≤ M) (hslot : ∀ (i : ι), ∀ z ∈ D.carrier i, |z.2| ≤ M * D.scale i) : (PolynomialJets D fun (i : ι) (z : Q × ℝ) => ViscousPropagator.referenceEigenvalue (lam i) (u i) (ell i) z.2) ∧ (PolynomialJets D fun (i : ι) (z : Q × ℝ) => PrimaryODE.referenceProfile (c0 i) (u i) (ell i) z.2) ∧ (PolynomialJets D fun (i : ι) (z : Q × ℝ) => PrimaryODE.referenceProfileRate (u i) (ell i) z.2) ∧ (∀ (i : ι), ∀ z ∈ D.carrier i, b ≤ |PrimaryODE.referenceProfile (c0 i) (u i) (ell i) z.2|) ∧ ∀ (i : ι), ∀ z ∈ D.carrier i, |PrimaryODE.referenceProfile (c0 i) (u i) (ell i) z.2| ≤ M * (1 + M + M ^ 2)

The reference eigenbasis is also derived from its explicit formula. The hypothesis on u/ell is the scale-normalized slot-length bound; all four parameters are frozen within each label.

noncomputable def NavierStokes.PhaseJetBounds.PhaseFamily.frameData {ι : Type u_1} (a : PhaseFamily ι) (lam c0 u ell ν : ι → ℝ) (i : ι) : PrimaryODE.FrameData Slow

The actual phase-derived frame with the explicit reference eigenbasis. Only the band/representative labels enter the frozen scalar choices.

Equations

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

theorem NavierStokes.PhaseJetBounds.PhaseFamily.frameData_jets_of_phase_comparison {ι : Type u_1} (a : PhaseFamily ι) (D : Domain ι Slow) (V : ι → Set ℝ) (hV : ∀ (i : ι), IsOpen (V i)) (lam c0 u ell ν B : ι → ℝ) (K : ι → Plane) (s δ : ι → Slow × ℝ → ℝ) (hF : PolynomialJets D a.F) (hG : PolynomialJets D a.G) {r b M : ℝ} (hr : 0 < r) (hb : 0 < b) (hM : 1 ≤ M) (hconstant : ∀ (i : ι), |a.epsilon i| ≤ M ∧ |a.p i| ≤ M ∧ |a.pz i| ≤ M ∧ |a.x0 i| ≤ M) (heps : ∀ (i : ι), a.epsilon i ≠ 0) (hR : ∀ (i : ι), ∀ q ∈ D.carrier i, r ≤ |q.1| ∧ |q.1| ≤ M) (hslot : ∀ (i : ι), ∀ v ∈ V i, |v| ≤ M * D.scale i) (hlam : ∀ (i : ι), |lam i| ≤ M) (hc : ∀ (i : ι), b ≤ |c0 i| ∧ |c0 i| ≤ M) (hu : ∀ (i : ι), |u i| ≤ M) (hrate : ∀ (i : ι), |u i / ell i| * D.scale i ≤ M) (hν : ∀ (i : ι), |ν i| ≤ M) (hB : ∀ (i : ι), 2 * b ≤ B i ∧ B i ≤ M) (hK : ∀ (i : ι), ‖K i‖ = 1) (hs : ∀ (i : ι), ∀ z ∈ (D.slot V hV).carrier i, |s i z| ≤ M) (hδ : ∀ (i : ι), ∀ z ∈ (D.slot V hV).carrier i, δ i z ≤ B i / 2) (hclose : ∀ (i : ι), ∀ z ∈ (D.slot V hV).carrier i, ‖a.normal i z - MovingFrameODE.pack (B i * s i z) (B i • K i)‖ ≤ δ i z) : FrameJets (D.slot V hV) (a.frameData lam c0 u ell ν)

Assembly from actual base jets, frozen representative bounds, and the zeroth-order phase comparison. That comparison is the conclusion of PhaseEstimates.actual_phase_estimates; smallness follows from its large-band theorems. The lower bound on the actual normal is derived inside this proof.

theorem NavierStokes.PhaseJetBounds.FrameJets.coefficient_parameter_bounds {ι : Type u_1} {Q : Type} [NormedAddCommGroup Q] [NormedSpace ℝ Q] {D : Domain ι (Q × ℝ)} {d : ι → PrimaryODE.FrameData Q} (hd : FrameJets D d) (j : ℤ) (N : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∃ (m : ℕ), ∀ (i : ι) (p : Q) (v : ℝ), (p, v) ∈ D.carrier i → ∀ k ≤ N, ‖iteratedFDeriv ℝ k (fun (q : Q) => (d i).coefficient j (q, v)) p‖ ≤ C * D.scale i ^ m

Direct output in the fixed-slot format used by the ODE jet theorem. The coefficient is the actual FrameData.coefficient, not a comparison ODE.

theorem NavierStokes.PhaseJetBounds.rounded_frequency_jets {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} (k target : ι → ℝ) {M : ℝ} (hM : 1 ≤ M) (hk : ∀ (i : ι), 1 ≤ k i) (ht : ∀ (i : ι), |target i| ≤ M) : PolynomialJets D fun (i : ι) (x : E) => PhaseEstimates.roundedFrequency (k i) (target i)

The genuine nonzero angular rounding preserves uniform boundedness. It is constant in the chart variables even when it jumps across labels.

theorem NavierStokes.PhaseJetBounds.band_viscosity_jets {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} (band : ι → ℕ) (h : ℝ) (hh : 0 ≤ h) : PolynomialJets D fun (i : ι) (x : E) => ChartScales.epsilon h (band i) * ↑(ChartScales.carrier h (band i)) ^ 2

With the actual carrier choice, the fundamental viscosity factor is a uniformly bounded label constant. Thus no factor k is lost in slow jets.

theorem NavierStokes.PhaseJetBounds.band_epsilon_jets {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} (band : ι → ℕ) (h : ℝ) (hh : 0 ≤ h) : PolynomialJets D fun (i : ι) (x : E) => ChartScales.epsilon h (band i)

theorem NavierStokes.PhaseJetBounds.band_rounded_frequency_jets {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {D : Domain ι E} (band : ι → ℕ) (h : ℝ) (target : ι → ℝ) {M : ℝ} (hM : 1 ≤ M) (ht : ∀ (i : ι), |target i| ≤ M) : PolynomialJets D fun (i : ι) (x : E) => PhaseEstimates.roundedFrequency (↑(ChartScales.carrier h (band i))) (target i)

noncomputable def NavierStokes.PhaseJetBounds.Domain.ofBands {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (band : ι → ℕ) (hband : ∀ (i : ι), 1 ≤ band i) (U : ι → Set E) (hU : ∀ (i : ι), IsOpen (U i)) : Domain ι E

A direct domain constructor with the manuscript's S(n)=n².

Equations

• NavierStokes.PhaseJetBounds.Domain.ofBands band hband U hU = { scale := fun (i : ι) => NavierStokes.ChartScales.S (band i), carrier := U, isOpen := hU, one_le_scale := ⋯ }

theorem NavierStokes.PhaseJetBounds.normalized_slot_rate_le {S ell u c M : ℝ} (hS : 0 < S) (hc : 0 < c) (hell : c * S ≤ ell) (hu : |u| ≤ M) : |u / ell| * S ≤ M / c

The reference logarithmic-rate input follows from a lower slot-length bound. In particular ChartScales.slotLength_bounds gives c=2r₀.

@[reducible, inline]

abbrev NavierStokes.CurlClassBounds.RealVector : Type

Real vector: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.CurlClassBounds.RealVector = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.CurlClassBounds.ComplexVector : Type

Complex vector: an abbreviation for HarmonicCalculus.ComplexVector.

Equations

• NavierStokes.CurlClassBounds.ComplexVector = NavierStokes.HarmonicCalculus.ComplexVector

theorem NavierStokes.CurlClassBounds.class_congr {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (hfg : ∀ (n : ℕ), Set.EqOn (f n) (g n) s.domain) : WeightedClasses.MemClass s w α g

theorem NavierStokes.CurlClassBounds.class_neg {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => -f n x

theorem NavierStokes.CurlClassBounds.class_sub {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f g : ℕ → D → E} (hf : WeightedClasses.MemClass s w α f) (hg : WeightedClasses.MemClass s w α g) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => f n x - g n x

theorem NavierStokes.CurlClassBounds.class_component {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {a : ℕ → D → ComplexVector} (ha : WeightedClasses.MemClass s w α a) (i : Fin 3) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => a n x i

theorem NavierStokes.CurlClassBounds.class_vector {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {a : ℕ → D → ComplexVector} (ha : ∀ (i : Fin 3), WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => a n x i) : WeightedClasses.MemClass s w α a

theorem NavierStokes.CurlClassBounds.class_along {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {V : ℕ → D → D} {f : ℕ → D → E} (hV : WeightedClasses.UnweightedClass s β V) (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass s w (α + β) fun (n : ℕ) => HarmonicCalculus.along (V n) (f n)

A genuine directional derivative consumes the class of its vector field.

theorem NavierStokes.CurlClassBounds.class_mul_real {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α β : ℝ} {r : ℕ → D → ℝ} {f : ℕ → D → E} (hr : WeightedClasses.UnweightedClass s β r) (hf : WeightedClasses.MemClass s w α f) : WeightedClasses.MemClass s w (β + α) fun (n : ℕ) (x : D) => r n x • f n x

theorem NavierStokes.CurlClassBounds.class_const_complex {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {f : ℕ → D → ComplexVector} (hf : WeightedClasses.MemClass s w α f) (c : ℂ) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => c • f n x

noncomputable def NavierStokes.CurlClassBounds.phaseDomain {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) : PhaseJetBounds.Domain ℕ D

The phase-jet domain corresponding to the actual strip data.

Equations

• NavierStokes.CurlClassBounds.phaseDomain s = { scale := s.slow, carrier := fun (x : ℕ) => s.domain, isOpen := ⋯, one_le_scale := ⋯ }

theorem NavierStokes.CurlClassBounds.polynomialJets_unweighted {D : Type u_1} {E : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {s : WeightedClasses.StripData D} {f : ℕ → D → E} (hf : PhaseJetBounds.PolynomialJets (phaseDomain s) f) : WeightedClasses.UnweightedClass s 0 f

noncomputable def NavierStokes.CurlClassBounds.complexify : RealVector →L[ℝ] ComplexVector

Real vectors embedded coordinatewise in the complex coefficient space.

Equations

• NavierStokes.CurlClassBounds.complexify = ContinuousLinearMap.pi fun (i : Fin 3) => Complex.ofRealCLM ∘SL EuclideanSpace.proj i

@[simp]

theorem NavierStokes.CurlClassBounds.complexify_apply (a : RealVector) (i : Fin 3) : complexify a i = ↑(a.ofLp i)

noncomputable def NavierStokes.CurlClassBounds.complexCrossLinear : ComplexVector →L[ℝ] ComplexVector →L[ℝ] ComplexVector

Complex cross linear as an element of ComplexVector →L[ℝ] ComplexVector →L[ℝ] ComplexVector.

Equations

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

noncomputable def NavierStokes.CurlClassBounds.normalCross (n : RealVector) (a : ComplexVector) : ComplexVector

Normal cross, given by complexCrossLinear (complexify n) a.

Equations

• NavierStokes.CurlClassBounds.normalCross n a = (NavierStokes.CurlClassBounds.complexCrossLinear (NavierStokes.CurlClassBounds.complexify n)) a

theorem NavierStokes.CurlClassBounds.normalCross_apply (n : RealVector) (a : ComplexVector) : normalCross n a = ↑(n.ofLp 1) • a 2 • Pi.single 0 1 - ↑(n.ofLp 2) • a 1 • Pi.single 0 1 + ↑(n.ofLp 2) • a 0 • Pi.single 1 1 - ↑(n.ofLp 0) • a 2 • Pi.single 1 1 + ↑(n.ofLp 0) • a 1 • Pi.single 2 1 - ↑(n.ofLp 1) • a 0 • Pi.single 2 1

@[simp]

theorem NavierStokes.CurlClassBounds.normalCross_zero (n : RealVector) (a : ComplexVector) : normalCross n a 0 = ↑(n.ofLp 1) * a 2 - ↑(n.ofLp 2) * a 1

@[simp]

theorem NavierStokes.CurlClassBounds.normalCross_one (n : RealVector) (a : ComplexVector) : normalCross n a 1 = ↑(n.ofLp 2) * a 0 - ↑(n.ofLp 0) * a 2

@[simp]

theorem NavierStokes.CurlClassBounds.normalCross_two (n : RealVector) (a : ComplexVector) : normalCross n a 2 = ↑(n.ofLp 0) * a 1 - ↑(n.ofLp 1) * a 0

theorem NavierStokes.CurlClassBounds.normalCross_smul (n : RealVector) (a : ComplexVector) (c : ℂ) : normalCross n (c • a) = c • normalCross n a

theorem NavierStokes.CurlClassBounds.normalCross_real_smul (n : RealVector) (a : ComplexVector) (c : ℝ) : normalCross n (c • a) = c • normalCross n a

theorem NavierStokes.CurlClassBounds.normalCross_triple (n : RealVector) (a : ComplexVector) : normalCross n (normalCross n a) = HarmonicCalculus.normalDot n a • complexify n - ‖n‖ ^ 2 • a

noncomputable def NavierStokes.CurlClassBounds.normalCoefficient (n : RealVector) (a : ComplexVector) : ComplexVector

The actual coefficient in the vector potential (30).

Equations

• NavierStokes.CurlClassBounds.normalCoefficient n a = (‖n‖ ^ 2)⁻¹ • NavierStokes.CurlClassBounds.normalCross n a

theorem NavierStokes.CurlClassBounds.normalCross_normalCoefficient {n : RealVector} {a : ComplexVector} (hn : n ≠ 0) (ha : HarmonicCalculus.normalDot n a = 0) : normalCross n (normalCoefficient n a) = -a

theorem NavierStokes.CurlClassBounds.normalInverse_unweighted {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {N : ℕ → D → RealVector} (hN : PhaseJetBounds.PolynomialJets (phaseDomain s) N) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖N n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖N n x‖ ≤ M) : WeightedClasses.UnweightedClass s 0 fun (n : ℕ) (x : D) => (‖N n x‖ ^ 2)⁻¹

The inverse-square normalization is derived from normal jets and a separated bounded range. It is not an assumed coefficient estimate.

theorem NavierStokes.CurlClassBounds.normalCoefficient_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α : ℝ} {N : ℕ → D → RealVector} {a : ℕ → D → ComplexVector} (hN : PhaseJetBounds.PolynomialJets (phaseDomain s) N) (ha : WeightedClasses.MemClass s w α a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖N n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖N n x‖ ≤ M) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : D) => normalCoefficient (N n x) (a n x)

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

Actual cylindrical curl, including the frame connection in its axial component.

Equations

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

theorem NavierStokes.CurlClassBounds.cylindricalCurl_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} {R : D → ℝ} {Vr Vθ Vz : ℕ → D → D} {a : ℕ → D → ComplexVector} (ha : WeightedClasses.MemClass s w α a) (hκ : 0 ≤ κ) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hθ : WeightedClasses.UnweightedClass s 0 Vθ) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) : WeightedClasses.MemClass s w (α - κ) fun (n : ℕ) => cylindricalCurl R (Vr n) (Vθ n) (Vz n) (a n)

theorem NavierStokes.CurlClassBounds.strippedDivergence_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} {R : D → ℝ} {Vr Vz : ℕ → D → D} {a : ℕ → D → ComplexVector} (ha : WeightedClasses.MemClass s w α a) (hκ : 0 ≤ κ) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) : WeightedClasses.MemClass s w (α - κ) fun (n : ℕ) => HarmonicCalculus.strippedDivergence R (Vr n) (Vz n) (a n)

noncomputable def NavierStokes.CurlClassBounds.curlRemainder {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) (R : D → ℝ) (Vr Vθ Vz : D → D) (B : D → ComplexVector) (x : D) : ComplexVector

The inverse frequency is the only band factor in the stripped curl error.

Equations

• NavierStokes.CurlClassBounds.curlRemainder K R Vr Vθ Vz B x = (1 / K) • Complex.I • NavierStokes.CurlClassBounds.cylindricalCurl R Vr Vθ Vz B x

theorem NavierStokes.CurlClassBounds.curlRemainder_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} {R : D → ℝ} {Vr Vθ Vz : ℕ → D → D} {K : ℕ → ℝ} {B : ℕ → D → ComplexVector} (hB : WeightedClasses.MemClass s w α B) (hκ : 0 ≤ κ) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hθ : WeightedClasses.UnweightedClass s 0 Vθ) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / K n) : WeightedClasses.MemClass s w (α + 1 / 2 - κ) fun (n : ℕ) => curlRemainder (K n) R (Vr n) (Vθ n) (Vz n) (B n)

theorem NavierStokes.CurlClassBounds.normalCurlRemainder_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} {R : D → ℝ} {Vr Vθ Vz : ℕ → D → D} {K : ℕ → ℝ} {N : ℕ → D → RealVector} {a : ℕ → D → ComplexVector} (hN : PhaseJetBounds.PolynomialJets (phaseDomain s) N) (ha : WeightedClasses.MemClass s w α a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖N n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖N n x‖ ≤ M) (hκ : 0 ≤ κ) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hθ : WeightedClasses.UnweightedClass s 0 Vθ) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / K n) : WeightedClasses.MemClass s w (α + 1 / 2 - κ) fun (n : ℕ) => curlRemainder (K n) R (Vr n) (Vθ n) (Vz n) fun (x : D) => normalCoefficient (N n x) (a n x)

The all-jet estimate is derived for the actual normalized vector potential.

noncomputable def NavierStokes.CurlClassBounds.carrierFrequency {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (n : ℕ) : ℝ

Carrier frequency, given by Scaling.carrierFrequency (s.epsilon n).

Equations

• NavierStokes.CurlClassBounds.carrierFrequency s n = ↑(NavierStokes.Scaling.carrierFrequency (s.epsilon n))

theorem NavierStokes.CurlClassBounds.carrierFrequency_pos {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (n : ℕ) : 0 < carrierFrequency s n

theorem NavierStokes.CurlClassBounds.harmonic_inverse_bandBound {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (j : ℕ → ℤ) (hj : ∀ (n : ℕ), j n ≠ 0) : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / (carrierFrequency s n * ↑(j n))

The rounded frequency itself supplies the half-power gain, uniformly in any nonzero integer harmonic.

theorem NavierStokes.CurlClassBounds.graphVector_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {κ : ℝ} {ρ : D → ℝ} {M : ℕ → ℝ} (hρ : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) => ρ) (hM : WeightedClasses.BandBound s (-κ) M) (hκ : 0 ≤ κ) (e v : D) : WeightedClasses.UnweightedClass s (-κ) fun (n : ℕ) (x : D) => e + M n • ρ x • v

theorem NavierStokes.CurlClassBounds.axialVector_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (z : D) : WeightedClasses.UnweightedClass s 1 fun (n : ℕ) (x : D) => s.epsilon n • z

theorem NavierStokes.CurlClassBounds.cylindricalCurl_contDiffOn {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) {R : D → ℝ} {Vr Vθ Vz : D → D} {B : D → ComplexVector} (hR : ContDiffOn ℝ (↑⊤) (fun (x : D) => (R x)⁻¹) U) (hr : ContDiffOn ℝ (↑⊤) Vr U) (hθ : ContDiffOn ℝ (↑⊤) Vθ U) (hz : ContDiffOn ℝ (↑⊤) Vz U) (hB : ContDiffOn ℝ (↑⊤) B U) : ContDiffOn ℝ (↑⊤) (cylindricalCurl R Vr Vθ Vz B) U

theorem NavierStokes.CurlClassBounds.cylindricalCurl_vectorMode {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (K : ℝ) {Φ : D → ℝ} {B : D → ComplexVector} {x : D} (hΦ : DifferentiableAt ℝ Φ x) (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => B y i) x) : cylindricalCurl R Vr Vθ Vz (HarmonicCalculus.vectorMode K Φ B) x = fun (i : Fin 3) => (cylindricalCurl R Vr Vθ Vz B x i + HarmonicCalculus.phaseFactor K * normalCross (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (B x) i) * HarmonicCalculus.carrier K Φ x

Every coefficient derivative and cylindrical connection survives stripping.

theorem NavierStokes.CurlClassBounds.cylindricalCurl_const_smul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (c : ℂ) {B : D → ComplexVector} {x : D} (hB : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D) => B y i) x) : cylindricalCurl R Vr Vθ Vz (fun (y : D) => c • B y) x = c • cylindricalCurl R Vr Vθ Vz B x

structure NavierStokes.CurlClassBounds.CylindricalGeometry {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (U : Set D) (R : D → ℝ) (Vr Vθ Vz : D → D) : Prop

Primitive geometric identities for genuine cylindrical graph directions. The bracket hypotheses concern derivatives of the direction fields themselves.

• isOpen : IsOpen U
• radius_smooth : ContDiffOn ℝ (↑⊤) R U
• radius_ne (x : D) : x ∈ U → R x ≠ 0
• radial_smooth : ContDiffOn ℝ (↑⊤) Vr U
• angular_smooth : ContDiffOn ℝ (↑⊤) Vθ U
• axial_smooth : ContDiffOn ℝ (↑⊤) Vz U
• radial_radius (x : D) : x ∈ U → HarmonicCalculus.along Vr R x = 1
• angular_radius (x : D) : x ∈ U → HarmonicCalculus.along Vθ R x = 0
• axial_radius (x : D) : x ∈ U → HarmonicCalculus.along Vz R x = 0
• radial_angular (x : D) : x ∈ U → (fderiv ℝ Vθ x) (Vr x) = (fderiv ℝ Vr x) (Vθ x)
• radial_axial (x : D) : x ∈ U → (fderiv ℝ Vz x) (Vr x) = (fderiv ℝ Vr x) (Vz x)
• angular_axial (x : D) : x ∈ U → (fderiv ℝ Vz x) (Vθ x) = (fderiv ℝ Vθ x) (Vz x)

theorem NavierStokes.CurlClassBounds.along_commute {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : D → F} {V W : D → D} {x : D} (hf : ContDiffAt ℝ (↑⊤) f x) (hV : DifferentiableAt ℝ V x) (hW : DifferentiableAt ℝ W x) (hbracket : (fderiv ℝ W x) (V x) = (fderiv ℝ V x) (W x)) : HarmonicCalculus.along V (HarmonicCalculus.along W f) x = HarmonicCalculus.along W (HarmonicCalculus.along V f) x

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

theorem NavierStokes.CurlClassBounds.along_real_smul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (V : D → D) {r : D → ℝ} {f : D → ℂ} {x : D} (hr : DifferentiableAt ℝ r x) (hf : DifferentiableAt ℝ f x) : HarmonicCalculus.along V (fun (y : D) => r y • f y) x = HarmonicCalculus.along V r x • f x + r x • HarmonicCalculus.along V f x

theorem NavierStokes.CurlClassBounds.along_inv {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (V : D → D) {R : D → ℝ} {x : D} (hR : DifferentiableAt ℝ R x) (hne : R x ≠ 0) : HarmonicCalculus.along V (fun (y : D) => (R y)⁻¹) x = -(R x ^ 2)⁻¹ * HarmonicCalculus.along V R x

theorem NavierStokes.CurlClassBounds.divergence_curl_zero {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vθ Vz : D → D} (G : CylindricalGeometry U R Vr Vθ Vz) {B : D → ComplexVector} (hB : ContDiffOn ℝ (↑⊤) B U) {x : D} (hx : x ∈ U) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (cylindricalCurl R Vr Vθ Vz B) x = 0

Divergence of the actual cylindrical curl is zero, including its frame term.

noncomputable def NavierStokes.CurlClassBounds.radialField {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] (K : ℝ → ℝ) (v : A) (x : ℝ × A) : ℝ × A

Radial field, given by (1, K x.1 • v).

Equations

• NavierStokes.CurlClassBounds.radialField K v x = (1, K x.1 • v)

theorem NavierStokes.CurlClassBounds.radialField_aux_derivative {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] {K : ℝ → ℝ} (v w : A) {x : ℝ × A} (hK : DifferentiableAt ℝ K x.1) : (fderiv ℝ (radialField K v) x) (0, w) = 0

theorem NavierStokes.CurlClassBounds.explicitGraph_geometry {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] {U : Set (ℝ × A)} (hU : IsOpen U) {K : ℝ → ℝ} (v θ z : A) (hK : ∀ x ∈ U, ContDiffAt ℝ (↑⊤) K x.1) (hR : ∀ x ∈ U, x.1 ≠ 0) : CylindricalGeometry U Prod.fst (radialField K v) (fun (x : ℝ × A) => (0, θ)) fun (x : ℝ × A) => (0, z)

Concrete graph directions commute because their radial coefficient only depends on the radius. No operator commutation is assumed in this constructor.

theorem NavierStokes.CurlClassBounds.phaseNormal_contDiffOn {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vθ Vz : D → D} (G : CylindricalGeometry U R Vr Vθ Vz) {Φ : D → ℝ} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) : ContDiffOn ℝ (↑⊤) (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ) U

theorem NavierStokes.CurlClassBounds.normalCoefficient_contDiffOn {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {N : D → RealVector} {a : D → ComplexVector} (hN : ContDiffOn ℝ (↑⊤) N U) (ha : ContDiffOn ℝ (↑⊤) a U) (hne : ∀ x ∈ U, N x ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (x : D) => normalCoefficient (N x) (a x)) U

noncomputable def NavierStokes.CurlClassBounds.coefficient {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (Φ : D → ℝ) (a : D → ComplexVector) (x : D) : ComplexVector

Coefficient, given by normalCoefficient (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (a x).

Equations

• NavierStokes.CurlClassBounds.coefficient R Vr Vθ Vz Φ a x = NavierStokes.CurlClassBounds.normalCoefficient (NavierStokes.HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (a x)

noncomputable def NavierStokes.CurlClassBounds.inverseCarrier (K : ℝ) : ℂ

Inverse carrier, given by Complex.I / (K : ℂ).

Equations

• NavierStokes.CurlClassBounds.inverseCarrier K = Complex.I / ↑K

theorem NavierStokes.CurlClassBounds.inverseCarrier_phaseFactor {K : ℝ} (hK : K ≠ 0) : inverseCarrier K * HarmonicCalculus.phaseFactor K = -1

theorem NavierStokes.CurlClassBounds.curlRemainder_eq {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) (R : D → ℝ) (Vr Vθ Vz : D → D) (B : D → ComplexVector) (x : D) : curlRemainder K R Vr Vθ Vz B x = inverseCarrier K • cylindricalCurl R Vr Vθ Vz B x

noncomputable def NavierStokes.CurlClassBounds.vectorPotential {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) (R : D → ℝ) (Vr Vθ Vz : D → D) (Φ : D → ℝ) (a : D → ComplexVector) : D → ComplexVector

Vector potential, given by HarmonicCalculus.vectorMode K Φ (fun x => inverseCarrier K • coefficient R Vr Vθ Vz Φ a x).

Equations

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

noncomputable def NavierStokes.CurlClassBounds.realizedCoefficient {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) (R : D → ℝ) (Vr Vθ Vz : D → D) (Φ : D → ℝ) (a : D → ComplexVector) (x : D) : ComplexVector

Realized coefficient, given by a x + curlRemainder K R Vr Vθ Vz (coefficient R Vr Vθ Vz Φ a) x.

Equations

• NavierStokes.CurlClassBounds.realizedCoefficient K R Vr Vθ Vz Φ a x = a x + NavierStokes.CurlClassBounds.curlRemainder K R Vr Vθ Vz (NavierStokes.CurlClassBounds.coefficient R Vr Vθ Vz Φ a) x

theorem NavierStokes.CurlClassBounds.vectorPotential_contDiffOn {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vθ Vz : D → D} (G : CylindricalGeometry U R Vr Vθ Vz) (K : ℝ) {Φ : D → ℝ} {a : D → ComplexVector} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ x ∈ U, HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x ≠ 0) : ContDiffOn ℝ (↑⊤) (vectorPotential K R Vr Vθ Vz Φ a) U

theorem NavierStokes.CurlClassBounds.cylindricalCurl_vectorPotential {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vθ Vz : D → D} (G : CylindricalGeometry U R Vr Vθ Vz) {K : ℝ} (hK : K ≠ 0) {Φ : D → ℝ} {a : D → ComplexVector} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ x ∈ U, HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x ≠ 0) (ht : ∀ x ∈ U, HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (a x) = 0) {x : D} (hx : x ∈ U) : cylindricalCurl R Vr Vθ Vz (vectorPotential K R Vr Vθ Vz Φ a) x = HarmonicCalculus.vectorMode K Φ (realizedCoefficient K R Vr Vθ Vz Φ a) x

Formula (30): the actual curl of the vector potential equals the tangent harmonic plus exactly the displayed coefficient-derivative remainder.

theorem NavierStokes.CurlClassBounds.cylindricalDivergence_congr {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (hU : IsOpen U) (R : D → ℝ) (Vr Vθ Vz : D → D) {a b : D → ComplexVector} (hab : Set.EqOn a b U) {x : D} (hx : x ∈ U) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz a x = HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz b x

theorem NavierStokes.CurlClassBounds.realizedCoefficient_divergence {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {R : D → ℝ} {Vr Vθ Vz : D → D} (G : CylindricalGeometry U R Vr Vθ Vz) {K : ℝ} (hK : K ≠ 0) {Φ : D → ℝ} {a : D → ComplexVector} (hΦ : ContDiffOn ℝ (↑⊤) Φ U) (ha : ContDiffOn ℝ (↑⊤) a U) (hn : ∀ x ∈ U, HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x ≠ 0) (ht : ∀ x ∈ U, HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R Vr Vθ Vz Φ x) (a x) = 0) {x : D} (hx : x ∈ U) : HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (HarmonicCalculus.vectorMode K Φ (realizedCoefficient K R Vr Vθ Vz Φ a)) x = 0

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

Solving the actual harmonic divergence identity gives the same inverse carrier as in the curl remainder. This equality includes normal derivatives when differentiated; there is no pointwise-only estimate here.

theorem NavierStokes.CurlClassBounds.longitudinal_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} {R : D → ℝ} {Vr Vθ Vz : ℕ → D → D} {K : ℕ → ℝ} {Φ : ℕ → D → ℝ} {a : ℕ → D → ComplexVector} (ha : WeightedClasses.MemClass s w α a) (hκ : 0 ≤ κ) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) (hK : ∀ (n : ℕ), K n ≠ 0) (hfreq : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / K n) (hΦ : ∀ (n : ℕ), DifferentiableOn ℝ (Φ n) s.domain) (hθ : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.along (Vθ n) (fun (y : D) => a n y 1) x = 0) (hdiv : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.cylindricalDivergence R (Vr n) (Vθ n) (Vz n) (HarmonicCalculus.vectorMode (K n) (Φ n) (a n)) x = 0) : WeightedClasses.MemClass s w (α + 1 / 2 - κ) fun (n : ℕ) (x : D) => HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n) x) (a n x)

Actual all-order longitudinal contraction bounds from harmonic solenoidality and primitive coefficient/direction classes.

theorem NavierStokes.CurlClassBounds.longitudinal_from_curl_class {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {w : ℕ → D → ℝ} {α κ : ℝ} {R : D → ℝ} {Vr Vθ Vz : ℕ → D → D} {K : ℕ → ℝ} {Φ : ℕ → D → ℝ} {a : ℕ → D → ComplexVector} (ha : WeightedClasses.MemClass s w α a) (hκ : 0 ≤ κ) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) (hK : ∀ (n : ℕ), K n ≠ 0) (hfreq : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / K n) (hΦ : ∀ (n : ℕ), DifferentiableOn ℝ (Φ n) s.domain) (hθ : ∀ (n : ℕ), ∀ x ∈ s.domain, HarmonicCalculus.along (Vθ n) (fun (y : D) => a n y 1) x = 0) (G : ∀ (n : ℕ), CylindricalGeometry s.domain R (Vr n) (Vθ n) (Vz n)) (A : ℕ → D → ComplexVector) (hA : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (A n) s.domain) (hreal : ∀ (n : ℕ), Set.EqOn (HarmonicCalculus.vectorMode (K n) (Φ n) (a n)) (cylindricalCurl R (Vr n) (Vθ n) (Vz n) (A n)) s.domain) : WeightedClasses.MemClass s w (α + 1 / 2 - κ) fun (n : ℕ) (x : D) => HarmonicCalculus.normalDot (HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n) x) (a n x)

The divergence premise is discharged by a genuine smooth vector potential. Equality is required on the open strip so all derivatives transfer.

theorem NavierStokes.CurlClassBounds.curlRemainder_waveClass {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {R : D → ℝ} {Vr Vθ Vz : ℕ → D → D} {K : ℕ → ℝ} {Φ : ℕ → D → ℝ} {a : ℕ → D → ComplexVector} (hN : PhaseJetBounds.PolynomialJets (phaseDomain s) fun (n : ℕ) => HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n)) (ha : WeightedClasses.WaveClass s P α a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n) x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n) x‖ ≤ M) (hκ : 0 ≤ κ) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hθ : WeightedClasses.UnweightedClass s 0 Vθ) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / K n) : WeightedClasses.WaveClass s P (α + 1 / 2 - κ) fun (n : ℕ) => curlRemainder (K n) R (Vr n) (Vθ n) (Vz n) (coefficient R (Vr n) (Vθ n) (Vz n) (Φ n) (a n))

Lemma 9.2's curl remainder, with the original wave weight unchanged.

theorem NavierStokes.CurlClassBounds.realizedCoefficient_waveClass {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {P : ℕ → D → ℝ} {α κ : ℝ} {R : D → ℝ} {Vr Vθ Vz : ℕ → D → D} {K : ℕ → ℝ} {Φ : ℕ → D → ℝ} {a : ℕ → D → ComplexVector} (hN : PhaseJetBounds.PolynomialJets (phaseDomain s) fun (n : ℕ) => HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n)) (ha : WeightedClasses.WaveClass s P α a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n) x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖HarmonicCalculus.phaseNormal R (Vr n) (Vθ n) (Vz n) (Φ n) x‖ ≤ M) (hκ : 0 ≤ κ) (hκhalf : κ ≤ 1 / 2) (hr : WeightedClasses.UnweightedClass s (-κ) Vr) (hθ : WeightedClasses.UnweightedClass s 0 Vθ) (hz : WeightedClasses.UnweightedClass s 1 Vz) (hR : WeightedClasses.UnweightedClass s 0 fun (x : ℕ) (x_1 : D) => (R x_1)⁻¹) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / K n) : WeightedClasses.WaveClass s P α fun (n : ℕ) => realizedCoefficient (K n) R (Vr n) (Vθ n) (Vz n) (Φ n) (a n)

theorem NavierStokes.CurlClassBounds.coefficient_tsupport_subset {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (Φ : D → ℝ) (a : D → ComplexVector) : tsupport (coefficient R Vr Vθ Vz Φ a) ⊆ tsupport a

theorem NavierStokes.CurlClassBounds.cylindricalCurl_tsupport_subset {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (R : D → ℝ) (Vr Vθ Vz : D → D) (B : D → ComplexVector) : tsupport (cylindricalCurl R Vr Vθ Vz B) ⊆ tsupport B

theorem NavierStokes.CurlClassBounds.vectorPotential_tsupport_subset {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) (R : D → ℝ) (Vr Vθ Vz : D → D) (Φ : D → ℝ) (a : D → ComplexVector) : tsupport (vectorPotential K R Vr Vθ Vz Φ a) ⊆ tsupport a

theorem NavierStokes.CurlClassBounds.realizedWave_tsupport_subset {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (K : ℝ) (R : D → ℝ) (Vr Vθ Vz : D → D) (Φ : D → ℝ) (a : D → ComplexVector) : tsupport (cylindricalCurl R Vr Vθ Vz (vectorPotential K R Vr Vθ Vz Φ a)) ⊆ tsupport a

theorem NavierStokes.CurlClassBounds.physicalCurl_class {s : WeightedClasses.StripData ProblemStatement.SpaceTime} {w : ℕ → ProblemStatement.SpaceTime → ℝ} {α : ℝ} {B : ℕ → ProblemStatement.VelocityField} (hB : WeightedClasses.MemClass s w α B) : WeightedClasses.MemClass s w α fun (n : ℕ) => SpatialCurl.spatialCurl (B n)

Direct compatibility with the actual Euclidean spatial curl. All input jets here are physical spacetime jets, so no separate graph factor occurs.

theorem NavierStokes.CurlClassBounds.physical_strippedRemainder_class {s : WeightedClasses.StripData ProblemStatement.SpaceTime} {w : ℕ → ProblemStatement.SpaceTime → ℝ} {α : ℝ} {B : ℕ → ProblemStatement.VelocityField} {K : ℕ → ℝ} (hB : WeightedClasses.MemClass s w α B) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / K n) : WeightedClasses.MemClass s w (α + 1 / 2) fun (n : ℕ) => OscillatoryCurl.strippedRemainder (K n) (B n)

theorem NavierStokes.CurlClassBounds.physical_normalCoefficient_class {s : WeightedClasses.StripData ProblemStatement.SpaceTime} {w : ℕ → ProblemStatement.SpaceTime → ℝ} {α : ℝ} {N a : ℕ → ProblemStatement.VelocityField} (hN : PhaseJetBounds.PolynomialJets (phaseDomain s) N) (ha : WeightedClasses.MemClass s w α a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖N n x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖N n x‖ ≤ M) : WeightedClasses.MemClass s w α fun (n : ℕ) (x : ProblemStatement.SpaceTime) => OscillatoryCurl.normalCoefficient (N n x) (a n x)

theorem NavierStokes.CurlClassBounds.physical_actualRemainder_class {s : WeightedClasses.StripData ProblemStatement.SpaceTime} {w : ℕ → ProblemStatement.SpaceTime → ℝ} {α : ℝ} {K : ℕ → ℝ} {Φ : ℕ → ProblemStatement.PressureField} {a : ℕ → ProblemStatement.VelocityField} (hN : PhaseJetBounds.PolynomialJets (phaseDomain s) fun (n : ℕ) => OscillatoryCurl.phaseNormal (Φ n)) (ha : WeightedClasses.MemClass s w α a) {b M : ℝ} (hb : 0 < b) (hlower : ∀ (n : ℕ), ∀ x ∈ s.domain, b ≤ ‖OscillatoryCurl.phaseNormal (Φ n) x‖) (hupper : ∀ (n : ℕ), ∀ x ∈ s.domain, ‖OscillatoryCurl.phaseNormal (Φ n) x‖ ≤ M) (hK : WeightedClasses.BandBound s (1 / 2) fun (n : ℕ) => 1 / K n) : WeightedClasses.MemClass s w (α + 1 / 2) fun (n : ℕ) => OscillatoryCurl.strippedRemainder (K n) (OscillatoryCurl.coefficient (Φ n) (a n))

The remainder in the existing physical exact-curl theorem belongs to the claimed class once its actual normal and amplitude jets are supplied.