Actual primitives of exponential-flat edges

This file studies the integral of exp (-c / u²) * u⁻ʲ * b u from zero. The integrand uses the smooth zero extension from FlatCutoff.

In particular, smoothness of the primitive is distinct from smoothness of its quotient by an exponentially small factor. The statements below keep those obligations separate.

noncomputable def NavierStokes.FlatPrimitive.integrand (c : ℝ) (j : ℕ) (b : ℝ → ℝ) (x : ℝ) : ℝ

Integrand, given by (edge c x / x ^ j) * b x.

Equations

• NavierStokes.FlatPrimitive.integrand c j b x = NavierStokes.FlatCutoff.edge c x / x ^ j * b x

noncomputable def NavierStokes.FlatPrimitive.primitive (c : ℝ) (j : ℕ) (b : ℝ → ℝ) (x : ℝ) : ℝ

Primitive, given by ∫ u in (0 : ℝ)..x, integrand c j b u.

Equations

• NavierStokes.FlatPrimitive.primitive c j b x = ∫ (u : ℝ) in 0..x, NavierStokes.FlatPrimitive.integrand c j b u

noncomputable def NavierStokes.FlatPrimitive.scale (c : ℝ) (j : ℕ) (x : ℝ) : ℝ

The expected factor exp(-c/x²) x^(3-j), written without truncated natural subtraction and defined smoothly at zero.

Equations

• NavierStokes.FlatPrimitive.scale c j x = NavierStokes.FlatCutoff.edge c x / x ^ j * x ^ 3

theorem NavierStokes.FlatPrimitive.integrand_contDiff {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} {n : ℕ∞} (hb : ContDiff ℝ (↑n) b) : ContDiff ℝ (↑n) (integrand c j b)

theorem NavierStokes.FlatPrimitive.integrand_continuous {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : Continuous b) : Continuous (integrand c j b)

theorem NavierStokes.FlatPrimitive.primitive_hasDerivAt {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : Continuous b) (x : ℝ) : HasDerivAt (primitive c j b) (integrand c j b x) x

theorem NavierStokes.FlatPrimitive.primitive_deriv {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : Continuous b) : deriv (primitive c j b) = integrand c j b

theorem NavierStokes.FlatPrimitive.primitive_contDiff {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) : ContDiff ℝ (↑⊤) (primitive c j b)

@[simp]

theorem NavierStokes.FlatPrimitive.primitive_zero (c : ℝ) (j : ℕ) (b : ℝ → ℝ) : primitive c j b 0 = 0

theorem NavierStokes.FlatPrimitive.primitive_of_nonpos (c : ℝ) (j : ℕ) (b : ℝ → ℝ) {x : ℝ} (hx : x ≤ 0) : primitive c j b x = 0

theorem NavierStokes.FlatPrimitive.iteratedDeriv_zero_on_nonpos {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hzero : ∀ x ≤ 0, f x = 0) (m : ℕ) (x : ℝ) : x ≤ 0 → iteratedDeriv m f x = 0

Smoothness and equality to zero on a closed half-line imply that every actual derivative vanishes there. This does not assume the derivative values.

theorem NavierStokes.FlatPrimitive.primitive_iteratedDeriv_zero {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (m : ℕ) : iteratedDeriv m (primitive c j b) 0 = 0

theorem NavierStokes.FlatPrimitive.integral_derivativePolynomial {c : ℝ} (hc : 0 < c) (p : Polynomial ℝ) (x : ℝ) : ∫ (u : ℝ) in 0..x, FlatCutoff.polynomialEdge c (FlatCutoff.derivativePolynomial c p) u = FlatCutoff.polynomialEdge c p x

Exact fundamental theorem of calculus for the explicit derivative polynomial family constructed in FlatCutoff.

theorem NavierStokes.FlatPrimitive.edge_hasDerivAt {c : ℝ} (hc : 0 < c) (x : ℝ) : HasDerivAt (FlatCutoff.edge c) (2 * c * FlatCutoff.edge c x / x ^ 3) x

theorem NavierStokes.FlatPrimitive.scale_contDiff {c : ℝ} (hc : 0 < c) (j : ℕ) {n : ℕ∞} : ContDiff ℝ (↑n) (scale c j)

@[simp]

theorem NavierStokes.FlatPrimitive.scale_zero (c : ℝ) (j : ℕ) : scale c j 0 = 0

theorem NavierStokes.FlatPrimitive.scale_hasDerivAt {c : ℝ} (hc : 0 < c) (j : ℕ) (x : ℝ) : HasDerivAt (scale c j) (FlatCutoff.edge c x / x ^ j * (2 * c + (3 - ↑j) * x ^ 2)) x

noncomputable def NavierStokes.FlatPrimitive.sourceCoefficient (c : ℝ) (j : ℕ) (a : ℝ → ℝ) (x : ℝ) : ℝ

The coefficient produced when differentiating scale c j * a. This is an explicit differential expression in the chosen smooth factor.

Equations

• NavierStokes.FlatPrimitive.sourceCoefficient c j a x = (2 * c + (3 - ↑j) * x ^ 2) * a x + x ^ 3 * deriv a x

theorem NavierStokes.FlatPrimitive.sourceCoefficient_contDiff (c : ℝ) (j : ℕ) {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) : ContDiff ℝ (↑⊤) (sourceCoefficient c j a)

theorem NavierStokes.FlatPrimitive.primitive_sourceCoefficient {c : ℝ} (hc : 0 < c) (j : ℕ) {a : ℝ → ℝ} (ha : ContDiff ℝ (↑⊤) a) (x : ℝ) : primitive c j (sourceCoefficient c j a) x = scale c j x * a x

A genuine primitive factorization for the explicit family of coefficients obtained from any smooth factor a, proved by the fundamental theorem of calculus rather than assumed as a representation hypothesis.

theorem NavierStokes.FlatPrimitive.primitive_recurrence {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : ContDiff ℝ (↑⊤) b) (x : ℝ) : 2 * c * primitive c j b x = scale c j x * b x - primitive c j (sourceCoefficient 0 j b) x

An exact integration-by-parts recurrence for every smooth coefficient. The new coefficient is (3-j) x² b + x³ b', which vanishes to at least second order at the endpoint.

theorem NavierStokes.FlatPrimitive.primitive_three_one {c : ℝ} (hc : 0 < c) (x : ℝ) : primitive c 3 (fun (x : ℝ) => 1) x = FlatCutoff.edge c x / (2 * c)

An exact constant-coefficient case of the claimed terminal factorization: for j = 3, the remaining smooth factor is the constant 1 / (2c).

theorem NavierStokes.FlatPrimitive.scale_pos (c : ℝ) (j : ℕ) {x : ℝ} (hx : 0 < x) : 0 < scale c j x

The natural primitive scale is strictly positive inside the active edge.

theorem NavierStokes.FlatPrimitive.primitive_normalized_tendsto {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : Continuous b) : Filter.Tendsto (fun (x : ℝ) => primitive c j b x / scale c j x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (b 0 / (2 * c)))

The leading quotient limit for an arbitrary continuous coefficient. This is a genuine asymptotic statement about the integral; smoothness of the quotient to all orders is a stronger assertion.

noncomputable def NavierStokes.FlatPrimitive.normalizedPrimitive (c : ℝ) (j : ℕ) (b : ℝ → ℝ) (x : ℝ) : ℝ

The normalized factor with its rigorously identified endpoint value.

Equations

• NavierStokes.FlatPrimitive.normalizedPrimitive c j b x = if x = 0 then b 0 / (2 * c) else NavierStokes.FlatPrimitive.primitive c j b x / NavierStokes.FlatPrimitive.scale c j x

theorem NavierStokes.FlatPrimitive.normalizedPrimitive_continuousWithinAt_zero {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : Continuous b) : ContinuousWithinAt (normalizedPrimitive c j b) (Set.Ici 0) 0

theorem NavierStokes.FlatPrimitive.normalizedPrimitive_factorization (c : ℝ) (j : ℕ) (b : ℝ → ℝ) {x : ℝ} (hx : 0 ≤ x) : primitive c j b x = scale c j x * normalizedPrimitive c j b x

The actual integral factors on the closed positive half-line, with the factor proved continuous at zero above. No smoothness conclusion is inferred merely from this quotient definition.

theorem NavierStokes.FlatPrimitive.primitive_normalized_eventually_pos {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : Continuous b) (hb0 : 0 < b 0) : ∀ᶠ (x : ℝ) in nhdsWithin 0 (Set.Ioi 0), 0 < primitive c j b x / scale c j x

A strictly positive endpoint coefficient gives an actual positive normalized primitive on a sufficiently short terminal interval.

theorem NavierStokes.FlatPrimitive.primitive_div_pow_tendsto_zero {c : ℝ} (hc : 0 < c) (j : ℕ) {b : ℝ → ℝ} (hb : Continuous b) (loss : ℕ) : Filter.Tendsto (fun (x : ℝ) => primitive c j b x / x ^ loss) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The actual primitive vanishes faster than every natural power, even for a merely continuous coefficient. This does not assume flatness of the primitive or a factorization by a smooth function.