Energy estimates for the viscous two-mode equation

The norm is the genuine Euclidean norm on EuclideanSpace ℝ (Fin 2). The auxiliary Hilbert-space lemmas derive an estimate from a differential equation and an energy inequality; no propagator bound is assumed.

theorem NavierStokes.ViscousPropagator.hasDerivWithinAt_norm_of_ne_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {u : ℝ → H} {u' : H} {s : Set ℝ} {t : ℝ} (hu : HasDerivWithinAt u u' s t) (hne : u t ≠ 0) : HasDerivWithinAt (fun (x : ℝ) => ‖u x‖) (inner ℝ (u t) u' / ‖u t‖) s t

Right derivative of the norm away from zero, obtained from the squared norm.

theorem NavierStokes.ViscousPropagator.norm_le_initial_add_integral {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {a b : ℝ} {u f : ℝ → H} (A : ℝ → H →L[ℝ] H) (hu : ContinuousOn u (Set.Icc a b)) (hf : Continuous f) (hode : ∀ t ∈ Set.Ico a b, HasDerivWithinAt u ((A t) (u t) + f t) (Set.Ici t) t) (hA : ∀ t ∈ Set.Ico a b, ∀ (x : H), inner ℝ x ((A t) x) ≤ 0) (t : ℝ) : t ∈ Set.Icc a b → ‖u t‖ ≤ ‖u a‖ + ∫ (s : ℝ) in a..t, ‖f s‖

A dissipative linear equation grows in norm by at most its integrated forcing. The equation is required only as a right derivative on the finite interval.

theorem NavierStokes.ViscousPropagator.weighted_norm_le_initial_add_integral {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {a b : ℝ} {u f : ℝ → H} (A : ℝ → H →L[ℝ] H) (growth W : ℝ → ℝ) (hWpos : ∀ (t : ℝ), 0 < W t) (hW : ∀ (t : ℝ), HasDerivAt W (growth t * W t) t) (hu : ContinuousOn u (Set.Icc a b)) (hf : Continuous f) (hode : ∀ t ∈ Set.Ico a b, HasDerivWithinAt u ((A t) (u t) + f t) (Set.Ici t) t) (hA : ∀ t ∈ Set.Ico a b, ∀ (x : H), inner ℝ x ((A t) x) ≤ growth t * ‖x‖ ^ 2) (t : ℝ) : t ∈ Set.Icc a b → ‖u t‖ / W t ≤ ‖u a‖ / W a + ∫ (s : ℝ) in a..t, ‖f s‖ / W s

Integrating-factor estimate from a quadratic-form bound on the actual operator. W is a positive scalar solution of W' = growth * W; it is not a bound assumed for the vector solution.

theorem NavierStokes.ViscousPropagator.norm_le_envelope_mul_integral {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {a b : ℝ} {u f : ℝ → H} (A : ℝ → H →L[ℝ] H) (rate P : ℝ → ℝ) {μ : ℝ} (hμ : 0 ≤ μ) (hPpos : ∀ (t : ℝ), 0 < P t) (hP : ∀ (t : ℝ), HasDerivAt P (rate t * P t) t) (hu : ContinuousOn u (Set.Icc a b)) (hf : Continuous f) (hode : ∀ t ∈ Set.Ico a b, HasDerivWithinAt u ((A t) (u t) + f t) (Set.Ici t) t) (hA : ∀ t ∈ Set.Ico a b, ∀ (x : H), inner ℝ x ((A t) x) ≤ (rate t + μ) * ‖x‖ ^ 2) (t : ℝ) : t ∈ Set.Icc a b → ‖u t‖ ≤ Real.exp (μ * (t - a)) * P t * (‖u a‖ / P a + ∫ (s : ℝ) in a..t, ‖f s‖ / P s)

The useful pulse bound: a positive envelope absorbs the variable reference growth, while the remaining nonnegative error contributes one exponential.

theorem NavierStokes.ViscousPropagator.norm_le_envelope_mul_integral_on {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {a b : ℝ} {u f : ℝ → H} (A : ℝ → H →L[ℝ] H) (rate P : ℝ → ℝ) {μ : ℝ} (hμ : 0 ≤ μ) (hPpos : ∀ (t : ℝ), 0 < P t) (hP : ∀ (t : ℝ), HasDerivAt P (rate t * P t) t) (hu : ContinuousOn u (Set.Icc a b)) (hf : ContinuousOn f (Set.Icc a b)) (hode : ∀ t ∈ Set.Ico a b, HasDerivWithinAt u ((A t) (u t) + f t) (Set.Ici t) t) (hA : ∀ t ∈ Set.Ico a b, ∀ (x : H), inner ℝ x ((A t) x) ≤ (rate t + μ) * ‖x‖ ^ 2) (t : ℝ) : t ∈ Set.Icc a b → ‖u t‖ ≤ Real.exp (μ * (t - a)) * P t * (‖u a‖ / P a + ∫ (s : ℝ) in a..t, ‖f s‖ / P s)

Interval-only forcing version. Clamping the source outside the interval shows that no global extension hypothesis on the forcing is needed.

theorem NavierStokes.ViscousPropagator.zero_initial_source_bound {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {a b K : ℝ} {u f : ℝ → H} (A : ℝ → H →L[ℝ] H) (rate P : ℝ → ℝ) {μ : ℝ} (hμ : 0 ≤ μ) (hPpos : ∀ (t : ℝ), 0 < P t) (hP : ∀ (t : ℝ), HasDerivAt P (rate t * P t) t) (hu : ContinuousOn u (Set.Icc a b)) (hf : ContinuousOn f (Set.Icc a b)) (hode : ∀ t ∈ Set.Ico a b, HasDerivWithinAt u ((A t) (u t) + f t) (Set.Ici t) t) (hA : ∀ t ∈ Set.Ico a b, ∀ (x : H), inner ℝ x ((A t) x) ≤ (rate t + μ) * ‖x‖ ^ 2) (hinit : u a = 0) (hsource : ∀ t ∈ Set.Icc a b, ‖f t‖ ≤ K * P t) (t : ℝ) : t ∈ Set.Icc a b → ‖u t‖ ≤ Real.exp (μ * (t - a)) * P t * (K * (t - a))

A source bounded by K * P retains that envelope and costs at most the slot length. The scalar K may be any prescribed small-scale power times weights.

theorem NavierStokes.ViscousPropagator.exists_solution_with_envelope_bound {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} (hab : a ≤ b) (A : ℝ → H →L[ℝ] H) (f : ℝ → H) (rate P : ℝ → ℝ) {μ : ℝ} (hμ : 0 ≤ μ) (hPpos : ∀ (t : ℝ), 0 < P t) (hP : ∀ (t : ℝ), HasDerivAt P (rate t * P t) t) (hcA : ContinuousOn A (Set.Icc a b)) (hcf : ContinuousOn f (Set.Icc a b)) (hA : ∀ t ∈ Set.Ico a b, ∀ (x : H), inner ℝ x ((A t) x) ≤ (rate t + μ) * ‖x‖ ^ 2) (x₀ : H) : ∃ (u : ℝ → H), u a = x₀ ∧ (∀ t ∈ Set.Icc a b, HasDerivAt u ((A t) (u t) + f t) t) ∧ ∀ t ∈ Set.Icc a b, ‖u t‖ ≤ Real.exp (μ * (t - a)) * P t * (‖x₀‖ / P a + ∫ (s : ℝ) in a..t, ‖f s‖ / P s)

Existence and the weighted estimate are compatible consequences of the actual continuous-coefficient ODE, with no assumed propagator.

@[reducible, inline]

abbrev NavierStokes.ViscousPropagator.Plane : Type

The two real modal coordinates with their Euclidean, not product-sup, norm.

Equations

• NavierStokes.ViscousPropagator.Plane = EuclideanSpace ℝ (Fin 2)

noncomputable def NavierStokes.ViscousPropagator.reflection : Plane →L[ℝ] Plane

Reflection in the growing coordinate.

Equations

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

noncomputable def NavierStokes.ViscousPropagator.diagonal (lam : ℝ) : Plane →L[ℝ] Plane

diag(lam,-lam) as a genuine continuous linear operator.

Equations

• NavierStokes.ViscousPropagator.diagonal lam = lam • NavierStokes.ViscousPropagator.reflection

noncomputable def NavierStokes.ViscousPropagator.coefficient (lam damping : ℝ) (E : Plane →L[ℝ] Plane) : Plane →L[ℝ] Plane

The actual diagonalized coefficient, including scalar damping and error.

Equations

• NavierStokes.ViscousPropagator.coefficient lam damping E = NavierStokes.ViscousPropagator.diagonal lam - damping • ContinuousLinearMap.id ℝ NavierStokes.ViscousPropagator.Plane + E

theorem NavierStokes.ViscousPropagator.plane_norm_sq (x : Plane) : ‖x‖ ^ 2 = x.ofLp 0 ^ 2 + x.ofLp 1 ^ 2

theorem NavierStokes.ViscousPropagator.inner_diagonal (lam : ℝ) (x : Plane) : inner ℝ x ((diagonal lam) x) = lam * (x.ofLp 0 ^ 2 - x.ofLp 1 ^ 2)

theorem NavierStokes.ViscousPropagator.diagonal_energy_le {lam : ℝ} (hlam : 0 ≤ lam) (x : Plane) : inner ℝ x ((diagonal lam) x) ≤ lam * ‖x‖ ^ 2

theorem NavierStokes.ViscousPropagator.error_energy_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (E : H →L[ℝ] H) (x : H) : inner ℝ x (E x) ≤ ‖E‖ * ‖x‖ ^ 2

Operator norm controls its quadratic form without losing the sign of damping.

theorem NavierStokes.ViscousPropagator.coefficient_energy_le {lam : ℝ} (hlam : 0 ≤ lam) (damping : ℝ) (E : Plane →L[ℝ] Plane) (x : Plane) : inner ℝ x ((coefficient lam damping E) x) ≤ (lam - damping + ‖E‖) * ‖x‖ ^ 2

Energy bound for the actual two-mode coefficient.

theorem NavierStokes.ViscousPropagator.hasDerivAt_envelope {rate : ℝ → ℝ} (hrate : Continuous rate) (midpoint t : ℝ) : HasDerivAt (GaussianEnvelope.envelope rate midpoint) (rate t * GaussianEnvelope.envelope rate midpoint t) t

The exponential-integral envelope has the required scalar ODE exactly.

theorem NavierStokes.ViscousPropagator.viscous_propagator_estimate {a b midpoint S dampingError matrixError : ℝ} (hS : 0 < S) (hdampingError : 0 ≤ dampingError) (hmatrixError : 0 ≤ matrixError) (lam damping referenceDamping rate : ℝ → ℝ) (E : ℝ → Plane →L[ℝ] Plane) {u f : ℝ → Plane} (hrate : Continuous rate) (hreference : ∀ t ∈ Set.Ico a b, rate t = lam t - referenceDamping t) (hlam : ∀ t ∈ Set.Ico a b, 0 ≤ lam t) (hdamping : ∀ t ∈ Set.Ico a b, referenceDamping t - dampingError / S ≤ damping t) (hE : ∀ t ∈ Set.Ico a b, ‖E t‖ ≤ matrixError / S) (hu : ContinuousOn u (Set.Icc a b)) (hf : ContinuousOn f (Set.Icc a b)) (hode : ∀ t ∈ Set.Ico a b, HasDerivWithinAt u ((coefficient (lam t) (damping t) (E t)) (u t) + f t) (Set.Ici t) t) (t : ℝ) : t ∈ Set.Icc a b → ‖u t‖ ≤ Real.exp ((dampingError + matrixError) / S * (t - a)) * GaussianEnvelope.envelope rate midpoint t * (‖u a‖ / GaussianEnvelope.envelope rate midpoint a + ∫ (s : ℝ) in a..t, ‖f s‖ / GaussianEnvelope.envelope rate midpoint s)

The actual viscous two-mode estimate. The damping may be smaller than the reference by dampingError / S, and the full operator error is at most matrixError / S. Neither error is multiplied by the harmonic index.

theorem NavierStokes.ViscousPropagator.high_harmonic_damping {j : ℤ} (hj : j ≠ 0) {D d δ : ℝ} (hD : 0 ≤ D) (hd : d - δ ≤ D) : d - δ ≤ ↑j ^ 2 * D

A nonzero integer harmonic only increases nonnegative fundamental damping.

theorem NavierStokes.ViscousPropagator.high_harmonic_propagator_estimate {a b midpoint S dampingError matrixError : ℝ} (hS : 0 < S) (hdampingError : 0 ≤ dampingError) (hmatrixError : 0 ≤ matrixError) (lam fundamentalDamping referenceDamping rate : ℝ → ℝ) (E : ℝ → Plane →L[ℝ] Plane) {u f : ℝ → Plane} {j : ℤ} (hj : j ≠ 0) (hrate : Continuous rate) (hreference : ∀ t ∈ Set.Ico a b, rate t = lam t - referenceDamping t) (hlam : ∀ t ∈ Set.Ico a b, 0 ≤ lam t) (hD : ∀ t ∈ Set.Ico a b, 0 ≤ fundamentalDamping t) (hdamping : ∀ t ∈ Set.Ico a b, referenceDamping t - dampingError / S ≤ fundamentalDamping t) (hE : ∀ t ∈ Set.Ico a b, ‖E t‖ ≤ matrixError / S) (hu : ContinuousOn u (Set.Icc a b)) (hf : ContinuousOn f (Set.Icc a b)) (hode : ∀ t ∈ Set.Ico a b, HasDerivWithinAt u ((coefficient (lam t) (↑j ^ 2 * fundamentalDamping t) (E t)) (u t) + f t) (Set.Ici t) t) (t : ℝ) : t ∈ Set.Icc a b → ‖u t‖ ≤ Real.exp ((dampingError + matrixError) / S * (t - a)) * GaussianEnvelope.envelope rate midpoint t * (‖u a‖ / GaussianEnvelope.envelope rate midpoint a + ∫ (s : ℝ) in a..t, ‖f s‖ / GaussianEnvelope.envelope rate midpoint s)

The same constants work for every nonzero harmonic.

theorem NavierStokes.ViscousPropagator.homogeneous_viscous_propagator_estimate {a b midpoint S dampingError matrixError : ℝ} (hS : 0 < S) (hdampingError : 0 ≤ dampingError) (hmatrixError : 0 ≤ matrixError) (lam damping referenceDamping rate : ℝ → ℝ) (E : ℝ → Plane →L[ℝ] Plane) {u : ℝ → Plane} (hrate : Continuous rate) (hreference : ∀ t ∈ Set.Ico a b, rate t = lam t - referenceDamping t) (hlam : ∀ t ∈ Set.Ico a b, 0 ≤ lam t) (hdamping : ∀ t ∈ Set.Ico a b, referenceDamping t - dampingError / S ≤ damping t) (hE : ∀ t ∈ Set.Ico a b, ‖E t‖ ≤ matrixError / S) (hu : ContinuousOn u (Set.Icc a b)) (hode : ∀ t ∈ Set.Ico a b, HasDerivWithinAt u ((coefficient (lam t) (damping t) (E t)) (u t)) (Set.Ici t) t) (t : ℝ) : t ∈ Set.Icc a b → ‖u t‖ ≤ Real.exp ((dampingError + matrixError) / S * |t - a|) * (GaussianEnvelope.envelope rate midpoint t / GaussianEnvelope.envelope rate midpoint a) * ‖u a‖

Homogeneous forward bound in the usual envelope-ratio form.

noncomputable def NavierStokes.ViscousPropagator.referenceEigenvalue (lam u ell t : ℝ) : ℝ

The positive reference eigenvalue appearing in the Gaussian construction.

Equations

• NavierStokes.ViscousPropagator.referenceEigenvalue lam u ell t = lam / √(1 + NavierStokes.PulseGrowth.slotMagnitude u ell t ^ 2)

noncomputable def NavierStokes.ViscousPropagator.referenceViscosity (lam u ell t : ℝ) : ℝ

The fundamental damping fixed by the manuscript's choice of B_s.

Equations

• NavierStokes.ViscousPropagator.referenceViscosity lam u ell t = lam * (1 + NavierStokes.PulseGrowth.slotMagnitude u ell t ^ 2) / ((1 + u ^ 2) * √(1 + u ^ 2))

theorem NavierStokes.ViscousPropagator.reference_rate_split (lam u ell t : ℝ) : GaussianEnvelope.referenceRate lam u ell t = referenceEigenvalue lam u ell t - referenceViscosity lam u ell t

theorem NavierStokes.ViscousPropagator.referenceEigenvalue_nonneg {lam : ℝ} (hlam : 0 ≤ lam) (u ell t : ℝ) : 0 ≤ referenceEigenvalue lam u ell t

theorem NavierStokes.ViscousPropagator.continuous_referenceRate (lam u ell : ℝ) : Continuous (GaussianEnvelope.referenceRate lam u ell)

theorem NavierStokes.ViscousPropagator.reference_pulse_propagator_estimate {a b S dampingError matrixError lam₀ u₀ ell : ℝ} (hS : 0 < S) (hdampingError : 0 ≤ dampingError) (hmatrixError : 0 ≤ matrixError) (hlam₀ : 0 ≤ lam₀) (damping : ℝ → ℝ) (E : ℝ → Plane →L[ℝ] Plane) {u f : ℝ → Plane} (hdamping : ∀ t ∈ Set.Ico a b, referenceViscosity lam₀ u₀ ell t - dampingError / S ≤ damping t) (hE : ∀ t ∈ Set.Ico a b, ‖E t‖ ≤ matrixError / S) (hu : ContinuousOn u (Set.Icc a b)) (hf : ContinuousOn f (Set.Icc a b)) (hode : ∀ t ∈ Set.Ico a b, HasDerivWithinAt u ((coefficient (referenceEigenvalue lam₀ u₀ ell t) (damping t) (E t)) (u t) + f t) (Set.Ici t) t) : have P := GaussianEnvelope.envelope (GaussianEnvelope.referenceRate lam₀ u₀ ell) (ell / 2); ∀ t ∈ Set.Icc a b, ‖u t‖ ≤ Real.exp ((dampingError + matrixError) / S * (t - a)) * P t * (‖u a‖ / P a + ∫ (s : ℝ) in a..t, ‖f s‖ / P s)

Concrete specialization to the same scalar reference used by GaussianEnvelope.reference_gaussian_bounds.

theorem NavierStokes.ViscousPropagator.fundamental_damping_nonneg {H : Type u_1} [NormedAddCommGroup H] {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (k : ℝ) (n : H) : 0 ≤ epsilon * k ^ 2 * ‖n‖ ^ 2

The physical viscosity coefficient is nonnegative.

theorem NavierStokes.ViscousPropagator.slot_exponential_bound {C S L a t : ℝ} (hC : 0 ≤ C) (hS : 0 < S) (hslot : t - a ≤ L * S) : Real.exp (C / S * (t - a)) ≤ Real.exp (C * L)

On a slot of length at most L * S, the error exponential is uniformly bounded independently of the small scale and of the harmonic index.