The whole-space logarithmic gradient estimate. Every input norm belongs to the given smooth L² field, and the vorticity is its literal curl. The proof uses the constructed Gaussian kernel and its true heat equation.

The logarithmic middle heat scales for an actual elliptic curl equation.

The small-time heat remainder from genuine third spatial L² derivatives.

theorem EulerWholeSpaceGaussian.derivative_high_remainder {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (A : EulerLpTranslation.SmoothL2Field V) (j : Fin 3) (x : EulerSmoothLimit.Space) {ε : ℝ} (hε : 0 < ε) : ‖(fderiv ℝ A.field x) (EulerOrdinarySobolev.axis j) - average ε (A.directionalField (EulerOrdinarySobolev.axis j)).field x‖ ≤ 3 * ε ^ (1 / 4) * ‖A.jetLp 3‖

The heat remainder of one actual spatial derivative is O(ε^(1/4)) times the third spatial L² tensor. No Hölder or heat estimate is assumed.

noncomputable def EulerWholeSpaceGaussian.middleCost : ℝ

Middle cost, given by 5*(2:ℝ)^((3:ℝ)/2).

Equations

• EulerWholeSpaceGaussian.middleCost = 5 * 2 ^ (3 / 2)

theorem EulerWholeSpaceGaussian.middleCost_nonneg : 0 ≤ middleCost

theorem EulerWholeSpaceGaussian.secondAverage_elliptic (A G H : EulerLpTranslation.SmoothL2Field ℝ) (a b j : Fin 3) (hΔ : ∀ (y : EulerSmoothLimit.Space), Laplacian.laplacian A.field y = EulerVectorCalculus.partialDerivative G.field a y - EulerVectorCalculus.partialDerivative H.field b y) {t : ℝ} (ht : 0 < t) (x : EulerSmoothLimit.Space) : secondAverage t (A.directionalField (EulerOrdinarySobolev.axis j)).field x = average t ((G.directionalField (EulerOrdinarySobolev.axis a)).directionalField (EulerOrdinarySobolev.axis j)).field x - average t ((H.directionalField (EulerOrdinarySobolev.axis b)).directionalField (EulerOrdinarySobolev.axis j)).field x

theorem EulerWholeSpaceGaussian.secondAverage_elliptic_bound (A G H : EulerLpTranslation.SmoothL2Field ℝ) (a b j : Fin 3) (hΔ : ∀ (y : EulerSmoothLimit.Space), Laplacian.laplacian A.field y = EulerVectorCalculus.partialDerivative G.field a y - EulerVectorCalculus.partialDerivative H.field b y) (W : ℝ) (hG : ∀ (y : EulerSmoothLimit.Space), ‖G.field y‖ ≤ W) (hH : ∀ (y : EulerSmoothLimit.Space), ‖H.field y‖ ≤ W) {t : ℝ} (ht : 0 < t) (x : EulerSmoothLimit.Space) : ‖(1 / 4) • secondAverage t (A.directionalField (EulerOrdinarySobolev.axis j)).field x‖ ≤ middleCost * t⁻¹ * W

theorem EulerWholeSpaceGaussian.derivative_elliptic_middle (A G H : EulerLpTranslation.SmoothL2Field ℝ) (a b j : Fin 3) (hΔ : ∀ (y : EulerSmoothLimit.Space), Laplacian.laplacian A.field y = EulerVectorCalculus.partialDerivative G.field a y - EulerVectorCalculus.partialDerivative H.field b y) (W : ℝ) (hG : ∀ (y : EulerSmoothLimit.Space), ‖G.field y‖ ≤ W) (hH : ∀ (y : EulerSmoothLimit.Space), ‖H.field y‖ ≤ W) (x : EulerSmoothLimit.Space) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : ‖average ε (A.directionalField (EulerOrdinarySobolev.axis j)).field x - average 1 (A.directionalField (EulerOrdinarySobolev.axis j)).field x‖ ≤ middleCost * W * -Real.log ε

Integrating the genuine 1/t estimate gives the logarithmic middle term.

theorem EulerWholeSpaceGaussian.elliptic_derivative_split (A G H : EulerLpTranslation.SmoothL2Field ℝ) (a b j : Fin 3) (hΔ : ∀ (y : EulerSmoothLimit.Space), Laplacian.laplacian A.field y = EulerVectorCalculus.partialDerivative G.field a y - EulerVectorCalculus.partialDerivative H.field b y) (W : ℝ) (hG : ∀ (y : EulerSmoothLimit.Space), ‖G.field y‖ ≤ W) (hH : ∀ (y : EulerSmoothLimit.Space), ‖H.field y‖ ≤ W) (x : EulerSmoothLimit.Space) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : ‖EulerVectorCalculus.partialDerivative A.field j x‖ ≤ lowCost * ‖A.toLp‖ + middleCost * W * -Real.log ε + 3 * ε ^ (1 / 4) * ‖A.jetLp 3‖

The three heat scales, with every term attached to the original field.

The actual whole-space logarithmic derivative estimate for a scalar elliptic equation whose right-hand side is the derivative of bounded fields.

Optimization of the actual heat-scale estimate used in the whole-space logarithmic gradient bound.

theorem EulerLogarithmicCutoff.optimize (X c L W H : ℝ) (hc : 0 ≤ c) (hL : 0 ≤ L) (hH : 0 ≤ H) (hbound : ∀ (ε : ℝ), 0 < ε → ε < 1 → X ≤ c * (L + W * -Real.log ε + ε ^ (1 / 4) * H)) : X ≤ 4 * c * (1 + L + W * Real.log (Real.exp 1 + H))

noncomputable def EulerWholeSpaceGaussian.splitCost : ℝ

Split cost, given by lowCost+middleCost+3.

Equations

• EulerWholeSpaceGaussian.splitCost = EulerWholeSpaceGaussian.lowCost + EulerWholeSpaceGaussian.middleCost + 3

theorem EulerWholeSpaceGaussian.splitCost_nonneg : 0 ≤ splitCost

theorem EulerWholeSpaceGaussian.splitCost_pos : 0 < splitCost

theorem EulerWholeSpaceGaussian.elliptic_derivative_logarithmic (A G J : EulerLpTranslation.SmoothL2Field ℝ) (a b j : Fin 3) (hΔ : ∀ (y : EulerSmoothLimit.Space), Laplacian.laplacian A.field y = EulerVectorCalculus.partialDerivative G.field a y - EulerVectorCalculus.partialDerivative J.field b y) (W : ℝ) (hG : ∀ (y : EulerSmoothLimit.Space), ‖G.field y‖ ≤ W) (hJ : ∀ (y : EulerSmoothLimit.Space), ‖J.field y‖ ≤ W) (H : ℝ) (hH : ‖A.jetLp 3‖ ≤ H) (x : EulerSmoothLimit.Space) : ‖EulerVectorCalculus.partialDerivative A.field j x‖ ≤ 4 * splitCost * (1 + ‖A.toLp‖ + W * Real.log (Real.exp 1 + H))

The bound is proved for the genuine derivative of A. H only bounds its actual third L² derivative tensor; the elliptic equation is literal.

noncomputable def EulerOrdinarySobolev.logarithmicGradientConstant : ℝ

Logarithmic gradient constant, given by 36*splitCost.

Equations

• EulerOrdinarySobolev.logarithmicGradientConstant = 36 * EulerWholeSpaceGaussian.splitCost

theorem EulerOrdinarySobolev.logarithmicGradientConstant_pos : 0 < logarithmicGradientConstant

theorem EulerOrdinarySobolev.logarithmicGradientConstant_nonneg : 0 ≤ logarithmicGradientConstant

theorem EulerOrdinarySobolev.logarithmic_gradient_bound (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hdiv : ∀ (y : EulerSmoothLimit.Space), EulerSmoothLimit.divergence A.field y = 0) (W : ℝ) (hW : ∀ (y : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl A.field y‖ ≤ W) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ A.field x‖ ≤ logarithmicGradientConstant * (1 + ‖A.toLp‖ + W * Real.log (Real.exp 1 + tensorNorm 3 A))

A genuine whole-space BKM logarithmic estimate from the actual velocity, its actual H³ tensors, and its actual vorticity.

theorem EulerOrdinarySobolev.logarithmic_gradient_bound_solenoidal (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (W : ℝ) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hW : ∀ (y : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl A.field y‖ ≤ W) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ A.field x‖ ≤ logarithmicGradientConstant * (1 + ‖A.toLp‖ + W * Real.log (Real.exp 1 + tensorNorm 3 A))

This form discharges the entire logarithmic-estimate hypothesis of the ordinary Euler continuation theorem.