Related estimates used together by the same construction modules.

Cancellation in the heat-kernel commutator

The multiplier is the square of a cutoff valued in [0, 1]. Its difference is bounded by its Lipschitz variation near the diagonal and by 1 everywhere. The resulting minimum is the cancellation factor used before interchanging the heat-time and spatial integrals.

def NavierStokesR3.Comparison.cutoffSquareDifference (φ : ProblemStatement.Space → ℝ) (x y : ProblemStatement.Space) : ℝ

The cancellation factor for the multiplier φ².

Equations

• NavierStokesR3.Comparison.cutoffSquareDifference φ x y = φ y ^ 2 - φ x ^ 2

theorem NavierStokesR3.Comparison.abs_sq_sub_sq_le_two_mul_abs_sub {a b : ℝ} (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) : |a ^ 2 - b ^ 2| ≤ 2 * |a - b|

theorem NavierStokesR3.Comparison.abs_sq_sub_sq_le_one {a b : ℝ} (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) : |a ^ 2 - b ^ 2| ≤ 1

theorem NavierStokesR3.Comparison.cutoffSquareDifference_abs_le_one {φ : ProblemStatement.Space → ℝ} (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (x y : ProblemStatement.Space) : |cutoffSquareDifference φ x y| ≤ 1

theorem NavierStokesR3.Comparison.cutoffSquareDifference_abs_le_lipschitz {φ : ProblemStatement.Space → ℝ} {L : NNReal} (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (hLip : LipschitzWith L φ) (x y : ProblemStatement.Space) : |cutoffSquareDifference φ x y| ≤ 2 * ↑L * ‖x - y‖

theorem NavierStokesR3.Comparison.cutoffSquareDifference_abs_le_min {φ : ProblemStatement.Space → ℝ} {L : NNReal} (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (hLip : LipschitzWith L φ) (x y : ProblemStatement.Space) : |cutoffSquareDifference φ x y| ≤ min (2 * ↑L * ‖x - y‖) 1

theorem NavierStokesR3.Comparison.cutoffSquareDifference_abs_le_scaled_min {φ : 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) : |cutoffSquareDifference φ x y| ≤ max (2 * L) 1 * min (‖x - y‖ / R) 1

A form with a real scale parameter, convenient for scaled bump functions.

@[simp]

theorem NavierStokesR3.Comparison.cutoffSquareDifference_self (φ : ProblemStatement.Space → ℝ) (x : ProblemStatement.Space) : cutoffSquareDifference φ x x = 0

theorem NavierStokesR3.Comparison.cutoffSquareDifference_swap (φ : ProblemStatement.Space → ℝ) (x y : ProblemStatement.Space) : cutoffSquareDifference φ y x = -cutoffSquareDifference φ x y

noncomputable def NavierStokesR3.Comparison.cancelledTimeKernel (K : ℝ → ProblemStatement.Space → ℝ) (φ : ProblemStatement.Space → ℝ) (x y : ProblemStatement.Space) : ℝ

The time-integrated kernel with cancellation already inserted.

Equations

• NavierStokesR3.Comparison.cancelledTimeKernel K φ x y = ∫ (s : ℝ) in Set.Ioi 0, K s (x - y) * NavierStokesR3.Comparison.cutoffSquareDifference φ x y

noncomputable def NavierStokesR3.Comparison.absoluteCancelledTimeKernel (K : ℝ → ProblemStatement.Space → ℝ) (φ : ProblemStatement.Space → ℝ) (x y : ProblemStatement.Space) : ℝ

The absolute time integral is used to justify the subsequent Fubini step.

Equations

• NavierStokesR3.Comparison.absoluteCancelledTimeKernel K φ x y = ∫ (s : ℝ) in Set.Ioi 0, |K s (x - y) * NavierStokesR3.Comparison.cutoffSquareDifference φ x y|

theorem NavierStokesR3.Comparison.cancelledTimeKernel_abs_le (K : ℝ → ProblemStatement.Space → ℝ) (φ : ProblemStatement.Space → ℝ) (x y : ProblemStatement.Space) : |cancelledTimeKernel K φ x y| ≤ absoluteCancelledTimeKernel K φ x y

theorem NavierStokesR3.Comparison.absoluteCancelledTimeKernel_nonneg (K : ℝ → ProblemStatement.Space → ℝ) (φ : ProblemStatement.Space → ℝ) (x y : ProblemStatement.Space) : 0 ≤ absoluteCancelledTimeKernel K φ x y

theorem NavierStokesR3.Comparison.cancelledTimeKernel_integrable_time {K : ℝ → ProblemStatement.Space → ℝ} (hK : ∀ (z : ProblemStatement.Space), z ≠ 0 → MeasureTheory.IntegrableOn (fun (s : ℝ) => K s z) (Set.Ioi 0) MeasureTheory.volume) (φ : ProblemStatement.Space → ℝ) (x y : ProblemStatement.Space) : MeasureTheory.IntegrableOn (fun (s : ℝ) => K s (x - y) * cutoffSquareDifference φ x y) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokesR3.Comparison.absoluteCancelledTimeKernel_le {K : ℝ → ProblemStatement.Space → ℝ} {φ : ProblemStatement.Space → ℝ} {C L R : ℝ} (hC : 0 ≤ C) (hR : 0 < R) (hK : ∀ (z : ProblemStatement.Space), z ≠ 0 → ∫ (s : ℝ) in Set.Ioi 0, |K s z| ≤ C * ‖z‖ ^ (-3)) (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (hLip : ∀ (x y : ProblemStatement.Space), |φ x - φ y| ≤ L / R * ‖x - y‖) (x y : ProblemStatement.Space) : absoluteCancelledTimeKernel K φ x y ≤ C * max (2 * L) 1 * (‖x - y‖ ^ (-3) * min (‖x - y‖ / R) 1)

theorem NavierStokesR3.Comparison.cancelledTimeKernel_le {K : ℝ → ProblemStatement.Space → ℝ} {φ : ProblemStatement.Space → ℝ} {C L R : ℝ} (hC : 0 ≤ C) (hR : 0 < R) (hK : ∀ (z : ProblemStatement.Space), z ≠ 0 → ∫ (s : ℝ) in Set.Ioi 0, |K s z| ≤ C * ‖z‖ ^ (-3)) (hφ : ∀ (x : ProblemStatement.Space), φ x ∈ Set.Icc 0 1) (hLip : ∀ (x y : ProblemStatement.Space), |φ x - φ y| ≤ L / R * ‖x - y‖) (x y : ProblemStatement.Space) : |cancelledTimeKernel K φ x y| ≤ C * max (2 * L) 1 * (‖x - y‖ ^ (-3) * min (‖x - y‖ / R) 1)

theorem NavierStokesR3.Comparison.cancelledTimeIntegrand_measurable {K : ℝ → ProblemStatement.Space → ℝ} {φ : ProblemStatement.Space → ℝ} (hK : Measurable (Function.uncurry K)) (hφ : Measurable φ) : Measurable fun (p : (ProblemStatement.Space × ProblemStatement.Space) × ℝ) => K p.2 (p.1.1 - p.1.2) * cutoffSquareDifference φ p.1.1 p.1.2

theorem NavierStokesR3.Comparison.cancelledTimeKernel_measurable {K : ℝ → ProblemStatement.Space → ℝ} {φ : ProblemStatement.Space → ℝ} (hK : Measurable (Function.uncurry K)) (hφ : Measurable φ) : Measurable (Function.uncurry (cancelledTimeKernel K φ))

theorem NavierStokesR3.Comparison.absoluteCancelledTimeKernel_measurable {K : ℝ → ProblemStatement.Space → ℝ} {φ : ProblemStatement.Space → ℝ} (hK : Measurable (Function.uncurry K)) (hφ : Measurable φ) : Measurable (Function.uncurry (absoluteCancelledTimeKernel K φ))

theorem NavierStokesR3.Comparison.cutoffSquareDifference_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (k : ℝ) (φ : ProblemStatement.Space → ℝ) (r : E) (x y : ProblemStatement.Space) : k • φ y ^ 2 • r - φ x ^ 2 • k • r = (k * cutoffSquareDifference φ x y) • r

The algebraic cancellation is inserted before either variable is integrated.

The three dimensional heat kernel

The definitions in this file are the ordinary Gaussian heat kernel and its coordinate Hessian. The latter is proved to agree with the spatial derivatives used in the comparison argument.

noncomputable def NavierStokesR3.Comparison.heatKernel (s : ℝ) (z : ProblemStatement.Space) : ℝ

The Euclidean heat kernel in three spatial dimensions.

Equations

• NavierStokesR3.Comparison.heatKernel s z = (4 * Real.pi * s) ^ (-(3 / 2)) * Real.exp (-‖z‖ ^ 2 / (4 * s))

noncomputable def NavierStokesR3.Comparison.heatKernelSecond (s : ℝ) (i j : Fin 3) (z : ProblemStatement.Space) : ℝ

The explicit coordinate Hessian of the Euclidean heat kernel.

Equations

• NavierStokesR3.Comparison.heatKernelSecond s i j z = (z.ofLp i * z.ofLp j / (4 * s ^ 2) - (if i = j then 1 else 0) / (2 * s)) * NavierStokesR3.Comparison.heatKernel s z

theorem NavierStokesR3.Comparison.heatKernel_pos {s : ℝ} (hs : 0 < s) (z : ProblemStatement.Space) : 0 < heatKernel s z

theorem NavierStokesR3.Comparison.heatKernel_nonneg {s : ℝ} (hs : 0 ≤ s) (z : ProblemStatement.Space) : 0 ≤ heatKernel s z

theorem NavierStokesR3.Comparison.hasFDerivAt_heatKernel {s : ℝ} (hs : 0 < s) (z : ProblemStatement.Space) : HasFDerivAt (heatKernel s) (-(heatKernel s z / (2 * s)) • (innerSL ℝ) z) z

theorem NavierStokesR3.Comparison.partial_heatKernel {s : ℝ} (hs : 0 < s) (i : Fin 3) (z : ProblemStatement.Space) : partialD i (heatKernel s) z = -(z.ofLp i / (2 * s)) * heatKernel s z

theorem NavierStokesR3.Comparison.differentiable_heatKernel {s : ℝ} (hs : 0 < s) : Differentiable ℝ (heatKernel s)

theorem NavierStokesR3.Comparison.contDiff_heatKernel (s : ℝ) : ContDiff ℝ (↑⊤) (heatKernel s)

theorem NavierStokesR3.Comparison.heatKernelSecond_eq_partial {s : ℝ} (hs : 0 < s) (i j : Fin 3) (z : ProblemStatement.Space) : heatKernelSecond s i j z = partialD i (partialD j (heatKernel s)) z

The explicit Gaussian Hessian is the actual iterated coordinate derivative.

theorem NavierStokesR3.Comparison.norm_heatKernelSecond_le {s : ℝ} (hs : 0 < s) (i j : Fin 3) (z : ProblemStatement.Space) : ‖heatKernelSecond s i j z‖ ≤ (‖z‖ ^ 2 / (4 * s ^ 2) + 1 / (2 * s)) * heatKernel s z

A radial envelope for every component of the Gaussian Hessian.