The paired estimate for the heat commutator kernel

The time-integrated heat Hessian, after cutoff cancellation, is dominated by the radial L^(4/3) kernel. Its exact scaling and the sectionwise Hölder bound give the factor R^(-3/4) in the paired commutator estimate.

Integration in time for the heat-kernel Hessian

The reciprocal substitution reduces the inverse-time Gaussian integrals to the ordinary Gamma integral. These estimates are uniform in the spatial indices and give the inverse-cube kernel bound in three dimensions.

theorem NavierStokesR3.Comparison.integrableOn_inverseTimeGamma {a p : ℝ} (ha : 0 < a) (hp : 0 < p) : MeasureTheory.IntegrableOn (fun (s : ℝ) => s ^ (-(p + 1)) * Real.exp (-a / s)) (Set.Ioi 0) MeasureTheory.volume

The inverse-time Gaussian power is integrable for every positive shape parameter and positive spatial scale.

theorem NavierStokesR3.Comparison.integral_inverseTimeGamma {a p : ℝ} (ha : 0 < a) (hp : 0 < p) : ∫ (s : ℝ) in Set.Ioi 0, s ^ (-(p + 1)) * Real.exp (-a / s) = a ^ (-p) * Real.Gamma p

Reciprocal substitution evaluates the inverse-time Gamma integral.

theorem NavierStokesR3.Comparison.integral_inverseTimeGamma_square_scale {r p : ℝ} (hr : 0 < r) (hp : 0 < p) : ∫ (s : ℝ) in Set.Ioi 0, s ^ (-(p + 1)) * Real.exp (-(r ^ 2 / 4) / s) = 4 ^ p * r ^ (-2 * p) * Real.Gamma p

The scale occurring in the heat kernel gives the expected homogeneous power after integration in time.

noncomputable def NavierStokesR3.Comparison.heatKernelSecondTimeEnvelope (r s : ℝ) : ℝ

A common, nonnegative majorant of the nine coordinate Hessians.

Equations

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

noncomputable def NavierStokesR3.Comparison.heatKernelTimeConstant : ℝ

One universal constant for the time-integrated three dimensional heat kernel Hessian. Its exact value is immaterial to the commutator estimate.

Equations

• NavierStokesR3.Comparison.heatKernelTimeConstant = (4 * Real.pi) ^ (-(3 / 2)) * (4 ^ (5 / 2) / 4 * Real.Gamma (5 / 2) + 4 ^ (3 / 2) / 2 * Real.Gamma (3 / 2))

theorem NavierStokesR3.Comparison.heatKernelTimeConstant_pos : 0 < heatKernelTimeConstant

theorem NavierStokesR3.Comparison.heatKernelSecondTimeEnvelope_nonneg {s : ℝ} (r : ℝ) (hs : 0 ≤ s) : 0 ≤ heatKernelSecondTimeEnvelope r s

theorem NavierStokesR3.Comparison.heatKernelSecondTimeEnvelope_integrable {r : ℝ} (hr : 0 < r) : MeasureTheory.IntegrableOn (heatKernelSecondTimeEnvelope r) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokesR3.Comparison.integral_heatKernelSecondTimeEnvelope {r : ℝ} (hr : 0 < r) : ∫ (s : ℝ) in Set.Ioi 0, heatKernelSecondTimeEnvelope r s = heatKernelTimeConstant * r ^ (-3)

theorem NavierStokesR3.Comparison.heatKernelSecond_inverseTime_decomposition {s : ℝ} (hs : 0 < s) (i j : Fin 3) (z : ProblemStatement.Space) : heatKernelSecond s i j z = (4 * Real.pi) ^ (-(3 / 2)) * (z.ofLp i * z.ofLp j / 4 * (s ^ (-(5 / 2 + 1)) * Real.exp (-(‖z‖ ^ 2 / 4) / s)) - (if i = j then 1 else 0) / 2 * (s ^ (-(3 / 2 + 1)) * Real.exp (-(‖z‖ ^ 2 / 4) / s)))

The Gaussian coordinate Hessian is the difference of two integrable inverse-time Gamma terms.

theorem NavierStokesR3.Comparison.heatKernelSecondTimeEnvelope_eq {s : ℝ} (hs : 0 < s) (z : ProblemStatement.Space) : heatKernelSecondTimeEnvelope ‖z‖ s = (‖z‖ ^ 2 / (4 * s ^ 2) + 1 / (2 * s)) * heatKernel s z

theorem NavierStokesR3.Comparison.norm_heatKernelSecond_le_timeEnvelope {s : ℝ} (hs : 0 < s) (i j : Fin 3) (z : ProblemStatement.Space) : ‖heatKernelSecond s i j z‖ ≤ heatKernelSecondTimeEnvelope ‖z‖ s

theorem NavierStokesR3.Comparison.heatKernelSecond_integrable_time (i j : Fin 3) {z : ProblemStatement.Space} (hz : z ≠ 0) : MeasureTheory.IntegrableOn (fun (s : ℝ) => heatKernelSecond s i j z) (Set.Ioi 0) MeasureTheory.volume

Away from the spatial origin, every Hessian component is integrable in positive time.

theorem NavierStokesR3.Comparison.heatKernelSecond_integral_norm_le (i j : Fin 3) {z : ProblemStatement.Space} (hz : z ≠ 0) : ∫ (s : ℝ) in Set.Ioi 0, ‖heatKernelSecond s i j z‖ ≤ heatKernelTimeConstant * ‖z‖ ^ (-3)

The positive-time integral of the absolute Hessian kernel has the inverse-cube decay needed for the pressure commutator.

theorem NavierStokesR3.Comparison.heatKernelSecond_integral_abs_le (i j : Fin 3) {z : ProblemStatement.Space} (hz : z ≠ 0) : ∫ (s : ℝ) in Set.Ioi 0, |heatKernelSecond s i j z| ≤ heatKernelTimeConstant * ‖z‖ ^ (-3)

noncomputable def NavierStokesR3.Comparison.heatCommutatorKernel (i j : Fin 3) (φ : ProblemStatement.Space → ℝ) (x y : ProblemStatement.Space) : ℝ

The actual time-integrated heat Hessian with cutoff cancellation already inserted into the time integrand.

Equations

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

noncomputable def NavierStokesR3.Comparison.rieszCommutatorConstant : ℝ

A universal positive constant for the paired commutator estimate.

Equations

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

theorem NavierStokesR3.Comparison.rieszCommutatorConstant_pos : 0 < rieszCommutatorConstant

theorem NavierStokesR3.Comparison.heatKernelSecond_joint_measurable (i j : Fin 3) : Measurable (Function.uncurry fun (s : ℝ) (z : ProblemStatement.Space) => heatKernelSecond s i j z)

The explicit heat Hessian is jointly measurable in time and space, including the totalized formula at time zero.

theorem NavierStokesR3.Comparison.heatCommutatorKernel_measurable (i j : Fin 3) {φ : ProblemStatement.Space → ℝ} (hφ : Measurable φ) : Measurable (Function.uncurry (heatCommutatorKernel i j φ))

The integrated, cancelled heat kernel is jointly measurable in its two spatial variables.

theorem NavierStokesR3.Comparison.heatCommutatorKernel_bound (i j : Fin 3) {φ : ProblemStatement.Space → ℝ} {L R : ℝ} (hR : 0 < R) (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (hLip : ∀ (x y : ProblemStatement.Space), |φ x - φ y| ≤ L / R * ‖x - y‖) (x y : ProblemStatement.Space) : ‖heatCommutatorKernel i j φ x y‖ ≤ heatKernelTimeConstant * max (2 * L) 1 * radialCommutatorKernel R (x - y)

Pointwise domination by the radial commutator kernel.

theorem NavierStokesR3.Comparison.heatKernel_commutator_section_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i j : Fin 3) {φ : ProblemStatement.Space → ℝ} {r : ProblemStatement.Space → E} {L R : ℝ} (hR : 0 < R) (hφm : Measurable φ) (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (hLip : ∀ (x y : ProblemStatement.Space), |φ x - φ y| ≤ L / R * ‖x - y‖) (hr : MeasureTheory.MemLp r 4 MeasureTheory.volume) (x : ProblemStatement.Space) : MeasureTheory.Integrable (fun (y : ProblemStatement.Space) => heatCommutatorKernel i j φ x y • r y) MeasureTheory.volume

Every heat commutator section acts by an integrable scalar product on L⁴ data.

theorem NavierStokesR3.Comparison.heatKernel_commutator_product_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i j : Fin 3) {φ g : ProblemStatement.Space → ℝ} {r : ProblemStatement.Space → E} {L R : ℝ} (hR : 0 < R) (hφm : Measurable φ) (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (hLip : ∀ (x y : ProblemStatement.Space), |φ x - φ y| ≤ L / R * ‖x - y‖) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hr : MeasureTheory.MemLp r 4 MeasureTheory.volume) : MeasureTheory.Integrable (fun (p : ProblemStatement.Space × ProblemStatement.Space) => g p.1 • heatCommutatorKernel i j φ p.1 p.2 • r p.2) (MeasureTheory.volume.prod MeasureTheory.volume)

The paired heat kernel is integrable on the product of spatial domains.

theorem NavierStokesR3.Comparison.heatKernel_commutator_pair_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i j : Fin 3) {φ g : ProblemStatement.Space → ℝ} {r : ProblemStatement.Space → E} {L R : ℝ} (hR : 0 < R) (hφm : Measurable φ) (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (hLip : ∀ (x y : ProblemStatement.Space), |φ x - φ y| ≤ L / R * ‖x - y‖) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hr : MeasureTheory.MemLp r 4 MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => g x • ∫ (y : ProblemStatement.Space), heatCommutatorKernel i j φ x y • r y) MeasureTheory.volume

The outer pairing is genuinely integrable for real L¹ and vector-valued L⁴ data.

theorem NavierStokesR3.Comparison.heatKernel_paired_commutator_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i j : Fin 3) {φ g : ProblemStatement.Space → ℝ} {r : ProblemStatement.Space → E} {L R : ℝ} (hR : 0 < R) (hφm : Measurable φ) (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (hLip : ∀ (x y : ProblemStatement.Space), |φ x - φ y| ≤ L / R * ‖x - y‖) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hr : MeasureTheory.MemLp r 4 MeasureTheory.volume) : ‖∫ (x : ProblemStatement.Space), g x • ∫ (y : ProblemStatement.Space), heatCommutatorKernel i j φ x y • r y‖ ≤ rieszCommutatorConstant * max (2 * L) 1 * R ^ (-(3 / 4)) * comparisonLpNorm 1 g * comparisonLpNorm 4 r

The actual heat commutator satisfies the required paired estimate, with the precise R^(-3/4) decay and a universal positive constant.