Documentation

LeanPool.NavierStokesAndEuler.NavierStokes.PhaseEstimates

Quantitative estimates for the actual pulse normal #

The rounded frequency is used consistently throughout the actual phase. The estimates below start from representative data and local base derivative bounds, rather than assuming that the normal is close to its reference value.

The actual moving tangent frame #

The ambient coordinates are radial, angular, axial. The two tangent coordinates are taken in e_r - ρ K, N, where K,N is an orthonormal frame of the last two coordinates. Normal motion, rotation, viscosity and projected forcing are all retained in the exact equation.

The actual growing mode stays in a narrow cone #

The invariant region is proved using a quadratic boundary function, without dividing by the growing coordinate or assuming its positivity along the solution.

@[reducible, inline]

abbrev NavierStokes.GrowingMode.State :

State: an abbreviation for EuclideanSpace ℝ (Fin 2).

Equations

NavierStokes.GrowingMode.State = EuclideanSpace ℝ (Fin 2)

Instances For

noncomputable def NavierStokes.GrowingMode.modalOperator (lam damping e11 e12 e21 e22 : ℝ) :

State →L[ℝ ] State

The actual two-mode coefficient, including four independent error entries.

Equations

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

Instances For

@[simp]

theorem NavierStokes.GrowingMode.modalOperator_zero (lam damping e11 e12 e21 e22 : ℝ) (z : State) :

((modalOperator lam damping e11 e12 e21 e22) z).ofLp 0 = (lam - damping + e11) * z.ofLp 0 + e12 * z.ofLp 1

@[simp]

theorem NavierStokes.GrowingMode.modalOperator_one (lam damping e11 e12 e21 e22 : ℝ) (z : State) :

((modalOperator lam damping e11 e12 e21 e22) z).ofLp 1 = e21 * z.ofLp 0 + (-lam - damping + e22) * z.ofLp 1

theorem NavierStokes.GrowingMode.linear_solution_ne_zero {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {a b : ℝ} (hab : a ≤ b) (A : ℝ → H →L[ℝ ] H) (hA : ContinuousOn A (Set.Icc a b)) {z : ℝ → H} (hz : ∀ t ∈ Set.Icc a b, HasDerivAt z ((A t) (z t)) t) (hinit : z a ≠ 0) (t : ℝ) :

t ∈ Set.Icc a b → z t ≠ 0

A nonzero solution of a continuous homogeneous linear equation cannot hit zero. This uses backwards uniqueness, not a positivity assumption on any coordinate.

theorem NavierStokes.GrowingMode.upper_edge_factor_negative {lam lamMin eps r e11 e12 e21 e22 : ℝ} (hr : 0 < r) (hlam : lamMin ≤ lam) (he11 : |e11| ≤ eps) (he12 : |e12| ≤ eps) (he21 : |e21| ≤ eps) (he22 : |e22| ≤ eps) (hgap : eps * (1 + r) ^ 2 < 2 * lamMin * r) :

e21 + r * (e22 - e11) - r ^ 2 * e12 - 2 * lam * r < 0

The inward algebra at the upper edge of the cone.

theorem NavierStokes.GrowingMode.lower_edge_factor_negative {lam lamMin eps r e11 e12 e21 e22 : ℝ} (hr : 0 < r) (hlam : lamMin ≤ lam) (he11 : |e11| ≤ eps) (he12 : |e12| ≤ eps) (he21 : |e21| ≤ eps) (he22 : |e22| ≤ eps) (hgap : eps * (1 + r) ^ 2 < 2 * lamMin * r) :

-e21 + r * (e22 - e11) + r ^ 2 * e12 - 2 * lam * r < 0

The inward algebra at the lower edge follows by reversing the off-diagonal signs.

theorem NavierStokes.GrowingMode.cone_boundary_derivative_negative {p q lam damping lamMin eps r e11 e12 e21 e22 : ℝ} (hr : 0 < r) (hp : p ≠ 0) (hboundary : q ^ 2 = r ^ 2 * p ^ 2) (hlam : lamMin ≤ lam) (he11 : |e11| ≤ eps) (he12 : |e12| ≤ eps) (he21 : |e21| ≤ eps) (he22 : |e22| ≤ eps) (hgap : eps * (1 + r) ^ 2 < 2 * lamMin * r) :

2 * q * (e21 * p + (-lam - damping + e22) * q) - r ^ 2 * (2 * p * ((lam - damping + e11) * p + e12 * q)) < 0

The quadratic cone boundary has strictly negative derivative at every nonzero boundary point. Scalar damping cancels from this computation.

theorem NavierStokes.GrowingMode.hasDerivAt_coordinate {z : ℝ → State} {z' : State} {t : ℝ} (hz : HasDerivAt z z' t) (i : Fin 2) :

HasDerivAt (fun (s : ℝ) => (z s).ofLp i) (z'.ofLp i) t

theorem NavierStokes.GrowingMode.positive_invariant_cone {a b r eps lamMin : ℝ} (hab : a ≤ b) (hr : 0 < r) (hgap : eps * (1 + r) ^ 2 < 2 * lamMin * r) (lam damping e11 e12 e21 e22 : ℝ → ℝ) {z : ℝ → State} (hA : ContinuousOn (fun (t : ℝ) => modalOperator (lam t) (damping t) (e11 t) (e12 t) (e21 t) (e22 t)) (Set.Icc a b)) (hode : ∀ t ∈ Set.Icc a b, HasDerivAt z ((modalOperator (lam t) (damping t) (e11 t) (e12 t) (e21 t) (e22 t)) (z t)) t) (hlam : ∀ t ∈ Set.Icc a b, lamMin ≤ lam t) (herr : ∀ t ∈ Set.Icc a b, |e11 t| ≤ eps ∧ |e12 t| ≤ eps ∧ |e21 t| ≤ eps ∧ |e22 t| ≤ eps) (hplus : 0 < (z a).ofLp 0) (hminus : (z a).ofLp 1 = 0) (t : ℝ) :

t ∈ Set.Icc a b → 0 < (z t).ofLp 0 ∧ |(z t).ofLp 1| ≤ r * (z t).ofLp 0

The actual homogeneous solution stays in the growing cone, and the growing coordinate is strictly positive. Positivity and nonvanishing are conclusions.

noncomputable def NavierStokes.GrowingMode.coneConstant (lamMin C : ℝ) :

A fixed constant for the manuscript's O(1/S) cone width. The added one allows the same statement when the perturbation bound is zero.

Equations

NavierStokes.GrowingMode.coneConstant lamMin C = 4 * (C + 1) / lamMin

Instances For

theorem NavierStokes.GrowingMode.scaled_cone_conditions {lamMin C S : ℝ} (hlamMin : 0 < lamMin) (hC : 0 ≤ C) (hS : 0 < S) (hlarge : 2 * coneConstant lamMin C ≤ S) :

0 < coneConstant lamMin C / S ∧ coneConstant lamMin C / S ≤ 1 / 2 ∧ C / S * (1 + coneConstant lamMin C / S) ^ 2 < 2 * lamMin * (coneConstant lamMin C / S)

An explicit sufficient meaning of "sufficiently large S".

theorem NavierStokes.GrowingMode.scaled_positive_invariant_cone {a b S C lamMin : ℝ} (hab : a ≤ b) (hlamMin : 0 < lamMin) (hC : 0 ≤ C) (hS : 0 < S) (hlarge : 2 * coneConstant lamMin C ≤ S) (lam damping e11 e12 e21 e22 : ℝ → ℝ) {z : ℝ → State} (hA : ContinuousOn (fun (t : ℝ) => modalOperator (lam t) (damping t) (e11 t) (e12 t) (e21 t) (e22 t)) (Set.Icc a b)) (hode : ∀ t ∈ Set.Icc a b, HasDerivAt z ((modalOperator (lam t) (damping t) (e11 t) (e12 t) (e21 t) (e22 t)) (z t)) t) (hlam : ∀ t ∈ Set.Icc a b, lamMin ≤ lam t) (herr : ∀ t ∈ Set.Icc a b, |e11 t| ≤ C / S ∧ |e12 t| ≤ C / S ∧ |e21 t| ≤ C / S ∧ |e22 t| ≤ C / S) (hplus : 0 < (z a).ofLp 0) (hminus : (z a).ofLp 1 = 0) (t : ℝ) :

t ∈ Set.Icc a b → 0 < (z t).ofLp 0 ∧ |(z t).ofLp 1| ≤ coneConstant lamMin C / S * (z t).ofLp 0

The fixed-width result in the exact K/S form used in (28).

theorem NavierStokes.GrowingMode.hasDerivAt_weighted_scalar {p P : ℝ → ℝ} {p' rate μ a t : ℝ} (hp : HasDerivAt p p' t) (hP : HasDerivAt P (rate * P t) t) (hPne : P t ≠ 0) :

HasDerivAt (fun (s : ℝ) => Real.exp (μ * (s - a)) * p s / P s) (Real.exp (μ * (t - a)) / P t * (p' + (μ - rate) * p t)) t

Derivative of the scalar integrating factor used for both sides of the comparison.

theorem NavierStokes.GrowingMode.scalar_envelope_comparison {a b μ : ℝ} {p p' P rate : ℝ → ℝ} (hab : a ≤ b) (hPpos : ∀ t ∈ Set.Icc a b, 0 < P t) (hP : ∀ t ∈ Set.Icc a b, HasDerivAt P (rate t * P t) t) (hp : ∀ t ∈ Set.Icc a b, HasDerivAt p (p' t) t) (herror : ∀ t ∈ Set.Icc a b, |p' t - rate t * p t| ≤ μ * p t) (t : ℝ) :

t ∈ Set.Icc a b → Real.exp (-μ * (t - a)) * (p a / P a) * P t ≤ p t ∧ p t ≤ Real.exp (μ * (t - a)) * (p a / P a) * P t

A scalar positive envelope comparison from an actual relative derivative bound. No lower bound on the unknown scalar solution is assumed.

theorem NavierStokes.GrowingMode.relative_error_of_cone {p q lam damping referenceDamping e11 e12 eps δ r : ℝ} (hp : 0 < p) (heps : 0 ≤ eps) (hcone : |q| ≤ r * p) (h11 : |e11| ≤ eps) (h12 : |e12| ≤ eps) (hd : |damping - referenceDamping| ≤ δ) :

|(lam - damping + e11) * p + e12 * q - (lam - referenceDamping) * p| ≤ (δ + eps * (1 + r)) * p

Inside the proved cone, the growing coordinate has a multiplicative derivative error. This is the only estimate used for its lower envelope.

theorem NavierStokes.GrowingMode.scaled_growing_mode_bounds {a b S C D L lamMin : ℝ} (hab : a ≤ b) (hlamMin : 0 < lamMin) (hC : 0 ≤ C) (hD : 0 ≤ D) (hS : 0 < S) (hlarge : 2 * coneConstant lamMin C ≤ S) (hslot : b - a ≤ L * S) (lam damping referenceDamping e11 e12 e21 e22 P : ℝ → ℝ) {z : ℝ → State} (hA : ContinuousOn (fun (t : ℝ) => modalOperator (lam t) (damping t) (e11 t) (e12 t) (e21 t) (e22 t)) (Set.Icc a b)) (hode : ∀ t ∈ Set.Icc a b, HasDerivAt z ((modalOperator (lam t) (damping t) (e11 t) (e12 t) (e21 t) (e22 t)) (z t)) t) (hlam : ∀ t ∈ Set.Icc a b, lamMin ≤ lam t) (herr : ∀ t ∈ Set.Icc a b, |e11 t| ≤ C / S ∧ |e12 t| ≤ C / S ∧ |e21 t| ≤ C / S ∧ |e22 t| ≤ C / S) (hdamping : ∀ t ∈ Set.Icc a b, |damping t - referenceDamping t| ≤ D / S) (hPpos : ∀ t ∈ Set.Icc a b, 0 < P t) (hP : ∀ t ∈ Set.Icc a b, HasDerivAt P ((lam t - referenceDamping t) * P t) t) (hplus : 0 < (z a).ofLp 0) (hminus : (z a).ofLp 1 = 0) (t : ℝ) :

t ∈ Set.Icc a b → 0 < (z t).ofLp 0 ∧ |(z t).ofLp 1| ≤ coneConstant lamMin C / S * (z t).ofLp 0 ∧ Real.exp (-(D + 2 * C) * L) * ((z a).ofLp 0 / P a) * P t ≤ (z t).ofLp 0 ∧ (z t).ofLp 0 ≤ Real.exp ((D + 2 * C) * L) * ((z a).ofLp 0 / P a) * P t

Positivity, the K/S cone, and two-sided bounds by a supplied reference envelope on a slot of length at most L*S. None of these conclusions is assumed.

For the manuscript normalization z a 0 = P a, the ratio of initial values is one. The comparison constants are exp(±(D+2*C)*L), independent of the scale S.

theorem NavierStokes.GrowingMode.original_coordinate_bounds {p q h r : ℝ} (hp : 0 < p) (hr : 0 ≤ r) (hrhalf : r ≤ 1 / 2) (hcone : |q| ≤ r * p) :

p / 2 ≤ p + q ∧ p + q ≤ 3 * p / 2 ∧ |h * (p - q) / (p + q) - h| ≤ 4 * |h| * r

Returning from the modal cone to x=p+q, y=h*(p-q) gives both the positive radial amplitude and the ratio error used in equation (28).

@[reducible, inline]

abbrev NavierStokes.MovingFrameODE.Plane :

Plane: an abbreviation for EuclideanSpace ℝ (Fin 2).

Equations

NavierStokes.MovingFrameODE.Plane = EuclideanSpace ℝ (Fin 2)

Instances For

@[reducible, inline]

abbrev NavierStokes.MovingFrameODE.Space :

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

Equations

NavierStokes.MovingFrameODE.Space = EuclideanSpace ℝ (Fin 3)

Instances For

@[reducible, inline]

abbrev NavierStokes.MovingFrameODE.Frame :

Frame: an abbreviation for OrthonormalBasis (Fin 2) ℝ Plane.

Equations

NavierStokes.MovingFrameODE.Frame = OrthonormalBasis (Fin 2) ℝ NavierStokes.MovingFrameODE.Plane

Instances For

noncomputable def NavierStokes.MovingFrameODE.pack (r : ℝ) (w : Plane) :

Pack, given by !₂[r, w 0, w 1].

Equations

NavierStokes.MovingFrameODE.pack r w = !₂[r, w.ofLp 0, w.ofLp 1]

Instances For

noncomputable def NavierStokes.MovingFrameODE.tail (w : Space) :

Tail, given by !₂[w 1, w 2].

Equations

NavierStokes.MovingFrameODE.tail w = !₂[w.ofLp 1, w.ofLp 2]

Instances For

noncomputable def NavierStokes.MovingFrameODE.unitTheta :

Unit theta, given by !₂[1, 0].

Equations

NavierStokes.MovingFrameODE.unitTheta = !₂[1, 0]

Instances For

@[simp]

theorem NavierStokes.MovingFrameODE.pack_zero (r : ℝ) (w : Plane) :

(pack r w).ofLp 0 = r

@[simp]

theorem NavierStokes.MovingFrameODE.pack_one (r : ℝ) (w : Plane) :

(pack r w).ofLp 1 = w.ofLp 0

@[simp]

theorem NavierStokes.MovingFrameODE.pack_two (r : ℝ) (w : Plane) :

(pack r w).ofLp 2 = w.ofLp 1

@[simp]

theorem NavierStokes.MovingFrameODE.tail_pack (r : ℝ) (w : Plane) :

tail (pack r w) = w

@[simp]

theorem NavierStokes.MovingFrameODE.tail_add (u v : Space) :

tail (u + v) = tail u + tail v

@[simp]

theorem NavierStokes.MovingFrameODE.tail_sub (u v : Space) :

tail (u - v) = tail u - tail v

@[simp]

theorem NavierStokes.MovingFrameODE.tail_neg (u : Space) :

tail (-u) = -tail u

@[simp]

theorem NavierStokes.MovingFrameODE.tail_smul (c : ℝ) (u : Space) :

tail (c • u) = c • tail u

theorem NavierStokes.MovingFrameODE.inner_pack (a b : ℝ) (u v : Plane) :

inner ℝ (pack a u) (pack b v) = a * b + inner ℝ u v

theorem NavierStokes.MovingFrameODE.inner_pack_left (a : ℝ) (u : Plane) (v : Space) :

inner ℝ (pack a u) v = a * v.ofLp 0 + inner ℝ u (tail v)

@[simp]

theorem NavierStokes.MovingFrameODE.inner_unitTheta (w : Plane) :

inner ℝ w unitTheta = w.ofLp 0

@[simp]

theorem NavierStokes.MovingFrameODE.frame_inner (B : Frame) (i j : Fin 2) :

inner ℝ (B i) (B j) = if i = j then 1 else 0

theorem NavierStokes.MovingFrameODE.frame_inner00 (B : Frame) :

inner ℝ (B 0) (B 0) = 1

theorem NavierStokes.MovingFrameODE.frame_inner11 (B : Frame) :

inner ℝ (B 1) (B 1) = 1

theorem NavierStokes.MovingFrameODE.frame_inner01 (B : Frame) :

inner ℝ (B 0) (B 1) = 0

theorem NavierStokes.MovingFrameODE.frame_inner10 (B : Frame) :

inner ℝ (B 1) (B 0) = 0

theorem NavierStokes.MovingFrameODE.frame_expand (B : Frame) (w : Plane) :

inner ℝ (B 0) w • B 0 + inner ℝ (B 1) w • B 1 = w

theorem NavierStokes.MovingFrameODE.frame_ext (B : Frame) {u v : Space} (hr : u.ofLp 0 = v.ofLp 0) (hK : inner ℝ (B 0) (tail u) = inner ℝ (B 0) (tail v)) (hN : inner ℝ (B 1) (tail u) = inner ℝ (B 1) (tail v)) :

u = v

noncomputable def NavierStokes.MovingFrameODE.normal (β ρ : ℝ) (B : Frame) :

Normal, given by pack (β * ρ) (β • B 0).

Equations

NavierStokes.MovingFrameODE.normal β ρ B = NavierStokes.MovingFrameODE.pack (β * ρ) (β • B 0)

Instances For

noncomputable def NavierStokes.MovingFrameODE.tangent (ρ : ℝ) (B : Frame) (x y : ℝ) :

Tangent, given by pack x ((-ρ * x) • B 0 + y • B 1).

Equations

NavierStokes.MovingFrameODE.tangent ρ B x y = NavierStokes.MovingFrameODE.pack x ((-ρ * x) • B 0 + y • B 1)

Instances For

noncomputable def NavierStokes.MovingFrameODE.normalMotion (β β' ρ ρ' rot : ℝ) (B : Frame) :

Normal motion, given by pack (β' * ρ + β * ρ') (β' • B 0 + (β * rot) • B 1).

Equations

NavierStokes.MovingFrameODE.normalMotion β β' ρ ρ' rot B = NavierStokes.MovingFrameODE.pack (β' * ρ + β * ρ') (β' • B 0 + (β * rot) • B 1)

Instances For

noncomputable def NavierStokes.MovingFrameODE.tangentMotion (ρ ρ' rot : ℝ) (B : Frame) (x y x' y' : ℝ) :

Tangent motion, given by pack x' (-(ρ' * x + ρ * x' + rot * y) • B 0 + (y' - ρ * rot * x) • B 1).

Equations

NavierStokes.MovingFrameODE.tangentMotion ρ ρ' rot B x y x' y' = NavierStokes.MovingFrameODE.pack x' (-(ρ' * x + ρ * x' + rot * y) • B 0 + (y' - ρ * rot * x) • B 1)

Instances For

noncomputable def NavierStokes.MovingFrameODE.baseAction (F : ℝ) (g : Plane) (t : Space) :

The exact zeroth-order ambient matrix from the pulse equation.

Equations

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

Instances For

theorem NavierStokes.MovingFrameODE.normal_ne_zero {β ρ : ℝ} (B : Frame) (hβ : β ≠ 0) :

normal β ρ B ≠ 0

@[simp]

theorem NavierStokes.MovingFrameODE.normal_tangent (β ρ : ℝ) (B : Frame) (x y : ℝ) :

inner ℝ (normal β ρ B) (tangent ρ B x y) = 0

theorem NavierStokes.MovingFrameODE.normal_self (β ρ : ℝ) (B : Frame) :

inner ℝ (normal β ρ B) (normal β ρ B) = β ^ 2 * (1 + ρ ^ 2)

theorem NavierStokes.MovingFrameODE.normalMotion_tangent (β β' ρ ρ' rot : ℝ) (B : Frame) (x y : ℝ) :

inner ℝ (normalMotion β β' ρ ρ' rot B) (tangent ρ B x y) = β * (ρ' * x + rot * y)

theorem NavierStokes.MovingFrameODE.normal_tangentMotion (β ρ ρ' rot : ℝ) (B : Frame) (x y x' y' : ℝ) :

inner ℝ (normal β ρ B) (tangentMotion ρ ρ' rot B x y x' y') = -β * (ρ' * x + rot * y)

theorem NavierStokes.MovingFrameODE.normal_inner (β ρ : ℝ) (B : Frame) (v : Space) :

inner ℝ (normal β ρ B) v = β * ρ * v.ofLp 0 + β * inner ℝ (B 0) (tail v)

theorem NavierStokes.MovingFrameODE.normal_baseAction (β ρ F : ℝ) (B : Frame) (g : Plane) (x y : ℝ) :

inner ℝ (normal β ρ B) (baseAction F g (tangent ρ B x y)) = β * ((2 * F * (1 + ρ ^ 2) * (B 0).ofLp 0 + inner ℝ (B 0) g) * x - 2 * F * ρ * (B 1).ofLp 0 * y)

noncomputable def NavierStokes.MovingFrameODE.coeff11 (ρ ρ' gK : ℝ) :

Coefficients before subtracting the scalar viscous damping.

Equations

NavierStokes.MovingFrameODE.coeff11 ρ ρ' gK = ρ * (gK - ρ') / (1 + ρ ^ 2)

Instances For

noncomputable def NavierStokes.MovingFrameODE.coeff12 (F Nθ ρ rot : ℝ) :

Coeff12, given by (2 * F * Nθ - ρ * rot) / (1 + ρ ^ 2).

Equations

NavierStokes.MovingFrameODE.coeff12 F Nθ ρ rot = (2 * F * Nθ - ρ * rot) / (1 + ρ ^ 2)

Instances For

noncomputable def NavierStokes.MovingFrameODE.coeff21 (F Nθ gN ρ rot : ℝ) :

Coeff21, given by -(2 * F * Nθ + gN) + ρ * rot.

Equations

NavierStokes.MovingFrameODE.coeff21 F Nθ gN ρ rot = -(2 * F * Nθ + gN) + ρ * rot

Instances For

noncomputable def NavierStokes.MovingFrameODE.rhsX (F d ρ ρ' rot : ℝ) (B : Frame) (g : Plane) (f : Space) (x y : ℝ) :

Rhs X, given by (coeff11 ρ ρ' ⟪B 0, g⟫_ℝ - d) * x + coeff12 F ((B 1) 0) ρ rot * y - (f 0 - ρ * ⟪B 0, tail f⟫_ℝ) / (1 + ρ ^ 2).

Equations

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

Instances For

noncomputable def NavierStokes.MovingFrameODE.rhsY (F d ρ rot : ℝ) (B : Frame) (g : Plane) (f : Space) (x y : ℝ) :

Rhs Y, given by coeff21 F ((B 1) 0) ⟪B 1, g⟫_ℝ ρ rot * x - d * y - ⟪B 1, tail f⟫_ℝ.

Equations

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

Instances For

theorem NavierStokes.MovingFrameODE.projectedRhs_radial {β : ℝ} (hβ : β ≠ 0) (β' ρ ρ' rot F d : ℝ) (B : Frame) (g : Plane) (f : Space) (x y : ℝ) :

(TangentProjection.projectedRhs (normal β ρ B) (normalMotion β β' ρ ρ' rot B) (tangent ρ B x y) (baseAction F g (tangent ρ B x y)) f d).ofLp 0 = rhsX F d ρ ρ' rot B g f x y

theorem NavierStokes.MovingFrameODE.projectedRhs_N (β β' ρ ρ' rot F d : ℝ) (B : Frame) (g : Plane) (f : Space) (x y : ℝ) :

inner ℝ (B 1) (tail (TangentProjection.projectedRhs (normal β ρ B) (normalMotion β β' ρ ρ' rot B) (tangent ρ B x y) (baseAction F g (tangent ρ B x y)) f d)) = rhsY F d ρ rot B g f x y - ρ * rot * x

theorem NavierStokes.MovingFrameODE.projectedRhs_eq_tangentMotion {β : ℝ} (hβ : β ≠ 0) (β' ρ ρ' rot F d : ℝ) (B : Frame) (g : Plane) (f : Space) (x y : ℝ) :

TangentProjection.projectedRhs (normal β ρ B) (normalMotion β β' ρ ρ' rot B) (tangent ρ B x y) (baseAction F g (tangent ρ B x y)) f d = tangentMotion ρ ρ' rot B x y (rhsX F d ρ ρ' rot B g f x y) (rhsY F d ρ rot B g f x y)

Exact moving-frame reduction of the ambient projected equation.

theorem NavierStokes.MovingFrameODE.tangentMotion_eq_projectedRhs_iff {β : ℝ} (hβ : β ≠ 0) (β' ρ ρ' rot F d : ℝ) (B : Frame) (g : Plane) (f : Space) (x y x' y' : ℝ) :

tangentMotion ρ ρ' rot B x y x' y' = TangentProjection.projectedRhs (normal β ρ B) (normalMotion β β' ρ ρ' rot B) (tangent ρ B x y) (baseAction F g (tangent ρ B x y)) f d ↔ x' = rhsX F d ρ ρ' rot B g f x y ∧ y' = rhsY F d ρ rot B g f x y

The moving-coordinate equation has exactly two scalar equations.

noncomputable def NavierStokes.MovingFrameODE.packCLM :

ℝ × Plane →L[ℝ ] Space

Pack continuous linear map, constructed using LinearMap.toContinuousLinearMap.

Equations

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

Instances For

noncomputable def NavierStokes.MovingFrameODE.tailCLM :

Space →L[ℝ ] Plane

Tail continuous linear map, given by LinearMap.toContinuousLinearMap { toFun := tail map_add' := tail_add map_smul' := tail_smul }.

Equations

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

Instances For

theorem NavierStokes.MovingFrameODE.hasDerivAt_pack {r : ℝ → ℝ} {w : ℝ → Plane} {r' v : ℝ} {w' : Plane} (hr : HasDerivAt r r' v) (hw : HasDerivAt w w' v) :

HasDerivAt (fun (s : ℝ) => pack (r s) (w s)) (pack r' w') v

theorem NavierStokes.MovingFrameODE.hasDerivAt_normal {β ρ : ℝ → ℝ} {B : ℝ → Frame} {v β' ρ' rot : ℝ} (hβ : HasDerivAt β β' v) (hρ : HasDerivAt ρ ρ' v) (hK : HasDerivAt (fun (s : ℝ) => (B s) 0) (rot • (B v) 1) v) :

HasDerivAt (fun (s : ℝ) => normal (β s) (ρ s) (B s)) (normalMotion (β v) β' (ρ v) ρ' rot (B v)) v

Differentiation of the actual normal. The frame derivative is measured in the same moving orthonormal basis.

theorem NavierStokes.MovingFrameODE.hasDerivAt_tangent {ρ x y : ℝ → ℝ} {B : ℝ → Frame} {v ρ' rot x' y' : ℝ} (hρ : HasDerivAt ρ ρ' v) (hx : HasDerivAt x x' v) (hy : HasDerivAt y y' v) (hK : HasDerivAt (fun (s : ℝ) => (B s) 0) (rot • (B v) 1) v) (hN : HasDerivAt (fun (s : ℝ) => (B s) 1) (-rot • (B v) 0) v) :

HasDerivAt (fun (s : ℝ) => tangent (ρ s) (B s) (x s) (y s)) (tangentMotion (ρ v) ρ' rot (B v) (x v) (y v) x' y') v

Differentiation of the actual tangent parametrization.

theorem NavierStokes.MovingFrameODE.hasDerivAt_projected_iff {β ρ x y : ℝ → ℝ} {B : ℝ → Frame} {v β' ρ' rot x' y' F d : ℝ} {g : Plane} {f : Space} (hβ0 : β v ≠ 0) (hρ : HasDerivAt ρ ρ' v) (hx : HasDerivAt x x' v) (hy : HasDerivAt y y' v) (hK : HasDerivAt (fun (s : ℝ) => (B s) 0) (rot • (B v) 1) v) (hN : HasDerivAt (fun (s : ℝ) => (B s) 1) (-rot • (B v) 0) v) :

HasDerivAt (fun (s : ℝ) => tangent (ρ s) (B s) (x s) (y s)) (TangentProjection.projectedRhs (normal (β v) (ρ v) (B v)) (normalMotion (β v) β' (ρ v) ρ' rot (B v)) (tangent (ρ v) (B v) (x v) (y v)) (baseAction F g (tangent (ρ v) (B v) (x v) (y v))) f d) v ↔ x' = rhsX F d (ρ v) ρ' rot (B v) g f (x v) (y v) ∧ y' = rhsY F d (ρ v) rot (B v) g f (x v) (y v)

The ambient ODE is equivalent to the two explicit coordinate ODEs, using actual derivatives of the curve and the moving frame.

noncomputable def NavierStokes.MovingFrameODE.quarterTurn :

Plane →L[ℝ ] Plane

Counterclockwise quarter-turn in the angular-axial plane.

Equations

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

Instances For

theorem NavierStokes.MovingFrameODE.quarterTurn_square (w : Plane) :

quarterTurn (quarterTurn w) = -w

theorem NavierStokes.MovingFrameODE.inner_quarterTurn_self (w : Plane) :

inner ℝ w (quarterTurn w) = 0

theorem NavierStokes.MovingFrameODE.quarterTurn_inner (u v : Plane) :

inner ℝ (quarterTurn u) (quarterTurn v) = inner ℝ u v

theorem NavierStokes.MovingFrameODE.unit_pair_orthonormal (K : Plane) (hK : ‖K‖ = 1) :

Orthonormal ℝ ![K, quarterTurn K]

noncomputable def NavierStokes.MovingFrameODE.frameOfUnit (K : Plane) (hK : ‖K‖ = 1) :

Frame of unit as an element of Frame.

Equations

NavierStokes.MovingFrameODE.frameOfUnit K hK = (basisOfOrthonormalOfCardEqFinrank ⋯ NavierStokes.MovingFrameODE.frameOfUnit._proof_1).toOrthonormalBasis ⋯

Instances For

@[simp]

theorem NavierStokes.MovingFrameODE.frameOfUnit_zero (K : Plane) (hK : ‖K‖ = 1) :

(frameOfUnit K hK) 0 = K

@[simp]

theorem NavierStokes.MovingFrameODE.frameOfUnit_one (K : Plane) (hK : ‖K‖ = 1) :

(frameOfUnit K hK) 1 = quarterTurn K

noncomputable def NavierStokes.MovingFrameODE.normalScale (n : Space) :

Normal scale, given by ‖tail n‖.

Equations

NavierStokes.MovingFrameODE.normalScale n = ‖NavierStokes.MovingFrameODE.tail n‖

Instances For

noncomputable def NavierStokes.MovingFrameODE.radialSlope (n : Space) :

Radial slope, given by n 0 / normalScale n.

Equations

NavierStokes.MovingFrameODE.radialSlope n = n.ofLp 0 / NavierStokes.MovingFrameODE.normalScale n

Instances For

noncomputable def NavierStokes.MovingFrameODE.normalDirection (n : Space) :

Normal direction, given by (normalScale n)⁻¹ • tail n.

Equations

NavierStokes.MovingFrameODE.normalDirection n = (NavierStokes.MovingFrameODE.normalScale n)⁻¹ • NavierStokes.MovingFrameODE.tail n

Instances For

theorem NavierStokes.MovingFrameODE.normalScale_pos {n : Space} (hn : tail n ≠ 0) :

0 < normalScale n

theorem NavierStokes.MovingFrameODE.normalDirection_unit {n : Space} (hn : tail n ≠ 0) :

‖normalDirection n‖ = 1

noncomputable def NavierStokes.MovingFrameODE.normalFrame (n : Space) (hn : tail n ≠ 0) :

Normal frame, given by frameOfUnit (normalDirection n) (normalDirection_unit hn).

Equations

NavierStokes.MovingFrameODE.normalFrame n hn = NavierStokes.MovingFrameODE.frameOfUnit (NavierStokes.MovingFrameODE.normalDirection n) ⋯

Instances For

@[simp]

theorem NavierStokes.MovingFrameODE.normalFrame_zero (n : Space) (hn : tail n ≠ 0) :

(normalFrame n hn) 0 = normalDirection n

@[simp]

theorem NavierStokes.MovingFrameODE.normalFrame_one (n : Space) (hn : tail n ≠ 0) :

(normalFrame n hn) 1 = quarterTurn (normalDirection n)

theorem NavierStokes.MovingFrameODE.normal_reconstructed {n : Space} (hn : tail n ≠ 0) :

normal (normalScale n) (radialSlope n) (normalFrame n hn) = n

Reconstruction of the given normal, not an independent choice of reference normal. Only its tangential part is required to be nonzero.

theorem NavierStokes.MovingFrameODE.contDiffAt_normalScale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : WithTop ℕ∞} {n : E → Space} {q : E} (hn : ContDiffAt ℝ m n q) (hne : tail (n q) ≠ 0) :

ContDiffAt ℝ m (fun (p : E) => normalScale (n p)) q

theorem NavierStokes.MovingFrameODE.contDiffAt_radialSlope {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : WithTop ℕ∞} {n : E → Space} {q : E} (hn : ContDiffAt ℝ m n q) (hne : tail (n q) ≠ 0) :

ContDiffAt ℝ m (fun (p : E) => radialSlope (n p)) q

theorem NavierStokes.MovingFrameODE.contDiffAt_normalDirection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : WithTop ℕ∞} {n : E → Space} {q : E} (hn : ContDiffAt ℝ m n q) (hne : tail (n q) ≠ 0) :

ContDiffAt ℝ m (fun (p : E) => normalDirection (n p)) q

theorem NavierStokes.MovingFrameODE.contDiffAt_transverseDirection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : WithTop ℕ∞} {n : E → Space} {q : E} (hn : ContDiffAt ℝ m n q) (hne : tail (n q) ≠ 0) :

ContDiffAt ℝ m (fun (p : E) => quarterTurn (normalDirection (n p))) q

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

ContDiffAt ℝ (↑⊤) (fun (r : PhaseCalculus.Slot) => radialSlope (PhaseCalculus.phaseNormal ε p pz x0 F G r)) q ∧ ContDiffAt ℝ (↑⊤) (fun (r : PhaseCalculus.Slot) => normalDirection (PhaseCalculus.phaseNormal ε p pz x0 F G r)) q ∧ ContDiffAt ℝ (↑⊤) (fun (r : PhaseCalculus.Slot) => quarterTurn (normalDirection (PhaseCalculus.phaseNormal ε p pz x0 F G r))) q

The reconstructed directions are jointly smooth functions of the actual phase normal, away from the axis and zeros of its tangential part.

theorem NavierStokes.MovingFrameODE.unit_curve_rotation {K : ℝ → Plane} {K' : Plane} {v : ℝ} (hK : HasDerivAt K K' v) (hunit : ∀ᶠ (s : ℝ) in nhds v, ‖K s‖ = 1) :

K' = inner ℝ (quarterTurn (K v)) K' • quarterTurn (K v)

A differentiable unit vector has purely rotational derivative in its orthonormal frame. The angular speed is computed from the derivative.

theorem NavierStokes.MovingFrameODE.hasDerivAt_quarterTurn_of_rotation {K : ℝ → Plane} {v rot : ℝ} (hK : HasDerivAt K (rot • quarterTurn (K v)) v) :

HasDerivAt (fun (s : ℝ) => quarterTurn (K s)) (-rot • K v) v

Rotation of the second direction is derived, rather than assumed independently of the first direction.

theorem NavierStokes.MovingFrameODE.reconstructed_frame_hasDerivAt {n : ℝ → Space} {n' : Space} {v : ℝ} (hn : HasDerivAt n n' v) (hne : tail (n v) ≠ 0) :

∃ (rot : ℝ), HasDerivAt (fun (s : ℝ) => normalDirection (n s)) (rot • quarterTurn (normalDirection (n v))) v ∧ HasDerivAt (fun (s : ℝ) => quarterTurn (normalDirection (n s))) (-rot • normalDirection (n v)) v

Every differentiable normal with nonzero tangential part supplies the rotating frame needed by the exact coordinate equation.

Quantitative coefficient comparison #

theorem NavierStokes.MovingFrameODE.abs_div_le_of_one_le (a d : ℝ) (hd : 1 ≤ d) :

|a / d| ≤ |a|

theorem NavierStokes.MovingFrameODE.reciprocal_quadratic_difference (r s : ℝ) :

|1 / (1 + r ^ 2) - 1 / (1 + s ^ 2)| ≤ |r - s| * (|r| + |s|)

theorem NavierStokes.MovingFrameODE.product_perturbation_le {F F0 N N0 M η : ℝ} (hN : |N| ≤ 1) (hF0 : |F0| ≤ M) (hF : |F - F0| ≤ η) (hNd : |N - N0| ≤ η) :

|F * N - F0 * N0| ≤ (1 + M) * η

theorem NavierStokes.MovingFrameODE.scalar_coefficients_close {F F0 N N0 ρ s ρ' rot gK gN g0 M η : ℝ} (hM : 1 ≤ M) (hη : 0 ≤ η) (hρ : |ρ| ≤ M) (hs : |s| ≤ M) (hN : |N| ≤ 1) (hN0 : |N0| ≤ 1) (hF0 : |F0| ≤ M) (hF : |F - F0| ≤ η) (hNd : |N - N0| ≤ η) (hρd : |ρ - s| ≤ η) (hρ' : |ρ'| ≤ η) (hrot : |rot| ≤ η) (hgK : |gK| ≤ η) (hgN : |gN - g0| ≤ η) :

|coeff11 ρ ρ' gK| ≤ 16 * M ^ 2 * η ∧ |coeff12 F N ρ rot - 2 * F0 * N0 / (1 + s ^ 2)| ≤ 16 * M ^ 2 * η ∧ |coeff21 F N gN ρ rot - -(2 * F0 * N0 + g0)| ≤ 16 * M ^ 2 * η

Explicit bounds in geometric coordinates. The four small quantities are the normal slope error, rotation, radial slope derivative and projected shear. No coefficient or propagator estimate is included among the assumptions.

theorem NavierStokes.MovingFrameODE.inner_perturbation_le {K K0 g g0 : Plane} {M η : ℝ} (hK : ‖K‖ ≤ 1) (hg0 : ‖g0‖ ≤ M) (hKd : ‖K - K0‖ ≤ η) (hgd : ‖g - g0‖ ≤ η) :

|inner ℝ K g - inner ℝ K0 g0| ≤ (1 + M) * η

theorem NavierStokes.MovingFrameODE.frame_coordinate_abs_le_one (B : Frame) (i j : Fin 2) :

|(B i).ofLp j| ≤ 1

theorem NavierStokes.MovingFrameODE.frame_coordinate_difference_le {B B0 : Frame} {i j : Fin 2} {η : ℝ} (h : ‖B i - B0 i‖ ≤ η) :

|(B i).ofLp j - (B0 i).ofLp j| ≤ η

theorem NavierStokes.MovingFrameODE.frame_coefficients_close {B B0 : Frame} {g g0 : Plane} {F F0 ρ s ρ' rot M η : ℝ} (hM : 1 ≤ M) (hη : 0 ≤ η) (hρ : |ρ| ≤ M) (hs : |s| ≤ M) (hF0 : |F0| ≤ M) (hg0 : ‖g0‖ ≤ M) (horth : inner ℝ (B0 0) g0 = 0) (hF : |F - F0| ≤ η) (hg : ‖g - g0‖ ≤ η) (hK : ‖B 0 - B0 0‖ ≤ η) (hN : ‖B 1 - B0 1‖ ≤ η) (hρd : |ρ - s| ≤ η) (hρ' : |ρ'| ≤ η) (hrot : |rot| ≤ η) :

|coeff11 ρ ρ' (inner ℝ (B 0) g)| ≤ 16 * M ^ 2 * (1 + M) * η ∧ |coeff12 F ((B 1).ofLp 0) ρ rot - 2 * F0 * (B0 1).ofLp 0 / (1 + s ^ 2)| ≤ 16 * M ^ 2 * (1 + M) * η ∧ |coeff21 F ((B 1).ofLp 0) (inner ℝ (B 1) g) ρ rot - -(2 * F0 * (B0 1).ofLp 0 + inner ℝ (B0 1) g0)| ≤ 16 * M ^ 2 * (1 + M) * η

Norm bounds on actual geometric data imply the matrix comparison. Taking η = C / S gives the required O(1/S) with the displayed constant. The reference shear is perpendicular to the reference normal direction.

The moving eigenbasis, including its derivative #

noncomputable def NavierStokes.MovingFrameODE.modal11 (a b c h rate : ℝ) :

Modal11, given by (a + h * b + c / h - rate) / 2.

Equations

NavierStokes.MovingFrameODE.modal11 a b c h rate = (a + h * b + c / h - rate) / 2

Instances For

noncomputable def NavierStokes.MovingFrameODE.modal12 (a b c h rate : ℝ) :

Modal12, given by (a - h * b + c / h + rate) / 2.

Equations

NavierStokes.MovingFrameODE.modal12 a b c h rate = (a - h * b + c / h + rate) / 2

Instances For

noncomputable def NavierStokes.MovingFrameODE.modal21 (a b c h rate : ℝ) :

Modal21, given by (a + h * b - c / h + rate) / 2.

Equations

NavierStokes.MovingFrameODE.modal21 a b c h rate = (a + h * b - c / h + rate) / 2

Instances For

noncomputable def NavierStokes.MovingFrameODE.modal22 (a b c h rate : ℝ) :

Modal22, given by (a - h * b - c / h - rate) / 2.

Equations

NavierStokes.MovingFrameODE.modal22 a b c h rate = (a - h * b - c / h - rate) / 2

Instances For

theorem NavierStokes.MovingFrameODE.modal_equations_iff {h : ℝ} (hh : h ≠ 0) (p q p' q' lam damping a b c rate fx fy : ℝ) :

p' + q' = (a - damping) * (p + q) + (lam / h + b) * (h * (p - q)) + fx ∧ rate * h * (p - q) + h * (p' - q') = (lam * h + c) * (p + q) - damping * (h * (p - q)) + fy ↔ p' = (lam - damping + modal11 a b c h rate) * p + modal12 a b c h rate * q + (fx + fy / h) / 2 ∧ q' = modal21 a b c h rate * p + (-lam - damping + modal22 a b c h rate) * q + (fx - fy / h) / 2

Exact change to x = p + q, y = h (p - q), with h' = rate * h. Here the reference off-diagonal entries are λ/h and λ*h, and a,b,c are the three errors already estimated by frame_coefficients_close.

noncomputable def NavierStokes.MovingFrameODE.pairCLM :

ℝ × ℝ →L[ℝ ] Plane

Pair continuous linear map, constructed using LinearMap.toContinuousLinearMap.

Equations

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

Instances For

theorem NavierStokes.MovingFrameODE.hasDerivAt_modal {p q h : ℝ → ℝ} {v p' q' lam damping a b c rate fx fy : ℝ} (hh0 : h v ≠ 0) (hp : HasDerivAt p p' v) (hq : HasDerivAt q q' v) (hh : HasDerivAt h (rate * h v) v) (hx : HasDerivAt (fun (s : ℝ) => p s + q s) ((a - damping) * (p v + q v) + (lam / h v + b) * (h v * (p v - q v)) + fx) v) (hy : HasDerivAt (fun (s : ℝ) => h s * (p s - q s)) ((lam * h v + c) * (p v + q v) - damping * (h v * (p v - q v)) + fy) v) :

HasDerivAt (fun (s : ℝ) => !₂[p s, q s]) ((GrowingMode.modalOperator lam damping (modal11 a b c (h v) rate) (modal12 a b c (h v) rate) (modal21 a b c (h v) rate) (modal22 a b c (h v) rate)) !₂[p v, q v] + !₂[(fx + fy / h v) / 2, (fx - fy / h v) / 2]) v

Actual differentiation of the moving eigenbasis gives the operator used by GrowingMode; no propagator estimate or cone condition is assumed.

theorem NavierStokes.MovingFrameODE.abs_four_sum_div_two_le {a b c d A B C D : ℝ} (ha : |a| ≤ A) (hb : |b| ≤ B) (hc : |c| ≤ C) (hd : |d| ≤ D) :

|(a + b + c + d) / 2| ≤ A + B + C + D

theorem NavierStokes.MovingFrameODE.modal_errors_le {a b c h rate H δ κ : ℝ} (hH : 0 ≤ H) (ha : |a| ≤ δ) (hb : |b| ≤ δ) (hc : |c| ≤ δ) (hh : |h| ≤ H) (hhi : |1 / h| ≤ H) (hrate : |rate| ≤ κ) :

|modal11 a b c h rate| ≤ (1 + 2 * H) * δ + κ ∧ |modal12 a b c h rate| ≤ (1 + 2 * H) * δ + κ ∧ |modal21 a b c h rate| ≤ (1 + 2 * H) * δ + κ ∧ |modal22 a b c h rate| ≤ (1 + 2 * H) * δ + κ

All four modal errors are bounded explicitly. rate = h'/h is the extra error arising from the time-dependent eigenbasis.

theorem NavierStokes.MovingFrameODE.tangent_reconstructed {β ρ : ℝ} (hβ : β ≠ 0) (B : Frame) (t : Space) (ht : inner ℝ (normal β ρ B) t = 0) :

tangent ρ B (t.ofLp 0) (inner ℝ (B 1) (tail t)) = t

A tangent ambient vector is recovered from its two coordinate values.

theorem NavierStokes.MovingFrameODE.modalOperator_eq_coefficient (lam damping e11 e12 e21 e22 : ℝ) :

GrowingMode.modalOperator lam damping e11 e12 e21 e22 = ViscousPropagator.coefficient lam damping (GrowingMode.modalOperator 0 0 e11 e12 e21 e22)

theorem NavierStokes.MovingFrameODE.plane_norm_le_coordinate_sum (z : Plane) :

‖z‖ ≤ |z.ofLp 0| + |z.ofLp 1|

theorem NavierStokes.MovingFrameODE.modal_error_opNorm_le {e11 e12 e21 e22 ε : ℝ} (he11 : |e11| ≤ ε) (he12 : |e12| ≤ ε) (he21 : |e21| ≤ ε) (he22 : |e22| ≤ ε) :

‖GrowingMode.modalOperator 0 0 e11 e12 e21 e22‖ ≤ 4 * ε

Entrywise control gives a genuine Euclidean operator norm estimate. The harmless factor four avoids any choice of an equivalent matrix norm.

theorem NavierStokes.MovingFrameODE.modal_energy_le {lam e11 e12 e21 e22 ε : ℝ} (hlam : 0 ≤ lam) (damping : ℝ) (he11 : |e11| ≤ ε) (he12 : |e12| ≤ ε) (he21 : |e21| ≤ ε) (he22 : |e22| ≤ ε) (z : Plane) :

inner ℝ z ((GrowingMode.modalOperator lam damping e11 e12 e21 e22) z) ≤ (lam - damping + 4 * ε) * ‖z‖ ^ 2

This is the exact quadratic-form hypothesis accepted by the weighted propagator and parameter-jet estimates. Scalar viscosity keeps its sign.

@[reducible, inline]

abbrev NavierStokes.PhaseEstimates.Plane :

Plane: an abbreviation for MovingFrameODE.Plane.

Equations

NavierStokes.PhaseEstimates.Plane = NavierStokes.MovingFrameODE.Plane

Instances For

@[reducible, inline]

abbrev NavierStokes.PhaseEstimates.Space :

Space: an abbreviation for MovingFrameODE.Space.

Equations

NavierStokes.PhaseEstimates.Space = NavierStokes.MovingFrameODE.Space

Instances For

@[reducible, inline]

abbrev NavierStokes.PhaseEstimates.Slow :

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

NavierStokes.PhaseEstimates.Slow = NavierStokes.PhaseCalculus.Slow

Instances For

noncomputable def NavierStokes.PhaseEstimates.nonzeroRound (x : ℝ) :

Rounding in the punctured integer lattice. The zero floor is replaced by one; the distance to the input is still at most one.

Equations

NavierStokes.PhaseEstimates.nonzeroRound x = if ⌊x⌋ = 0 then 1 else ⌊x⌋

Instances For

theorem NavierStokes.PhaseEstimates.nonzeroRound_ne_zero (x : ℝ) :

nonzeroRound x ≠ 0

theorem NavierStokes.PhaseEstimates.nonzeroRound_error (x : ℝ) :

|↑(nonzeroRound x) - x| ≤ 1

noncomputable def NavierStokes.PhaseEstimates.roundedFrequency (k target : ℝ) :

Rounded frequency, given by (nonzeroRound (k * target) : ℝ) / k.

Equations

NavierStokes.PhaseEstimates.roundedFrequency k target = ↑(NavierStokes.PhaseEstimates.nonzeroRound (k * target)) / k

Instances For

theorem NavierStokes.PhaseEstimates.roundedFrequency_integer {k : ℝ} (hk : k ≠ 0) (target : ℝ) :

k * roundedFrequency k target = ↑(nonzeroRound (k * target))

theorem NavierStokes.PhaseEstimates.roundedFrequency_nonzero {k : ℝ} (hk : k ≠ 0) (target : ℝ) :

∃ (m : ℤ), m ≠ 0 ∧ k * roundedFrequency k target = ↑m

theorem NavierStokes.PhaseEstimates.roundedFrequency_ne_zero {k : ℝ} (hk : k ≠ 0) (target : ℝ) :

roundedFrequency k target ≠ 0

theorem NavierStokes.PhaseEstimates.roundedFrequency_error {k : ℝ} (hk : 0 < k) (target : ℝ) :

|roundedFrequency k target - target| ≤ 1 / k

noncomputable def NavierStokes.PhaseEstimates.representativeFrequency (B sigma u L : ℝ) (K g : Plane) :

The fixed representative frequency in its two tangential components.

Equations

NavierStokes.PhaseEstimates.representativeFrequency B sigma u L K g = B • (K - (sigma * u / (L * ‖g‖ ^ 2)) • g)

Instances For

theorem NavierStokes.PhaseEstimates.representative_slope (B sigma u L : ℝ) (K g : Plane) (hg : g ≠ 0) (horth : inner ℝ K g = 0) :

inner ℝ (representativeFrequency B sigma u L K g) g = -sigma * B * u / L

theorem NavierStokes.PhaseEstimates.representative_tilt (B sigma u L : ℝ) (K g : Plane) :

‖representativeFrequency B sigma u L K g - B • K‖ = |B| * |sigma| * |u| / (|L| * ‖g‖)

theorem NavierStokes.PhaseEstimates.representative_frequency_bound (B sigma u L : ℝ) (K g : Plane) (hK : ‖K‖ = 1) :

‖representativeFrequency B sigma u L K g‖ ≤ |B| + |B| * |sigma| * |u| / (|L| * ‖g‖)

A bound on the fixed representative frequency follows from its explicit tilt; its angular component is later multiplied by the representative radius.

noncomputable def NavierStokes.PhaseEstimates.signedSlot (sigma u L v : ℝ) :

Signed slot, given by sigma * (u / 2 + u * v / L).

Equations

NavierStokes.PhaseEstimates.signedSlot sigma u L v = sigma * (u / 2 + u * v / L)

Instances For

theorem NavierStokes.PhaseEstimates.radial_reference_identity (B sigma u L v : ℝ) :

sigma * B * u / 2 - v * (-sigma * B * u / L) = B * signedSlot sigma u L v

The cancellation producing the intended radial slope is exact for the unrounded representative data.

Local C2 control implies the derivative comparison at the representative #

theorem NavierStokes.PhaseEstimates.local_first_derivative_close {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F F0 : E → ℝ} {U : Set E} {q q0 : E} {M diameter baseError : ℝ} (hM : 0 ≤ M) (hU : Convex ℝ U) (hq : q ∈ U) (hq0 : q0 ∈ U) (hC2 : ∀ x ∈ U, DifferentiableAt ℝ (fderiv ℝ F0) x) (hsecond : ∀ x ∈ U, ‖fderiv ℝ (fderiv ℝ F0) x‖ ≤ M) (hdiameter : ‖q - q0‖ ≤ diameter) (hbase : ‖fderiv ℝ F q - fderiv ℝ F0 q‖ ≤ baseError) :

‖fderiv ℝ F q - fderiv ℝ F0 q0‖ ≤ M * diameter + baseError

The second derivative controls variation of the first derivative across a convex chart. The actual base differs in C1 by the independently supplied baseError, and the chart diameter is diameter.

theorem NavierStokes.PhaseEstimates.local_directional_derivative_close {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F F0 : E → ℝ} {U : Set E} {q q0 e : E} {M diameter baseError : ℝ} (hM : 0 ≤ M) (hU : Convex ℝ U) (hq : q ∈ U) (hq0 : q0 ∈ U) (hC2 : ∀ x ∈ U, DifferentiableAt ℝ (fderiv ℝ F0) x) (hsecond : ∀ x ∈ U, ‖fderiv ℝ (fderiv ℝ F0) x‖ ≤ M) (hdiameter : ‖q - q0‖ ≤ diameter) (hbase : ‖fderiv ℝ F q - fderiv ℝ F0 q‖ ≤ baseError) (he : ‖e‖ ≤ 1) :

|(fderiv ℝ F q) e - (fderiv ℝ F0 q0) e| ≤ M * diameter + baseError

Pointwise error estimates before choosing the band scale #

theorem NavierStokes.PhaseEstimates.radial_frequency_error {p target pz a a0 b b0 M rounding base : ℝ} (hp : |p - target| ≤ rounding) (ha : |a| ≤ M) (htarget : |target| ≤ M) (hpz : |pz| ≤ M) (ha0 : |a - a0| ≤ base) (hb0 : |b - b0| ≤ base) :

|p * a + pz * b - (target * a0 + pz * b0)| ≤ M * rounding + 2 * M * base

theorem NavierStokes.PhaseEstimates.angular_frequency_error {p target R R0 M rounding diameter : ℝ} (hR : R ≠ 0) (hR0 : R0 ≠ 0) (hp : |p - target| ≤ rounding) (htarget : |target| ≤ M) (hRi : |1 / R| ≤ M) (hR0i : |1 / R0| ≤ M) (hRd : |R - R0| ≤ diameter) :

|p / R - target / R0| ≤ M * rounding + M ^ 3 * diameter

theorem NavierStokes.PhaseEstimates.axial_frequency_bound {p target pz a b M rounding : ℝ} (hM : 1 ≤ M) (hr : rounding ≤ 1) (hp : |p - target| ≤ rounding) (htarget : |target| ≤ M) (hpz : |pz| ≤ M) (ha : |a| ≤ M) (hb : |b| ≤ M) :

|p * a + pz * b| ≤ 3 * M ^ 2

noncomputable def NavierStokes.PhaseEstimates.explicitNormal (ε p pz x0 R v FR GR FZ GZ : ℝ) :

Explicit normal, given by `!₂[x0 - v * (p * FR + pz * GR), p / R, pz - ε * v * (p * FZ + pz

GZ)]`.

Equations

NavierStokes.PhaseEstimates.explicitNormal ε p pz x0 R v FR GR FZ GZ = !₂[x0 - v * (p * FR + pz * GR), p / R, pz - ε * v * (p * FZ + pz * GZ)]

Instances For

noncomputable def NavierStokes.PhaseEstimates.referenceNormal (B sigma u L v : ℝ) (K : Plane) :

Reference normal, given by MovingFrameODE.pack (B * signedSlot sigma u L v) (B • K).

Equations

NavierStokes.PhaseEstimates.referenceNormal B sigma u L v K = NavierStokes.MovingFrameODE.pack (B * NavierStokes.PhaseEstimates.signedSlot sigma u L v) (B • K)

Instances For

theorem NavierStokes.PhaseEstimates.vec3_norm_le_sum (w : Space) :

‖w‖ ≤ |w.ofLp 0| + |w.ofLp 1| + |w.ofLp 2|

theorem NavierStokes.PhaseEstimates.normal_error_from_components {ε p pz R v FR GR FZ GZ B sigma u L radial angular axial shear : ℝ} {K : Plane} (hRadial : |p * FR + pz * GR - -sigma * B * u / L| ≤ radial) (hAngular : |p / R - B * K.ofLp 0| ≤ angular) (hAxial : |pz - B * K.ofLp 1| ≤ axial) (hShear : |p * FZ + pz * GZ| ≤ shear) :

‖explicitNormal ε p pz (sigma * B * u / 2) R v FR GR FZ GZ - referenceNormal B sigma u L v K‖ ≤ |v| * radial + angular + axial + |ε| * |v| * shear

Assembly of the actual normal error from its three independently derived coefficient errors. Slot length multiplies only the radial and axial defects.

theorem NavierStokes.PhaseEstimates.representative_slope_coordinates {B sigma u L R0 target pz FR0 GR0 : ℝ} {K g : Plane} (hR0 : R0 ≠ 0) (hg : g ≠ 0) (horth : inner ℝ K g = 0) (hgdef : g = !₂[R0 * FR0, GR0]) (hfreq : !₂[target / R0, pz] = representativeFrequency B sigma u L K g) :

target * FR0 + pz * GR0 = -sigma * B * u / L

theorem NavierStokes.PhaseEstimates.representative_coordinate_errors {B sigma u L R0 target pz : ℝ} {K g : Plane} (hfreq : !₂[target / R0, pz] = representativeFrequency B sigma u L K g) :

|target / R0 - B * K.ofLp 0| ≤ |B| * |sigma| * |u| / (|L| * ‖g‖) ∧ |pz - B * K.ofLp 1| ≤ |B| * |sigma| * |u| / (|L| * ‖g‖)

theorem NavierStokes.PhaseEstimates.explicit_normal_estimate {ε p target pz R R0 v FR GR FZ GZ FR0 GR0 B sigma u L M rounding diameter base : ℝ} {K g : Plane} (hR : R ≠ 0) (hR0 : R0 ≠ 0) (hg : g ≠ 0) (horth : inner ℝ K g = 0) (hgdef : g = !₂[R0 * FR0, GR0]) (hfreq : !₂[target / R0, pz] = representativeFrequency B sigma u L K g) (hM : 1 ≤ M) (hround : rounding ≤ 1) (hp : |p - target| ≤ rounding) (htarget : |target| ≤ M) (hpz : |pz| ≤ M) (hRi : |1 / R| ≤ M) (hR0i : |1 / R0| ≤ M) (hRd : |R - R0| ≤ diameter) (hFR : |FR| ≤ M) (hFZ : |FZ| ≤ M) (hGZ : |GZ| ≤ M) (hFR0 : |FR - FR0| ≤ base) (hGR0 : |GR - GR0| ≤ base) :

‖explicitNormal ε p pz (sigma * B * u / 2) R v FR GR FZ GZ - referenceNormal B sigma u L v K‖ ≤ |v| * (M * rounding + 2 * M * base) + M * rounding + M ^ 3 * diameter + 2 * (|B| * |sigma| * |u| / (|L| * ‖g‖)) + |ε| * |v| * (3 * M ^ 2)

The complete finite estimate starts from the chosen representative and the local derivatives of the actual base.

theorem NavierStokes.PhaseEstimates.phaseNormal_eq_explicit (ε p pz x0 : ℝ) (F G : Slow → ℝ) (q : PhaseCalculus.Slot) (hε : ε ≠ 0) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) :

PhaseCalculus.phaseNormal ε p pz x0 F G q = explicitNormal ε p pz x0 q.1.1 q.2.2 (PhaseCalculus.slowR F q.1) (PhaseCalculus.slowR G q.1) (PhaseCalculus.slowZ F q.1) (PhaseCalculus.slowZ G q.1)

noncomputable def NavierStokes.PhaseEstimates.phaseError (S ε k : ℝ) :

Phase error, given by 1 / S + S * ε ^ 2 + S / k + ε * S.

Equations

NavierStokes.PhaseEstimates.phaseError S ε k = 1 / S + S * ε ^ 2 + S / k + ε * S

Instances For

noncomputable def NavierStokes.PhaseEstimates.phaseConstant (M : ℝ) :

Phase constant, given by 8 * M ^ 3 + 2 * M ^ 4.

Equations

NavierStokes.PhaseEstimates.phaseConstant M = 8 * M ^ 3 + 2 * M ^ 4

Instances For

theorem NavierStokes.PhaseEstimates.inverse_cube_bounds {S : ℝ} (hS : 1 ≤ S) :

1 / S ^ 3 ≤ 1 / S ∧ S * (1 / S ^ 3) ≤ 1 / S

theorem NavierStokes.PhaseEstimates.representative_tilt_scaled {B sigma u L M S : ℝ} {g : Plane} (hM : 0 ≤ M) (hB : |B| ≤ M) (hsigma : |sigma| = 1) (hu : |u| ≤ M) (hg : 1 / ‖g‖ ≤ M) (hL : 1 / |L| ≤ M / S) :

|B| * |sigma| * |u| / (|L| * ‖g‖) ≤ M ^ 4 / S

theorem NavierStokes.PhaseEstimates.assembled_error_scaled {M S ε k v tilt : ℝ} (hM : 1 ≤ M) (hS : 1 ≤ S) (hk : 0 < k) (hε : 0 ≤ ε) (hv : |v| ≤ M * S) (htilt : tilt ≤ M ^ 4 / S) :

|v| * (M * (1 / k) + 2 * M * (M * (1 / S ^ 3 + ε ^ 2))) + M * (1 / k) + M ^ 3 * (1 / S ^ 3) + 2 * tilt + |ε| * |v| * (3 * M ^ 2) ≤ phaseConstant M * phaseError S ε k

A single algebraic estimate displays every long-slot loss.

theorem NavierStokes.PhaseEstimates.phaseError_le_four_div {S ε k : ℝ} (hS : 0 < S) (hε2 : S ^ 2 * ε ^ 2 ≤ 1) (hk2 : S ^ 2 / k ≤ 1) (hε1 : ε * S ^ 2 ≤ 1) :

phaseError S ε k ≤ 4 / S

noncomputable def NavierStokes.PhaseEstimates.normalVelocity (ε p pz FR GR FZ GZ : ℝ) :

Normal velocity, given by !₂[-(p * FR + pz * GR), 0, -ε * (p * FZ + pz * GZ)].

Equations

NavierStokes.PhaseEstimates.normalVelocity ε p pz FR GR FZ GZ = !₂[-(p * FR + pz * GR), 0, -ε * (p * FZ + pz * GZ)]

Instances For

theorem NavierStokes.PhaseEstimates.normalVelocity_bound {ε p pz FR GR FZ GZ slope error shear : ℝ} (herror : |p * FR + pz * GR - slope| ≤ error) (hshear : |p * FZ + pz * GZ| ≤ shear) :

‖normalVelocity ε p pz FR GR FZ GZ‖ ≤ |slope| + error + |ε| * shear

The slot derivative is estimated from its exact formula, independently of the estimate for the normal itself.

theorem NavierStokes.PhaseEstimates.representative_slope_scaled {B sigma u L M S : ℝ} (hM : 0 ≤ M) (hB : |B| ≤ M) (hsigma : |sigma| = 1) (hu : |u| ≤ M) (hL : 1 / |L| ≤ M / S) :

|-sigma * B * u / L| ≤ M ^ 3 / S

theorem NavierStokes.PhaseEstimates.velocity_error_scaled {M S ε k : ℝ} (hM : 1 ≤ M) (hS : 1 ≤ S) (hk : 0 < k) (hε : 0 ≤ ε) :

M ^ 3 / S + (M * (1 / k) + 2 * M * (M * (1 / S ^ 3 + ε ^ 2))) + |ε| * (3 * M ^ 2) ≤ phaseConstant M * phaseError S ε k

theorem NavierStokes.PhaseEstimates.rounded_normal_estimates {ε target pz R R0 v FR GR FZ GZ FR0 GR0 B sigma u L M S k : ℝ} {K g : Plane} (hR : R ≠ 0) (hR0 : R0 ≠ 0) (hg : g ≠ 0) (horth : inner ℝ K g = 0) (hgdef : g = !₂[R0 * FR0, GR0]) (hfreq : !₂[target / R0, pz] = representativeFrequency B sigma u L K g) (hM : 1 ≤ M) (hS : 1 ≤ S) (hk : 1 ≤ k) (hε : 0 ≤ ε) (htarget : |target| ≤ M) (hpz : |pz| ≤ M) (hB : |B| ≤ M) (hsigma : |sigma| = 1) (hu : |u| ≤ M) (hgi : 1 / ‖g‖ ≤ M) (hL : 1 / |L| ≤ M / S) (hv : |v| ≤ M * S) (hRi : |1 / R| ≤ M) (hR0i : |1 / R0| ≤ M) (hRd : |R - R0| ≤ 1 / S ^ 3) (hFR : |FR| ≤ M) (hFZ : |FZ| ≤ M) (hGZ : |GZ| ≤ M) (hFR0 : |FR - FR0| ≤ M * (1 / S ^ 3 + ε ^ 2)) (hGR0 : |GR - GR0| ≤ M * (1 / S ^ 3 + ε ^ 2)) :

‖explicitNormal ε (roundedFrequency k target) pz (sigma * B * u / 2) R v FR GR FZ GZ - referenceNormal B sigma u L v K‖ ≤ phaseConstant M * phaseError S ε k ∧ ‖normalVelocity ε (roundedFrequency k target) pz FR GR FZ GZ‖ ≤ phaseConstant M * phaseError S ε k

Quantitative estimates for the actual rounded phase. The C2 comparison lemma above supplies the two M (S⁻³ + ε²) derivative hypotheses.

Quantitative lower bounds and the actual normalized frame #

theorem NavierStokes.PhaseEstimates.tail_norm_le (n : Space) :

‖MovingFrameODE.tail n‖ ≤ ‖n‖

theorem NavierStokes.PhaseEstimates.normalScale_close {n : Space} {K : Plane} {B s δ : ℝ} (hB : 0 < B) (hK : ‖K‖ = 1) (hclose : ‖n - MovingFrameODE.pack (B * s) (B • K)‖ ≤ δ) :

|MovingFrameODE.normalScale n - B| ≤ δ

theorem NavierStokes.PhaseEstimates.normal_lower_bounds {n : Space} {K : Plane} {B s δ : ℝ} (hB : 0 < B) (hK : ‖K‖ = 1) (hδ : δ ≤ B / 2) (hclose : ‖n - MovingFrameODE.pack (B * s) (B • K)‖ ≤ δ) :

B / 2 ≤ MovingFrameODE.normalScale n ∧ B / 2 ≤ ‖n‖ ∧ MovingFrameODE.tail n ≠ 0 ∧ n ≠ 0

Closeness derived above controls the tangential normal as well as the full normal; the weaker full-normal lower bound alone would not build the frame.

theorem NavierStokes.PhaseEstimates.radialSlope_close {n : Space} {K : Plane} {B s δ : ℝ} (hB : 0 < B) (hK : ‖K‖ = 1) (hδ : δ ≤ B / 2) (hclose : ‖n - MovingFrameODE.pack (B * s) (B • K)‖ ≤ δ) :

|MovingFrameODE.radialSlope n - s| ≤ 2 * (1 + |s|) * δ / B

theorem NavierStokes.PhaseEstimates.normalDirection_close {n : Space} {K : Plane} {B s δ : ℝ} (hB : 0 < B) (hK : ‖K‖ = 1) (hδ : δ ≤ B / 2) (hclose : ‖n - MovingFrameODE.pack (B * s) (B • K)‖ ≤ δ) :

‖MovingFrameODE.normalDirection n - K‖ ≤ 4 * δ / B

theorem NavierStokes.PhaseEstimates.quarterTurn_norm (w : Plane) :

‖MovingFrameODE.quarterTurn w‖ = ‖w‖

theorem NavierStokes.PhaseEstimates.transverseDirection_close {n : Space} {K : Plane} {B s δ : ℝ} (hB : 0 < B) (hK : ‖K‖ = 1) (hδ : δ ≤ B / 2) (hclose : ‖n - MovingFrameODE.pack (B * s) (B • K)‖ ≤ δ) :

‖MovingFrameODE.quarterTurn (MovingFrameODE.normalDirection n) - MovingFrameODE.quarterTurn K‖ ≤ 4 * δ / B

noncomputable def NavierStokes.PhaseEstimates.scaleDerivative (n n' : Space) :

Scale derivative, given by ⟪MovingFrameODE.tail n, MovingFrameODE.tail n'⟫_ℝ / MovingFrameODE.normalScale n.

Equations

NavierStokes.PhaseEstimates.scaleDerivative n n' = inner ℝ (NavierStokes.MovingFrameODE.tail n) (NavierStokes.MovingFrameODE.tail n') / NavierStokes.MovingFrameODE.normalScale n

Instances For

noncomputable def NavierStokes.PhaseEstimates.slopeDerivative (n n' : Space) :

Slope derivative, given by (n' 0 - MovingFrameODE.radialSlope n * scaleDerivative n n') / MovingFrameODE.normalScale n.

Equations

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

Instances For

noncomputable def NavierStokes.PhaseEstimates.directionDerivative (n n' : Space) :

Direction derivative, given by (MovingFrameODE.normalScale n)⁻¹ • (MovingFrameODE.tail n' - scaleDerivative n n' • MovingFrameODE.normalDirection n).

Equations

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

Instances For

noncomputable def NavierStokes.PhaseEstimates.angularVelocity (n n' : Space) :

Angular velocity, given by ⟪MovingFrameODE.quarterTurn (MovingFrameODE.normalDirection n), directionDerivative n n'⟫_ℝ.

Equations

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

Instances For

theorem NavierStokes.PhaseEstimates.hasDerivAt_normalScale {n : ℝ → Space} {n' : Space} {v : ℝ} (hn : HasDerivAt n n' v) (hne : MovingFrameODE.tail (n v) ≠ 0) :

HasDerivAt (fun (s : ℝ) => MovingFrameODE.normalScale (n s)) (scaleDerivative (n v) n') v

theorem NavierStokes.PhaseEstimates.hasDerivAt_radialSlope {n : ℝ → Space} {n' : Space} {v : ℝ} (hn : HasDerivAt n n' v) (hne : MovingFrameODE.tail (n v) ≠ 0) :

HasDerivAt (fun (s : ℝ) => MovingFrameODE.radialSlope (n s)) (slopeDerivative (n v) n') v

theorem NavierStokes.PhaseEstimates.hasDerivAt_normalDirection {n : ℝ → Space} {n' : Space} {v : ℝ} (hn : HasDerivAt n n' v) (hne : MovingFrameODE.tail (n v) ≠ 0) :

HasDerivAt (fun (s : ℝ) => MovingFrameODE.normalDirection (n s)) (directionDerivative (n v) n') v

theorem NavierStokes.PhaseEstimates.hasDerivAt_actual_frame {n : ℝ → Space} {n' : Space} {v : ℝ} (hn : HasDerivAt n n' v) (hne : MovingFrameODE.tail (n v) ≠ 0) :

HasDerivAt (fun (s : ℝ) => MovingFrameODE.normalDirection (n s)) (angularVelocity (n v) n' • MovingFrameODE.quarterTurn (MovingFrameODE.normalDirection (n v))) v ∧ HasDerivAt (fun (s : ℝ) => MovingFrameODE.quarterTurn (MovingFrameODE.normalDirection (n s))) (-angularVelocity (n v) n' • MovingFrameODE.normalDirection (n v)) v

The angular speed is computed from the actual normal derivative.

theorem NavierStokes.PhaseEstimates.scaleDerivative_bound {n n' : Space} (hne : MovingFrameODE.tail n ≠ 0) :

|scaleDerivative n n'| ≤ ‖n'‖

theorem NavierStokes.PhaseEstimates.slopeDerivative_bound {n n' : Space} {B η : ℝ} (hB : 0 < B) (hlow : B / 2 ≤ MovingFrameODE.normalScale n) (hn' : ‖n'‖ ≤ η) :

|slopeDerivative n n'| ≤ 2 * (1 + |MovingFrameODE.radialSlope n|) * η / B

theorem NavierStokes.PhaseEstimates.directionDerivative_bound {n n' : Space} {B η : ℝ} (hB : 0 < B) (hlow : B / 2 ≤ MovingFrameODE.normalScale n) (hn' : ‖n'‖ ≤ η) :

‖directionDerivative n n'‖ ≤ 4 * η / B

theorem NavierStokes.PhaseEstimates.angularVelocity_bound {n n' : Space} {B η : ℝ} (hB : 0 < B) (hlow : B / 2 ≤ MovingFrameODE.normalScale n) (hn' : ‖n'‖ ≤ η) :

|angularVelocity n n'| ≤ 4 * η / B

The actual local base hypotheses #

structure NavierStokes.PhaseEstimates.LocalBaseBounds (F G F0 G0 : Slow → ℝ) (U : Set Slow) (M ε : ℝ) :

Local C1/C2 bounds on the given base and its order-zero limit. These are derivative bounds on actual functions, not a normal-comparison hypothesis.

convex : Convex ℝ U
actualF (x : Slow) : x ∈ U → DifferentiableAt ℝ F x
actualG (x : Slow) : x ∈ U → DifferentiableAt ℝ G x
referenceF (x : Slow) : x ∈ U → DifferentiableAt ℝ F0 x
referenceG (x : Slow) : x ∈ U → DifferentiableAt ℝ G0 x
secondF (x : Slow) : x ∈ U → DifferentiableAt ℝ (fderiv ℝ F0) x
secondG (x : Slow) : x ∈ U → DifferentiableAt ℝ (fderiv ℝ G0) x
secondF_bound (x : Slow) : x ∈ U → ‖fderiv ℝ (fderiv ℝ F0) x‖ ≤ M
secondG_bound (x : Slow) : x ∈ U → ‖fderiv ℝ (fderiv ℝ G0) x‖ ≤ M
firstF_bound (x : Slow) : x ∈ U → ‖fderiv ℝ F0 x‖ ≤ M
valueF_error (x : Slow) : x ∈ U → |F x - F0 x| ≤ M * ε ^ 2
firstF_error (x : Slow) : x ∈ U → ‖fderiv ℝ F x - fderiv ℝ F0 x‖ ≤ M * ε ^ 2
firstG_error (x : Slow) : x ∈ U → ‖fderiv ℝ G x - fderiv ℝ G0 x‖ ≤ M * ε ^ 2
radialF_bound (x : Slow) : x ∈ U → |PhaseCalculus.slowR F x| ≤ M
axialF_bound (x : Slow) : x ∈ U → |PhaseCalculus.slowZ F x| ≤ M
axialG_bound (x : Slow) : x ∈ U → |PhaseCalculus.slowZ G x| ≤ M

Instances For

theorem NavierStokes.PhaseEstimates.localBase_derivative_errors {F G F0 G0 : Slow → ℝ} {U : Set Slow} {M ε diameter : ℝ} {q q0 : Slow} (h : LocalBaseBounds F G F0 G0 U M ε) (hM : 0 ≤ M) (hq : q ∈ U) (hq0 : q0 ∈ U) (hd : ‖q - q0‖ ≤ diameter) :

|PhaseCalculus.slowR F q - PhaseCalculus.slowR F0 q0| ≤ M * (diameter + ε ^ 2) ∧ |PhaseCalculus.slowR G q - PhaseCalculus.slowR G0 q0| ≤ M * (diameter + ε ^ 2)

theorem NavierStokes.PhaseEstimates.localBase_value_error {F G F0 G0 : Slow → ℝ} {U : Set Slow} {M ε diameter : ℝ} {q q0 : Slow} (h : LocalBaseBounds F G F0 G0 U M ε) (hM : 0 ≤ M) (hq : q ∈ U) (hq0 : q0 ∈ U) (hd : ‖q - q0‖ ≤ diameter) :

|F q - F0 q0| ≤ M * (diameter + ε ^ 2)

theorem NavierStokes.PhaseEstimates.radius_difference_le {q q0 : Slow} {diameter : ℝ} (hd : ‖q - q0‖ ≤ diameter) :

|q.1 - q0.1| ≤ diameter

noncomputable def NavierStokes.PhaseEstimates.shearVector (F G : Slow → ℝ) (q : Slow) :

Shear vector, given by !₂[q.1 * PhaseCalculus.slowR F q, PhaseCalculus.slowR G q].

Equations

NavierStokes.PhaseEstimates.shearVector F G q = !₂[q.1 * NavierStokes.PhaseCalculus.slowR F q, NavierStokes.PhaseCalculus.slowR G q]

Instances For

theorem NavierStokes.PhaseEstimates.localBase_shear_error {F G F0 G0 : Slow → ℝ} {U : Set Slow} {M ε diameter : ℝ} {q q0 : Slow} (h : LocalBaseBounds F G F0 G0 U M ε) (hM : 1 ≤ M) (hq : q ∈ U) (hq0 : q0 ∈ U) (hd : ‖q - q0‖ ≤ diameter) (hR0 : |q0.1| ≤ M) :

‖shearVector F G q - shearVector F0 G0 q0‖ ≤ 4 * M ^ 2 * (diameter + ε ^ 2)

theorem NavierStokes.PhaseEstimates.actual_phase_estimates {F G F0 G0 : Slow → ℝ} {U : Set Slow} {q q0 : Slow} {ε target pz v θ B sigma u L M S k : ℝ} {K : Plane} (hbase : LocalBaseBounds F G F0 G0 U M ε) (hq : q ∈ U) (hq0 : q0 ∈ U) (hdiameter : ‖q - q0‖ ≤ 1 / S ^ 3) (hR : q.1 ≠ 0) (hR0 : q0.1 ≠ 0) (hg : shearVector F0 G0 q0 ≠ 0) (horth : inner ℝ K (shearVector F0 G0 q0) = 0) (hfreq : !₂[target / q0.1, pz] = representativeFrequency B sigma u L K (shearVector F0 G0 q0)) (hM : 1 ≤ M) (hS : 1 ≤ S) (hk : 1 ≤ k) (hε : 0 < ε) (htarget : |target| ≤ M) (hpz : |pz| ≤ M) (hB : |B| ≤ M) (hsigma : |sigma| = 1) (hu : |u| ≤ M) (hgi : 1 / ‖shearVector F0 G0 q0‖ ≤ M) (hL : 1 / |L| ≤ M / S) (hv : |v| ≤ M * S) (hRi : |1 / q.1| ≤ M) (hR0i : |1 / q0.1| ≤ M) :

‖PhaseCalculus.phaseNormal ε (roundedFrequency k target) pz (sigma * B * u / 2) F G (q, θ, v) - referenceNormal B sigma u L v K‖ ≤ phaseConstant M * phaseError S ε k ∧ ‖PhaseCalculus.normalSlotDerivative ε (roundedFrequency k target) pz F G q‖ ≤ phaseConstant M * phaseError S ε k

The principal estimate stated for the actual PhaseCalculus normal, with local C1/C2 hypotheses and the actual punctured-lattice rounded frequency.

theorem NavierStokes.PhaseEstimates.phase_normal_nonvanishing {ε k target pz x0 : ℝ} {F G : Slow → ℝ} {q : PhaseCalculus.Slot} (hε : ε ≠ 0) (hk : k ≠ 0) (hR : q.1.1 ≠ 0) (hF : DifferentiableAt ℝ F q.1) (hG : DifferentiableAt ℝ G q.1) :

MovingFrameODE.tail (PhaseCalculus.phaseNormal ε (roundedFrequency k target) pz x0 F G q) ≠ 0 ∧ PhaseCalculus.phaseNormal ε (roundedFrequency k target) pz x0 F G q ≠ 0

Punctured-lattice rounding itself already excludes exact zeros of the tangential normal; the comparison estimate supplies the uniform lower bound.

theorem NavierStokes.PhaseEstimates.actual_phase_geometry {F G F0 G0 : Slow → ℝ} {U : Set Slow} {q q0 : Slow} {ε target pz v θ B sigma u L M S k : ℝ} {K : Plane} (hbase : LocalBaseBounds F G F0 G0 U M ε) (hq : q ∈ U) (hq0 : q0 ∈ U) (hdiameter : ‖q - q0‖ ≤ 1 / S ^ 3) (hR : q.1 ≠ 0) (hR0 : q0.1 ≠ 0) (hg : shearVector F0 G0 q0 ≠ 0) (horth : inner ℝ K (shearVector F0 G0 q0) = 0) (hfreq : !₂[target / q0.1, pz] = representativeFrequency B sigma u L K (shearVector F0 G0 q0)) (hM : 1 ≤ M) (hS : 1 ≤ S) (hk : 1 ≤ k) (hε : 0 < ε) (htarget : |target| ≤ M) (hpz : |pz| ≤ M) (hB : |B| ≤ M) (hsigma : |sigma| = 1) (hu : |u| ≤ M) (hgi : 1 / ‖shearVector F0 G0 q0‖ ≤ M) (hL : 1 / |L| ≤ M / S) (hv : |v| ≤ M * S) (hRi : |1 / q.1| ≤ M) (hR0i : |1 / q0.1| ≤ M) (hBpos : 0 < B) (hK : ‖K‖ = 1) (hsmall : phaseConstant M * phaseError S ε k ≤ B / 2) :

have N := fun (w : ℝ) => PhaseCalculus.phaseNormal ε (roundedFrequency k target) pz (sigma * B * u / 2) F G (q, θ, w); have n' := PhaseCalculus.normalSlotDerivative ε (roundedFrequency k target) pz F G q; have δ := phaseConstant M * phaseError S ε k; HasDerivAt N n' v ∧ B / 2 ≤ MovingFrameODE.normalScale (N v) ∧ B / 2 ≤ ‖N v‖ ∧ MovingFrameODE.tail (N v) ≠ 0 ∧ N v ≠ 0 ∧ |MovingFrameODE.radialSlope (N v) - signedSlot sigma u L v| ≤ 2 * (1 + |signedSlot sigma u L v|) * δ / B ∧ ‖MovingFrameODE.normalDirection (N v) - K‖ ≤ 4 * δ / B ∧ ‖MovingFrameODE.quarterTurn (MovingFrameODE.normalDirection (N v)) - MovingFrameODE.quarterTurn K‖ ≤ 4 * δ / B ∧ |slopeDerivative (N v) n'| ≤ 2 * (1 + |MovingFrameODE.radialSlope (N v)|) * δ / B ∧ |angularVelocity (N v) n'| ≤ 4 * δ / B

The phase's actual derivative, uniform lower bounds and every changing frame quantity needed in MovingFrameODE, from local base and band data.

theorem NavierStokes.PhaseEstimates.signedSlot_bound {sigma u L v : ℝ} (hsigma : |sigma| = 1) (hu : 0 ≤ u) (hL : 0 < L) (hv : 0 ≤ v) (hvL : v ≤ L) :

|signedSlot sigma u L v| ≤ 3 * u / 2

theorem NavierStokes.PhaseEstimates.radialSlope_uniform_bound {n : Space} {K : Plane} {B s δ A : ℝ} (hB : 0 < B) (hK : ‖K‖ = 1) (hδ : δ ≤ B / 2) (hclose : ‖n - MovingFrameODE.pack (B * s) (B • K)‖ ≤ δ) (hs : |s| ≤ A) :

|MovingFrameODE.radialSlope n| ≤ 1 + 2 * A

theorem NavierStokes.PhaseEstimates.representative_uniform_frequency_bounds {B sigma u L M S R0 target pz : ℝ} {K g : Plane} (hR0 : R0 ≠ 0) (hM : 0 ≤ M) (hS : 1 ≤ S) (hB : |B| ≤ M) (hsigma : |sigma| = 1) (hu : |u| ≤ M) (hg : 1 / ‖g‖ ≤ M) (hL : 1 / |L| ≤ M / S) (hK : ‖K‖ = 1) (hRbound : |R0| ≤ M) (hfreq : !₂[target / R0, pz] = representativeFrequency B sigma u L K g) :

|target| ≤ M * (M + M ^ 4) ∧ |pz| ≤ M + M ^ 4

The representative frequencies are bounded uniformly before rounding; the bound follows from the specified frequency formula.

theorem NavierStokes.PhaseEstimates.chart_carrier_ge_one (h : ℝ) (n : ℕ) :

1 ≤ ↑(ChartScales.carrier h n)

theorem NavierStokes.PhaseEstimates.chart_S_tendsto_atTop :

Filter.Tendsto ChartScales.S Filter.atTop Filter.atTop

theorem NavierStokes.PhaseEstimates.eventually_band_conditions (h : ℝ) (hh : 0 < h) :

∀ᶠ (n : ℕ) in Filter.atTop , 1 ≤ ChartScales.S n ∧ ChartScales.S n ^ 2 * ChartScales.epsilon h n ^ 2 ≤ 1 ∧ ChartScales.S n ^ 2 / ↑(ChartScales.carrier h n) ≤ 1 ∧ ChartScales.epsilon h n * ChartScales.S n ^ 2 ≤ 1

The band conditions used in the finite estimate hold on the actual dyadic scale and actual ceiling-rounded carrier.

theorem NavierStokes.PhaseEstimates.eventually_phaseError_le (h : ℝ) (hh : 0 < h) :

∀ᶠ (n : ℕ) in Filter.atTop , phaseError (ChartScales.S n) (ChartScales.epsilon h n) ↑(ChartScales.carrier h n) ≤ 4 / ChartScales.S n

theorem NavierStokes.PhaseEstimates.eventually_error_small (h : ℝ) (hh : 0 < h) {C B : ℝ} (hC : 0 ≤ C) (hB : 0 < B) :

∀ᶠ (n : ℕ) in Filter.atTop , C * phaseError (ChartScales.S n) (ChartScales.epsilon h n) ↑(ChartScales.carrier h n) ≤ B / 2

Any fixed positive representative lower bound eventually dominates the derived normal error. This is a cutoff conclusion, not an assumed comparison.