A concrete smooth exponential-flat edge

For c > 0, this file constructs the actual function exp (-c / x^2) on x > 0, extended by zero on x ≤ 0. The proof works with polynomial multiples in x⁻¹, an explicit family closed under differentiation. It establishes smoothness, vanishing derivatives, and smooth inverse-power quotients.

These facts concern this scalar edge function, not the manuscript's stress factorization, PDE estimates, or asserted smooth force extension.

noncomputable def NavierStokes.FlatCutoff.edge (c x : ℝ) : ℝ

The one-sided Gaussian-flat edge used as a scalar model in Section 4.6.

Equations

• NavierStokes.FlatCutoff.edge c x = if x ≤ 0 then 0 else Real.exp (-c / x ^ 2)

theorem NavierStokes.FlatCutoff.edge_of_nonpos (c : ℝ) {x : ℝ} (hx : x ≤ 0) : edge c x = 0

@[simp]

theorem NavierStokes.FlatCutoff.edge_zero (c : ℝ) : edge c 0 = 0

theorem NavierStokes.FlatCutoff.edge_of_pos (c : ℝ) {x : ℝ} (hx : 0 < x) : edge c x = Real.exp (-c / x ^ 2)

theorem NavierStokes.FlatCutoff.edge_nonneg (c x : ℝ) : 0 ≤ edge c x

theorem NavierStokes.FlatCutoff.edge_pos (c : ℝ) {x : ℝ} (hx : 0 < x) : 0 < edge c x

theorem NavierStokes.FlatCutoff.edge_le_glue {c x : ℝ} (hxc : x ≤ c) : edge c x ≤ expNegInvGlue x

Near zero, the square-inverse exponential is bounded by Mathlib's already-constructed smooth inverse exponential.

noncomputable def NavierStokes.FlatCutoff.polynomialEdge (c : ℝ) (p : Polynomial ℝ) (x : ℝ) : ℝ

A family containing the edge and every inverse-power weighted edge.

Equations

• NavierStokes.FlatCutoff.polynomialEdge c p x = Polynomial.eval x⁻¹ p * NavierStokes.FlatCutoff.edge c x

@[simp]

theorem NavierStokes.FlatCutoff.polynomialEdge_zero (c : ℝ) (p : Polynomial ℝ) : polynomialEdge c p 0 = 0

theorem NavierStokes.FlatCutoff.polynomialEdge_tendsto_zero {c : ℝ} (hc : 0 < c) (p : Polynomial ℝ) : Filter.Tendsto (polynomialEdge c p) (nhds 0) (nhds 0)

Every polynomial in the inverse coordinate is defeated by this actual edge exponential. The limit is two-sided and includes the zero extension.

noncomputable def NavierStokes.FlatCutoff.derivativePolynomial (c : ℝ) (p : Polynomial ℝ) : Polynomial ℝ

The polynomial transformation induced by differentiating an inverse polynomial times the edge: 2 c X³ p - X² p'.

Equations

• NavierStokes.FlatCutoff.derivativePolynomial c p = Polynomial.C (2 * c) * Polynomial.X ^ 3 * p - Polynomial.X ^ 2 * Polynomial.derivative p

theorem NavierStokes.FlatCutoff.polynomialEdge_hasDerivAt {c : ℝ} (hc : 0 < c) (p : Polynomial ℝ) (x : ℝ) : HasDerivAt (polynomialEdge c p) (polynomialEdge c (derivativePolynomial c p) x) x

theorem NavierStokes.FlatCutoff.polynomialEdge_differentiable {c : ℝ} (hc : 0 < c) (p : Polynomial ℝ) : Differentiable ℝ (polynomialEdge c p)

theorem NavierStokes.FlatCutoff.polynomialEdge_contDiff {c : ℝ} (hc : 0 < c) (p : Polynomial ℝ) {n : ℕ∞} : ContDiff ℝ (↑n) (polynomialEdge c p)

The full inverse-polynomial family is smooth, including at the edge.

theorem NavierStokes.FlatCutoff.edge_contDiff {c : ℝ} (hc : 0 < c) {n : ℕ∞} : ContDiff ℝ (↑n) (edge c)

The concrete one-sided exponential edge is C^∞.

def NavierStokes.FlatCutoff.jetPolynomial (c : ℝ) (p : Polynomial ℝ) : ℕ → Polynomial ℝ

The explicit derivative polynomial after m differentiations.

Equations

• NavierStokes.FlatCutoff.jetPolynomial c p 0 = p
• NavierStokes.FlatCutoff.jetPolynomial c p m.succ = NavierStokes.FlatCutoff.derivativePolynomial c (NavierStokes.FlatCutoff.jetPolynomial c p m)

theorem NavierStokes.FlatCutoff.iteratedDeriv_polynomialEdge {c : ℝ} (hc : 0 < c) (p : Polynomial ℝ) (m : ℕ) : iteratedDeriv m (polynomialEdge c p) = polynomialEdge c (jetPolynomial c p m)

@[simp]

theorem NavierStokes.FlatCutoff.polynomialEdge_one (c : ℝ) : polynomialEdge c 1 = edge c

theorem NavierStokes.FlatCutoff.iteratedDeriv_edge_zero {c : ℝ} (hc : 0 < c) (m : ℕ) : iteratedDeriv m (edge c) 0 = 0

Every actual derivative vanishes at the joining point.

theorem NavierStokes.FlatCutoff.polynomialEdge_div_pow (c : ℝ) (p : Polynomial ℝ) (loss : ℕ) : (fun (x : ℝ) => polynomialEdge c p x / x ^ loss) = polynomialEdge c (p * Polynomial.X ^ loss)

Division by an arbitrary natural power stays inside the smooth family.

theorem NavierStokes.FlatCutoff.edge_div_pow_contDiff {c : ℝ} (hc : 0 < c) (loss : ℕ) {n : ℕ∞} : ContDiff ℝ ↑n fun (x : ℝ) => edge c x / x ^ loss

The total quotient, with value zero at the origin, is genuinely smooth.

theorem NavierStokes.FlatCutoff.weighted_iteratedDeriv_contDiff {c : ℝ} (hc : 0 < c) (m loss : ℕ) {n : ℕ∞} : ContDiff ℝ ↑n fun (x : ℝ) => iteratedDeriv m (edge c) x / x ^ loss

Every inverse-power weighted derivative of the edge is smooth.

theorem NavierStokes.FlatCutoff.weighted_iteratedDeriv_tendsto_zero {c : ℝ} (hc : 0 < c) (m loss : ℕ) : Filter.Tendsto (fun (x : ℝ) => iteratedDeriv m (edge c) x / x ^ loss) (nhds 0) (nhds 0)

Every derivative decays faster than every inverse power can grow. This is a limit for the constructed function, with no assumed flatness predicate.

theorem NavierStokes.FlatCutoff.edge_div_edge (c d : ℝ) : (fun (x : ℝ) => edge c x / edge d x) = edge (c - d)

Exponential flat factors can also be divided when a positive exponential margin remains. This identity includes the common zero region.

theorem NavierStokes.FlatCutoff.edge_quotient_contDiff {c d : ℝ} (hdc : d < c) {n : ℕ∞} : ContDiff ℝ ↑n fun (x : ℝ) => edge c x / edge d x