The transformed integral for a terminal flat primitive

The change of variables is u = x / sqrt (1 + x² t) for x > 0. Natural powers of the square root encode the real power (j - 3) / 2 without truncating subtraction in the natural numbers.

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

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

Equations

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

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

Coordinate, given by x / denominator x t.

Equations

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

noncomputable def NavierStokes.FlatPrimitiveFactor.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.

noncomputable def NavierStokes.FlatPrimitiveFactor.factor (c : ℝ) (j : ℕ) (b : ℝ → ℝ) (x : ℝ) : ℝ

Factor, given by ∫ t in Ioi (0 : ℝ), kernel c j b x t.

Equations

• NavierStokes.FlatPrimitiveFactor.factor c j b x = ∫ (t : ℝ) in Set.Ioi 0, NavierStokes.FlatPrimitiveFactor.kernel c j b x t

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

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

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

theorem NavierStokes.FlatPrimitiveFactor.denominator_ratio_eq_rpow (j : ℕ) (x : ℝ) {t : ℝ} (ht : 0 ≤ t) : denominator x t ^ j / denominator x t ^ 3 = (1 + x ^ 2 * t) ^ ((↑j - 3) / 2)

The square-root notation is exactly the real power appearing in the substitution formula, including when j < 3.

theorem NavierStokes.FlatPrimitiveFactor.coordinate_pos {x t : ℝ} (hx : 0 < x) (ht : 0 ≤ t) : 0 < coordinate x t

theorem NavierStokes.FlatPrimitiveFactor.coordinate_hasDerivAt (x : ℝ) {t : ℝ} (ht : 0 ≤ t) : HasDerivAt (coordinate x) (-(x ^ 3 / (2 * denominator x t ^ 3))) t

theorem NavierStokes.FlatPrimitiveFactor.coordinate_mem_Ioo {x t : ℝ} (hx : 0 < x) (ht : 0 < t) : coordinate x t ∈ Set.Ioo 0 x

theorem NavierStokes.FlatPrimitiveFactor.coordinate_injOn {x : ℝ} (hx : 0 < x) : Set.InjOn (coordinate x) (Set.Ioi 0)

theorem NavierStokes.FlatPrimitiveFactor.coordinate_image {x : ℝ} (hx : 0 < x) : coordinate x '' Set.Ioi 0 = Set.Ioo 0 x

theorem NavierStokes.FlatPrimitiveFactor.edge_coordinate (c : ℝ) {x t : ℝ} (hx : 0 < x) (ht : 0 ≤ t) : FlatCutoff.edge c (coordinate x t) = FlatCutoff.edge c x * Real.exp (-c * t)

theorem NavierStokes.FlatPrimitiveFactor.transformed_integrand (c : ℝ) (j : ℕ) (b : ℝ → ℝ) {x t : ℝ} (hx : 0 < x) (ht : 0 ≤ t) : |(-(x ^ 3 / (2 * denominator x t ^ 3)))| * FlatPrimitive.integrand c j b (coordinate x t) = FlatPrimitive.scale c j x * kernel c j b x t

theorem NavierStokes.FlatPrimitiveFactor.primitive_eq_scale_mul_factor (c : ℝ) (j : ℕ) (b : ℝ → ℝ) {x : ℝ} (hx : 0 < x) : FlatPrimitive.primitive c j b x = FlatPrimitive.scale c j x * factor c j b x

Exact change of variables for the actual primitive. The Jacobian theorem supplies the equality even before separate integrability estimates are used.

theorem NavierStokes.FlatPrimitiveFactor.factor_eq_normalized_primitive (c : ℝ) (j : ℕ) (b : ℝ → ℝ) {x : ℝ} (hx : 0 < x) : factor c j b x = FlatPrimitive.primitive c j b x / FlatPrimitive.scale c j x

The transformed integral is the normalized primitive for positive x.

theorem NavierStokes.FlatPrimitiveFactor.kernel_at_zero (c : ℝ) (j : ℕ) (b : ℝ → ℝ) (t : ℝ) : kernel c j b 0 t = b 0 / 2 * Real.exp (-c * t)

theorem NavierStokes.FlatPrimitiveFactor.factor_at_zero {c : ℝ} (hc : 0 < c) (j : ℕ) (b : ℝ → ℝ) : factor c j b 0 = b 0 / (2 * c)

The transformed integral has the predicted endpoint value directly, without passing to the normalized primitive's limit.

theorem NavierStokes.FlatPrimitiveFactor.polynomial_exp_integrable {c : ℝ} (hc : 0 < c) (N : ℕ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (1 + t) ^ N * Real.exp (-c * t)) (Set.Ioi 0) MeasureTheory.volume

Every fixed polynomial majorant is integrable against the decaying exponential on the transformed half-line.

theorem NavierStokes.FlatPrimitiveFactor.const_polynomial_exp_integrable {c : ℝ} (hc : 0 < c) (C : ℝ) (N : ℕ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => C * (1 + t) ^ N * Real.exp (-c * t)) (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.FlatPrimitiveFactor.kernel_ae_contDiff (c : ℝ) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ContDiff ℝ ↑⊤ fun (x : ℝ) => kernel c j b x t

theorem NavierStokes.FlatPrimitiveFactor.kernel_iteratedDeriv_measurable (c : ℝ) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (n : ℕ) (x : ℝ) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => iteratedDeriv n (fun (y : ℝ) => kernel c j b y t) x) (MeasureTheory.volume.restrict (Set.Ioi 0))

theorem NavierStokes.FlatPrimitiveFactor.kernel_locallyDominated {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : SmoothParameterIntegral.LocallyDominatedDeriv (kernel c j b) (MeasureTheory.volume.restrict (Set.Ioi 0))

All hypotheses for dominated differentiation come from actual kernel derivatives and polynomial-exponential bounds on bounded parameter sets.

theorem NavierStokes.FlatPrimitiveFactor.factor_contDiff {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : ContDiff ℝ (↑⊤) (factor c j b)

The concrete transformed integral is smooth on all of ℝ, including across the endpoint of the original primitive.

theorem NavierStokes.FlatPrimitiveFactor.factor_iteratedDeriv {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (n : ℕ) (x : ℝ) : iteratedDeriv n (factor c j b) x = ∫ (t : ℝ) in Set.Ioi 0, iteratedDeriv n (fun (y : ℝ) => kernel c j b y t) x

theorem NavierStokes.FlatPrimitiveFactor.exists_smooth_factor {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : ∃ (F : ℝ → ℝ), ContDiff ℝ (↑⊤) F ∧ F 0 = b 0 / (2 * c) ∧ ∀ (x : ℝ), 0 ≤ x → FlatPrimitive.primitive c j b x = FlatPrimitive.scale c j x * F x

Full smooth factorization of the actual terminal primitive, with its endpoint value fixed by the coefficient. The smooth factor is constructed as an improper integral rather than assumed.

theorem NavierStokes.FlatPrimitiveFactor.integral_exp_eq_primitive (c : ℝ) (j : ℕ) (b : ℝ → ℝ) {x : ℝ} (hx : 0 ≤ x) : ∫ (u : ℝ) in 0..x, Real.exp (-c / u ^ 2) / u ^ j * b u = FlatPrimitive.primitive c j b x

theorem NavierStokes.FlatPrimitiveFactor.scale_eq_rpow (c : ℝ) (j : ℕ) {x : ℝ} (hx : 0 < x) : FlatPrimitive.scale c j x = Real.exp (-c / x ^ 2) * x ^ (3 - ↑j)

theorem NavierStokes.FlatPrimitiveFactor.exists_smooth_factor_original {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : ∃ (F : ℝ → ℝ), ContDiff ℝ (↑⊤) F ∧ F 0 = b 0 / (2 * c) ∧ ∀ (x : ℝ), 0 < x → ∫ (u : ℝ) in 0..x, Real.exp (-c / u ^ 2) / u ^ j * b u = Real.exp (-c / x ^ 2) * x ^ (3 - ↑j) * F x

The manuscript's scalar primitive factorization in its original exponential and real-power notation, with a genuine smooth extension.

theorem NavierStokes.FlatPrimitiveFactor.factor_sqrt_contDiffAt_zero {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hb0 : 0 < b 0) : ContDiffAt ℝ (↑⊤) (fun (x : ℝ) => √(factor c j b x)) 0