Derivative bounds for the normalized flat primitive kernel

The expression algebra below is closed under actual differentiation in x. It bounds all derivatives of the concrete square-root kernel from finitely many derivatives of its smooth profile and proves continuity in the integral parameter. Exponential-majorant integrability is supplied separately.

noncomputable def NavierStokes.FlatKernelBounds.denominator (x t : ℝ) : ℝ

Denominator, given by Real.sqrt (1 + x ^ 2 * t).

Equations

• NavierStokes.FlatKernelBounds.denominator x t = √(1 + x ^ 2 * t)

noncomputable def NavierStokes.FlatKernelBounds.coordinate (x t : ℝ) : ℝ

Coordinate, given by x / denominator x t.

Equations

• NavierStokes.FlatKernelBounds.coordinate x t = x / NavierStokes.FlatKernelBounds.denominator x t

theorem NavierStokes.FlatKernelBounds.base_pos {x t : ℝ} (ht : 0 ≤ t) : 0 < 1 + x ^ 2 * t

theorem NavierStokes.FlatKernelBounds.denominator_pos {x t : ℝ} (ht : 0 ≤ t) : 0 < denominator x t

theorem NavierStokes.FlatKernelBounds.denominator_ne_zero {x t : ℝ} (ht : 0 ≤ t) : denominator x t ≠ 0

theorem NavierStokes.FlatKernelBounds.denominator_sq {x t : ℝ} (ht : 0 ≤ t) : denominator x t ^ 2 = 1 + x ^ 2 * t

theorem NavierStokes.FlatKernelBounds.one_le_denominator {x t : ℝ} (ht : 0 ≤ t) : 1 ≤ denominator x t

theorem NavierStokes.FlatKernelBounds.hasDerivAt_denominator {x t : ℝ} (ht : 0 ≤ t) : HasDerivAt (fun (y : ℝ) => denominator y t) (x * t * (denominator x t)⁻¹) x

theorem NavierStokes.FlatKernelBounds.hasDerivAt_inv_denominator {x t : ℝ} (ht : 0 ≤ t) : HasDerivAt (fun (y : ℝ) => (denominator y t)⁻¹) (-(x * t) * (denominator x t)⁻¹ ^ 3) x

theorem NavierStokes.FlatKernelBounds.hasDerivAt_coordinate {x t : ℝ} (ht : 0 ≤ t) : HasDerivAt (fun (y : ℝ) => coordinate y t) ((denominator x t)⁻¹ ^ 3) x

inductive NavierStokes.FlatKernelBounds.Expr : Type

Finite expressions in the variables needed by every kernel derivative.

• const (c : ℝ) : Expr
• x : Expr
• t : Expr
• root : Expr
• invRoot : Expr
• jet (k : ℕ) : Expr
• add (e f : Expr) : Expr
• mul (e f : Expr) : Expr

def NavierStokes.FlatKernelBounds.Expr.eval : Expr → (ℝ → ℝ) → ℝ → ℝ → ℝ

Eval used in flat kernel bounds.

Equations

• (NavierStokes.FlatKernelBounds.Expr.const c).eval x✝² x✝¹ x✝ = c
• NavierStokes.FlatKernelBounds.Expr.x.eval x✝² x✝¹ x✝ = x✝¹
• NavierStokes.FlatKernelBounds.Expr.t.eval x✝² x✝¹ x✝ = x✝
• NavierStokes.FlatKernelBounds.Expr.root.eval x✝² x✝¹ x✝ = NavierStokes.FlatKernelBounds.denominator x✝¹ x✝
• NavierStokes.FlatKernelBounds.Expr.invRoot.eval x✝² x✝¹ x✝ = (NavierStokes.FlatKernelBounds.denominator x✝¹ x✝)⁻¹
• (NavierStokes.FlatKernelBounds.Expr.jet k).eval x✝² x✝¹ x✝ = iteratedDeriv k x✝² (NavierStokes.FlatKernelBounds.coordinate x✝¹ x✝)
• (e.add f).eval x✝² x✝¹ x✝ = e.eval x✝² x✝¹ x✝ + f.eval x✝² x✝¹ x✝
• (e.mul f).eval x✝² x✝¹ x✝ = e.eval x✝² x✝¹ x✝ * f.eval x✝² x✝¹ x✝

def NavierStokes.FlatKernelBounds.Expr.pow (e : Expr) : ℕ → Expr

Pow as an element of ℕ → Expr | 0 => .const 1 | n + 1 => .mul (e.pow n) e.

Equations

• e.pow 0 = NavierStokes.FlatKernelBounds.Expr.const 1
• e.pow n.succ = (e.pow n).mul e

@[simp]

theorem NavierStokes.FlatKernelBounds.Expr.eval_pow (e : Expr) (n : ℕ) (b : ℝ → ℝ) (x t : ℝ) : (e.pow n).eval b x t = e.eval b x t ^ n

def NavierStokes.FlatKernelBounds.Expr.diff : Expr → Expr

Diff used in flat kernel bounds.

Equations

• One or more equations did not get rendered due to their size.
• (NavierStokes.FlatKernelBounds.Expr.const c).diff = NavierStokes.FlatKernelBounds.Expr.const 0
• NavierStokes.FlatKernelBounds.Expr.x.diff = NavierStokes.FlatKernelBounds.Expr.const 1
• NavierStokes.FlatKernelBounds.Expr.t.diff = NavierStokes.FlatKernelBounds.Expr.const 0
• NavierStokes.FlatKernelBounds.Expr.root.diff = (NavierStokes.FlatKernelBounds.Expr.x.mul NavierStokes.FlatKernelBounds.Expr.t).mul NavierStokes.FlatKernelBounds.Expr.invRoot
• (NavierStokes.FlatKernelBounds.Expr.jet k).diff = (NavierStokes.FlatKernelBounds.Expr.jet (k + 1)).mul (NavierStokes.FlatKernelBounds.Expr.invRoot.pow 3)
• (e.add f).diff = e.diff.add f.diff
• (e.mul f).diff = (e.diff.mul f).add (e.mul f.diff)

theorem NavierStokes.FlatKernelBounds.Expr.hasDerivAt_eval (e : Expr) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) {x t : ℝ} (ht : 0 ≤ t) : HasDerivAt (fun (y : ℝ) => e.eval b y t) (e.diff.eval b x t) x

theorem NavierStokes.FlatKernelBounds.Expr.iteratedDeriv_eval (e : Expr) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) {t : ℝ} (ht : 0 ≤ t) (n : ℕ) : (iteratedDeriv n fun (x : ℝ) => e.eval b x t) = fun (x : ℝ) => (diff^[n] e).eval b x t

theorem NavierStokes.FlatKernelBounds.Expr.contDiff_eval (e : Expr) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (x : ℝ) => e.eval b x t

theorem NavierStokes.FlatKernelBounds.abs_coordinate_le {x t : ℝ} (ht : 0 ≤ t) : |coordinate x t| ≤ |x|

theorem NavierStokes.FlatKernelBounds.denominator_le_polynomial {R x t : ℝ} (hR : 0 ≤ R) (hx : |x| ≤ R) (ht : 0 ≤ t) : denominator x t ≤ (1 + R ^ 2) * (1 + t)

theorem NavierStokes.FlatKernelBounds.abs_inv_denominator_le_one {x t : ℝ} (ht : 0 ≤ t) : |(denominator x t)⁻¹| ≤ 1

def NavierStokes.FlatKernelBounds.PolynomialBound (R : ℝ) (F : ℝ → ℝ → ℝ) : Prop

A bound uniform in a closed x interval and polynomial in nonnegative t.

Equations

• NavierStokes.FlatKernelBounds.PolynomialBound R F = ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (x t : ℝ), |x| ≤ R → 0 ≤ t → |F x t| ≤ C * (1 + t) ^ N

theorem NavierStokes.FlatKernelBounds.PolynomialBound.add {R : ℝ} {F G : ℝ → ℝ → ℝ} (hF : PolynomialBound R F) (hG : PolynomialBound R G) : PolynomialBound R fun (x t : ℝ) => F x t + G x t

theorem NavierStokes.FlatKernelBounds.PolynomialBound.mul {R : ℝ} {F G : ℝ → ℝ → ℝ} (hF : PolynomialBound R F) (hG : PolynomialBound R G) : PolynomialBound R fun (x t : ℝ) => F x t * G x t

def NavierStokes.FlatKernelBounds.Expr.jetOrder : Expr → ℕ

The greatest profile derivative order present in a finite expression.

Equations

• (NavierStokes.FlatKernelBounds.Expr.jet k).jetOrder = k
• (e.add f).jetOrder = max e.jetOrder f.jetOrder
• (e.mul f).jetOrder = max e.jetOrder f.jetOrder
• x✝.jetOrder = 0

theorem NavierStokes.FlatKernelBounds.Expr.polynomialBound_of_jetBound (e : Expr) {b : ℝ → ℝ} {R : ℝ} (hR : 0 ≤ R) (hjets : ∀ k ≤ e.jetOrder, ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y : ℝ), |y| ≤ R → |iteratedDeriv k b y| ≤ C) : PolynomialBound R (e.eval b)

Only finitely many profile jets are needed for a given expression bound.

theorem NavierStokes.FlatKernelBounds.bounded_profile_jet {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (R : ℝ) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y : ℝ), |y| ≤ R → |iteratedDeriv k b y| ≤ C

theorem NavierStokes.FlatKernelBounds.Expr.polynomialBound (e : Expr) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) {R : ℝ} (hR : 0 ≤ R) : PolynomialBound R (e.eval b)

theorem NavierStokes.FlatKernelBounds.continuous_denominator_t (x : ℝ) : Continuous (denominator x)

theorem NavierStokes.FlatKernelBounds.continuousOn_coordinate_t (x : ℝ) : ContinuousOn (coordinate x) (Set.Ici 0)

theorem NavierStokes.FlatKernelBounds.Expr.continuousOn_eval_t (e : Expr) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (x : ℝ) : ContinuousOn (fun (t : ℝ) => e.eval b x t) (Set.Ici 0)

theorem NavierStokes.FlatKernelBounds.Expr.jetOrder_pow_le (e : Expr) (n : ℕ) : (e.pow n).jetOrder ≤ e.jetOrder

theorem NavierStokes.FlatKernelBounds.Expr.jetOrder_diff_le (e : Expr) : e.diff.jetOrder ≤ e.jetOrder + 1

theorem NavierStokes.FlatKernelBounds.Expr.jetOrder_iterate_diff_le (e : Expr) (n : ℕ) : (diff^[n] e).jetOrder ≤ e.jetOrder + n

def NavierStokes.FlatKernelBounds.kernelExpr (j : ℕ) : Expr

Kernel expr, given by .mul (.mul (Expr.root.pow j) (Expr.invRoot.pow 3)) (.jet 0).

Equations

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

theorem NavierStokes.FlatKernelBounds.kernelExpr_jetOrder (j : ℕ) : (kernelExpr j).jetOrder = 0

noncomputable def NavierStokes.FlatKernelBounds.kernel (c : ℝ) (j : ℕ) (b : ℝ → ℝ) (x t : ℝ) : ℝ

Kernel, given by (1 / 2 : ℝ) * Real.exp (-c * t) * (denominator x t ^ j / denominator x t ^ 3) * b (coordinate x t).

Equations

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

theorem NavierStokes.FlatKernelBounds.kernel_eq_expr (c : ℝ) (j : ℕ) (b : ℝ → ℝ) (x t : ℝ) : kernel c j b x t = 1 / 2 * Real.exp (-c * t) * (kernelExpr j).eval b x t

theorem NavierStokes.FlatKernelBounds.Expr.iteratedDeriv_const_mul_eval (e : Expr) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) {t : ℝ} (ht : 0 ≤ t) (w : ℝ) (n : ℕ) : (iteratedDeriv n fun (x : ℝ) => w * e.eval b x t) = fun (x : ℝ) => w * (diff^[n] e).eval b x t

theorem NavierStokes.FlatKernelBounds.iteratedDeriv_kernel {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (c : ℝ) (j n : ℕ) {t : ℝ} (ht : 0 ≤ t) : (iteratedDeriv n fun (x : ℝ) => kernel c j b x t) = fun (x : ℝ) => 1 / 2 * Real.exp (-c * t) * (Expr.diff^[n] (kernelExpr j)).eval b x t

theorem NavierStokes.FlatKernelBounds.kernel_contDiff_x {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (c : ℝ) (j : ℕ) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (x : ℝ) => kernel c j b x t

theorem NavierStokes.FlatKernelBounds.kernel_iteratedDeriv_contDiff_x {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (c : ℝ) (j n : ℕ) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (iteratedDeriv n fun (x : ℝ) => kernel c j b x t)

theorem NavierStokes.FlatKernelBounds.unweighted_iteratedDeriv_bound {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (j n : ℕ) {R : ℝ} (hR : 0 ≤ R) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (x t : ℝ), |x| ≤ R → 0 ≤ t → |iteratedDeriv n (fun (y : ℝ) => denominator y t ^ j / denominator y t ^ 3 * b (coordinate y t)) x| ≤ C * (1 + t) ^ N

theorem NavierStokes.FlatKernelBounds.kernel_iteratedDeriv_bound_of_jetBounds {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (c : ℝ) (j n : ℕ) {R : ℝ} (hR : 0 ≤ R) (hjets : ∀ k ≤ n, ∃ (C : ℝ), 0 ≤ C ∧ ∀ (y : ℝ), |y| ≤ R → |iteratedDeriv k b y| ≤ C) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (x t : ℝ), |x| ≤ R → 0 ≤ t → |iteratedDeriv n (fun (y : ℝ) => kernel c j b y t) x| ≤ C * (1 + t) ^ N * Real.exp (-c * t)

An order-n bound uses only the first n profile jets on [-R,R]. The global smoothness assumption identifies the expression with the actual derivative.

theorem NavierStokes.FlatKernelBounds.kernel_iteratedDeriv_bound {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (c : ℝ) (j n : ℕ) {R : ℝ} (hR : 0 ≤ R) : ∃ (C : ℝ) (N : ℕ), 0 ≤ C ∧ ∀ (x t : ℝ), |x| ≤ R → 0 ≤ t → |iteratedDeriv n (fun (y : ℝ) => kernel c j b y t) x| ≤ C * (1 + t) ^ N * Real.exp (-c * t)

theorem NavierStokes.FlatKernelBounds.kernel_iteratedDeriv_continuousOn_t {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (c : ℝ) (j n : ℕ) (x : ℝ) : ContinuousOn (fun (t : ℝ) => iteratedDeriv n (fun (y : ℝ) => kernel c j b y t) x) (Set.Ici 0)