Gaussian bounds from a decreasing instantaneous rate

The integral is oriented: a point before the midpoint reverses the integration limits. The main theorem proves the same quadratic bounds on both sides, under local differentiability and derivative bounds on a convex domain.

Reference pulse growth

This file verifies the scalar reference growth calculation in Lemma 8.5 and Proposition A.4 of the supplied manuscript. The denominator (1 + u^2)^(3/2) is written as (1 + u^2) * sqrt (1 + u^2) to avoid fractional-power notation. These results do not assert bounds on the actual variable-coefficient ODE or on its parameter derivatives.

noncomputable def NavierStokes.PulseGrowth.netGrowth (lam u s : ℝ) : ℝ

Scalar growth of the positive reference mode after the chosen viscous damping.

Equations

• NavierStokes.PulseGrowth.netGrowth lam u s = lam / √(1 + s ^ 2) - lam * (1 + s ^ 2) / ((1 + u ^ 2) * √(1 + u ^ 2))

theorem NavierStokes.PulseGrowth.one_add_sq_pos (s : ℝ) : 0 < 1 + s ^ 2

theorem NavierStokes.PulseGrowth.radius_pos (s : ℝ) : 0 < √(1 + s ^ 2)

theorem NavierStokes.PulseGrowth.dampingDenominator_pos (u : ℝ) : 0 < (1 + u ^ 2) * √(1 + u ^ 2)

theorem NavierStokes.PulseGrowth.dampingDenominator_eq_radius_cube (u : ℝ) : (1 + u ^ 2) * √(1 + u ^ 2) = √(1 + u ^ 2) ^ 3

The three-halves denominator is the cube of the positive square root.

theorem NavierStokes.PulseGrowth.reference_eigenvalue_square (lam s : ℝ) : (lam / √(1 + s ^ 2)) ^ 2 = lam ^ 2 / (1 + s ^ 2)

Squaring the proposed positive eigenvalue gives the reference discriminant.

theorem NavierStokes.PulseGrowth.reference_characteristic_equation {a b lam s : ℝ} (hdisc : lam ^ 2 = a * b) : (lam / √(1 + s ^ 2)) ^ 2 - a / (1 + s ^ 2) * b = 0

Characteristic equation for the two off-diagonal reference coefficients.

Here a = 2 F₀ Nθ and b = -(2 F₀ Nθ + |g₀|) in the manuscript. The hypothesis is the manuscript's definition of the squared reference rate; its positivity from the geometric cone is not assumed to have been established.

theorem NavierStokes.PulseGrowth.netGrowth_even (lam u s : ℝ) : netGrowth lam u (-s) = netGrowth lam u s

Reversing the sign of the slot parameter does not change the growth.

theorem NavierStokes.PulseGrowth.netGrowth_at_threshold (lam u : ℝ) : netGrowth lam u u = 0

The prescribed damping exactly cancels growth at the threshold.

theorem NavierStokes.PulseGrowth.netGrowth_strictAnti_sq {lam u s t : ℝ} (hlam : 0 < lam) (hst : s ^ 2 < t ^ 2) : netGrowth lam u t < netGrowth lam u s

Strict decrease in squared distance from zero, for a positive reference rate.

theorem NavierStokes.PulseGrowth.netGrowth_eq_of_sq_eq {lam u s t : ℝ} (hst : s ^ 2 = t ^ 2) : netGrowth lam u s = netGrowth lam u t

theorem NavierStokes.PulseGrowth.netGrowth_pos_of_abs_lt {lam u s : ℝ} (hlam : 0 < lam) (hs : |s| < |u|) : 0 < netGrowth lam u s

Growth is positive strictly inside either threshold.

theorem NavierStokes.PulseGrowth.netGrowth_zero_of_abs_eq {lam u s : ℝ} (hs : |s| = |u|) : netGrowth lam u s = 0

Growth vanishes at both signed thresholds.

theorem NavierStokes.PulseGrowth.netGrowth_neg_of_abs_gt {lam u s : ℝ} (hlam : 0 < lam) (hs : |u| < |s|) : netGrowth lam u s < 0

Growth is negative outside either threshold.

theorem NavierStokes.PulseGrowth.netGrowth_sign {lam u s : ℝ} (hlam : 0 < lam) : (0 < netGrowth lam u s ↔ |s| < |u|) ∧ (netGrowth lam u s = 0 ↔ |s| = |u|) ∧ (netGrowth lam u s < 0 ↔ |u| < |s|)

A complete positive/zero/negative classification for a positive reference rate.

theorem NavierStokes.PulseGrowth.netGrowth_strictAntiOn_nonneg {lam u : ℝ} (hlam : 0 < lam) : StrictAntiOn (netGrowth lam u) (Set.Ici 0)

For positive magnitudes the reference growth is strictly decreasing.

noncomputable def NavierStokes.PulseGrowth.slotMagnitude (u ell v : ℝ) : ℝ

Magnitude of either signed schedule, in the slot-time variable.

Equations

• NavierStokes.PulseGrowth.slotMagnitude u ell v = u / 2 + u * v / ell

theorem NavierStokes.PulseGrowth.slotMagnitude_midpoint (u ell : ℝ) (hell : ell ≠ 0) : slotMagnitude u ell (ell / 2) = u

theorem NavierStokes.PulseGrowth.slotMagnitude_nonneg {u ell v : ℝ} (hu : 0 ≤ u) (hell : 0 < ell) (hv : 0 ≤ v) : 0 ≤ slotMagnitude u ell v

theorem NavierStokes.PulseGrowth.slotMagnitude_lt_threshold {u ell v : ℝ} (hu : 0 < u) (hell : 0 < ell) (hv : v < ell / 2) : slotMagnitude u ell v < u

theorem NavierStokes.PulseGrowth.slotMagnitude_gt_threshold {u ell v : ℝ} (hu : 0 < u) (hell : 0 < ell) (hv : ell / 2 < v) : u < slotMagnitude u ell v

theorem NavierStokes.PulseGrowth.netGrowth_slot_positive {lam u ell v : ℝ} (hlam : 0 < lam) (hu : 0 < u) (hell : 0 < ell) (hv : 0 ≤ v) (hmid : v < ell / 2) : 0 < netGrowth lam u (slotMagnitude u ell v)

Positive reference growth on the first half of a slot.

theorem NavierStokes.PulseGrowth.netGrowth_slot_midpoint (lam u ell : ℝ) (hell : ell ≠ 0) : netGrowth lam u (slotMagnitude u ell (ell / 2)) = 0

Zero reference growth at the slot midpoint.

theorem NavierStokes.PulseGrowth.netGrowth_slot_negative {lam u ell v : ℝ} (hlam : 0 < lam) (hu : 0 < u) (hell : 0 < ell) (hmid : ell / 2 < v) : netGrowth lam u (slotMagnitude u ell v) < 0

Negative reference growth on the second half of a slot (and beyond).

noncomputable def NavierStokes.GaussianEnvelope.envelope (rate : ℝ → ℝ) (midpoint time : ℝ) : ℝ

Envelope normalized to one at the midpoint.

Equations

• NavierStokes.GaussianEnvelope.envelope rate midpoint time = Real.exp (∫ (x : ℝ) in midpoint..time, rate x)

theorem NavierStokes.GaussianEnvelope.integral_centered_linear (k midpoint a b : ℝ) : ∫ (x : ℝ) in a..b, k * (x - midpoint) = k * ((b - midpoint) ^ 2 - (a - midpoint) ^ 2) / 2

Exact integral of a centered affine rate, for either order of the endpoints.

theorem NavierStokes.GaussianEnvelope.integral_quadratic_bounds {D : Set ℝ} {rate : ℝ → ℝ} {midpoint time lower upper : ℝ} (hD : Convex ℝ D) (hcont : ContinuousOn rate D) (hdiff : DifferentiableOn ℝ rate (interior D)) (hderiv : ∀ x ∈ interior D, lower ≤ deriv rate x ∧ deriv rate x ≤ upper) (hm : midpoint ∈ D) (ht : time ∈ D) (hzero : rate midpoint = 0) : lower * (time - midpoint) ^ 2 / 2 ≤ ∫ (x : ℝ) in midpoint..time, rate x ∧ ∫ (x : ℝ) in midpoint..time, rate x ≤ upper * (time - midpoint) ^ 2 / 2

Local derivative bounds integrate to a quadratic sandwich around a zero of the rate.

No ordering of midpoint and time is assumed. In the backwards case, both the pointwise comparison and the oriented integral reverse order.

theorem NavierStokes.GaussianEnvelope.gaussian_envelope_bounds {D : Set ℝ} {rate : ℝ → ℝ} {midpoint time c C ell : ℝ} (hD : Convex ℝ D) (hcont : ContinuousOn rate D) (hdiff : DifferentiableOn ℝ rate (interior D)) (hderiv : ∀ x ∈ interior D, -C / ell ≤ deriv rate x ∧ deriv rate x ≤ -c / ell) (hm : midpoint ∈ D) (ht : time ∈ D) (hzero : rate midpoint = 0) : Real.exp (-C * (time - midpoint) ^ 2 / (2 * ell)) ≤ envelope rate midpoint time ∧ envelope rate midpoint time ≤ Real.exp (-c * (time - midpoint) ^ 2 / (2 * ell))

Gaussian upper and lower bounds with the manuscript's slot-length normalization.

@[simp]

theorem NavierStokes.GaussianEnvelope.envelope_at_midpoint (rate : ℝ → ℝ) (midpoint : ℝ) : envelope rate midpoint midpoint = 1

theorem NavierStokes.GaussianEnvelope.envelope_pos (rate : ℝ → ℝ) (midpoint time : ℝ) : 0 < envelope rate midpoint time

theorem NavierStokes.GaussianEnvelope.envelope_lt_one_away_from_midpoint {D : Set ℝ} {rate : ℝ → ℝ} {midpoint time c C ell : ℝ} (hD : Convex ℝ D) (hcont : ContinuousOn rate D) (hdiff : DifferentiableOn ℝ rate (interior D)) (hderiv : ∀ x ∈ interior D, -C / ell ≤ deriv rate x ∧ deriv rate x ≤ -c / ell) (hm : midpoint ∈ D) (ht : time ∈ D) (hzero : rate midpoint = 0) (hc : 0 < c) (hell : 0 < ell) (hne : time ≠ midpoint) : envelope rate midpoint time < 1

For positive c and slot length the midpoint is the unique maximum on the domain.

noncomputable def NavierStokes.GaussianEnvelope.referenceSlope (lam u s : ℝ) : ℝ

Derivative of the manuscript's scalar reference rate in its magnitude variable.

Equations

• NavierStokes.GaussianEnvelope.referenceSlope lam u s = -lam * s / ((1 + s ^ 2) * √(1 + s ^ 2)) - 2 * lam * s / ((1 + u ^ 2) * √(1 + u ^ 2))

theorem NavierStokes.GaussianEnvelope.hasDerivAt_netGrowth (lam u s : ℝ) : HasDerivAt (PulseGrowth.netGrowth lam u) (referenceSlope lam u s) s

The displayed rate derivative is an actual derivative, including at zero.

noncomputable def NavierStokes.GaussianEnvelope.referenceMinSlope (lam u : ℝ) : ℝ

A positive lower bound on the magnitude of the rate derivative in the slot.

Equations

• NavierStokes.GaussianEnvelope.referenceMinSlope lam u = lam * u / ((1 + u ^ 2) * √(1 + u ^ 2))

noncomputable def NavierStokes.GaussianEnvelope.referenceMaxSlope (lam u : ℝ) : ℝ

An upper bound on the magnitude of the rate derivative in the slot.

Equations

• NavierStokes.GaussianEnvelope.referenceMaxSlope lam u = 3 * lam * u / 2 + 3 * lam * u / ((1 + u ^ 2) * √(1 + u ^ 2))

theorem NavierStokes.GaussianEnvelope.referenceMinSlope_pos {lam u : ℝ} (hlam : 0 < lam) (hu : 0 < u) : 0 < referenceMinSlope lam u

theorem NavierStokes.GaussianEnvelope.referenceMaxSlope_pos {lam u : ℝ} (hlam : 0 < lam) (hu : 0 < u) : 0 < referenceMaxSlope lam u

theorem NavierStokes.GaussianEnvelope.referenceSlope_bounds {lam u s : ℝ} (hlam : 0 < lam) (hu : 0 < u) (hs : s ∈ Set.Icc (u / 2) (3 * u / 2)) : -referenceMaxSlope lam u ≤ referenceSlope lam u s ∧ referenceSlope lam u s ≤ -referenceMinSlope lam u

Explicit, slot-length-independent bounds on the reference derivative.

noncomputable def NavierStokes.GaussianEnvelope.referenceRate (lam u ell time : ℝ) : ℝ

The reference rate expressed in slot time.

Equations

• NavierStokes.GaussianEnvelope.referenceRate lam u ell time = NavierStokes.PulseGrowth.netGrowth lam u (NavierStokes.PulseGrowth.slotMagnitude u ell time)

theorem NavierStokes.GaussianEnvelope.hasDerivAt_referenceRate (lam u ell time : ℝ) : HasDerivAt (referenceRate lam u ell) (referenceSlope lam u (PulseGrowth.slotMagnitude u ell time) * (u / ell)) time

theorem NavierStokes.GaussianEnvelope.slotMagnitude_mem_interval {u ell time : ℝ} (hu : 0 ≤ u) (hell : 0 < ell) (ht : time ∈ Set.Icc 0 ell) : PulseGrowth.slotMagnitude u ell time ∈ Set.Icc (u / 2) (3 * u / 2)

theorem NavierStokes.GaussianEnvelope.referenceRate_deriv_bounds {lam u ell time : ℝ} (hlam : 0 < lam) (hu : 0 < u) (hell : 0 < ell) (ht : time ∈ Set.Icc 0 ell) : -(u * referenceMaxSlope lam u) / ell ≤ deriv (referenceRate lam u ell) time ∧ deriv (referenceRate lam u ell) time ≤ -(u * referenceMinSlope lam u) / ell

Bounds on the derivative in slot time, uniformly for all positive slot lengths.

theorem NavierStokes.GaussianEnvelope.reference_gaussian_bounds {lam u ell time : ℝ} (hlam : 0 < lam) (hu : 0 < u) (hell : 0 < ell) (ht : time ∈ Set.Icc 0 ell) : Real.exp (-(u * referenceMaxSlope lam u) * (time - ell / 2) ^ 2 / (2 * ell)) ≤ envelope (referenceRate lam u ell) (ell / 2) time ∧ envelope (referenceRate lam u ell) (ell / 2) time ≤ Real.exp (-(u * referenceMinSlope lam u) * (time - ell / 2) ^ 2 / (2 * ell))

Two-sided Gaussian bounds for the actual scalar reference envelope.

All analytic hypotheses of gaussian_envelope_bounds are proved here from the explicit reference formula. The constants depend on lam and u, not ell.

theorem NavierStokes.GaussianEnvelope.reference_uniform_gaussian_bounds {lam u : ℝ} (hlam : 0 < lam) (hu : 0 < u) : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ 0 < C ∧ ∀ (ell : ℝ), 0 < ell → ∀ time ∈ Set.Icc 0 ell, Real.exp (-C * (time - ell / 2) ^ 2 / ell) ≤ envelope (referenceRate lam u ell) (ell / 2) time ∧ envelope (referenceRate lam u ell) (ell / 2) time ≤ Real.exp (-c * (time - ell / 2) ^ 2 / ell)

The reference envelope has positive Gaussian constants uniform in slot length.