Carleman Gauss Weights

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.gaussCarlemanTimeWeight (t : ℝ) : ℝ

The time factor in the Gaussian weight from prop:carleman-gauss of the Escauriaza–Seregin–Šverák manuscript.

Equations

• CKN.gaussCarlemanTimeWeight t = t * Real.exp ((1 - t) / 3)

noncomputable def CKN.gaussCarlemanPhase (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) : ℝ

The logarithmic Gaussian phase used in the proof of prop:carleman-gauss (ESS).

Equations

• CKN.gaussCarlemanPhase q z = -(8 * z.2)⁻¹ • ∑ i : Fin 3, z.1 i ^ 2 - q * Real.log (CKN.gaussCarlemanTimeWeight z.2)

theorem CKN.vec3_coordDeriv (x : Foundation.Parabolic.Vec3) (j : Fin 3) : fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => y j) x = ContinuousLinearMap.proj j

The derivative of a coordinate function on Vec3 is the coordinate projection.

theorem CKN.vec3_coordSqDeriv (x : Foundation.Parabolic.Vec3) (j i : Fin 3) : (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => y j ^ 2) x) (basisVec i) = if j = i then 2 * x j else 0

The directional derivative of a squared coordinate on Vec3.

theorem CKN.gaussCarlemanPhase_spatialPartial (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) (i : Fin 3) : spatialPartial (gaussCarlemanPhase q) i z = -z.1 i / (4 * z.2)

The spatial derivative of the Gaussian phase, used in the explicit weight calculation for prop:carleman-gauss (ESS).

theorem CKN.gaussCarlemanPhase_timePartial (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) : timePartial (gaussCarlemanPhase q) z = (∑ i : Fin 3, z.1 i ^ 2) / (8 * z.2 ^ 2) - q * (1 / z.2 - 1 / 3)

The time derivative of the Gaussian phase on positive time, used in the weight calculation for prop:carleman-gauss (ESS).

theorem CKN.gaussTimeRatio_sq_bounds {t : ℝ} (ht0 : 0 < t) (ht2 : t < 2) : Real.exp (-(2 / 3)) ≤ (t / (t * Real.exp ((1 - t) / 3))) ^ 2 ∧ (t / (t * Real.exp ((1 - t) / 3))) ^ 2 ≤ Real.exp (2 / 3)

The time comparison used to return from the Gaussian conjugation to the original weight in prop:carleman-gauss (ESS).

theorem CKN.gaussTimeWeight_div_sq_bounds {t : ℝ} (ht0 : 0 < t) (ht2 : t < 2) : Real.exp (-(2 / 3)) ≤ (gaussCarlemanTimeWeight t / t) ^ 2 ∧ (gaussCarlemanTimeWeight t / t) ^ 2 ≤ Real.exp (2 / 3)

The reciprocal comparison for the Gaussian time weight on (0,2).