The smooth transition function and cutoffs near zero

Mathlib's Analysis/SpecialFunctions/SmoothTransition.lean proves that Real.smoothTransition is smooth and equals one on [1, ∞), but states no derivative values. This file records that its derivative vanishes on the open rays (-∞, 0) and (1, ∞), where the function is locally constant, so that the derivative is compactly supported. Being continuous, it is then bounded, which bounds the gradients of cutoffs built from Real.smoothTransition. It is also integrable with integral one, so its rescalings t ↦ c ψ'(c (a - t)) are approximate identities; together with the chain rule and local Lipschitz continuity of ψ (c (u - t)), this is what is needed to smooth the indicator of a superlevel set {u > t}. The one-sided rescalings y ↦ c ψ'(c (y - a)), supported in [a, a + c⁻¹], converge at every Lebesgue point: if the mean oscillation of u about v on closedBall a r tends to zero, then ∫ c ψ'(c (y - a)) u y dy → v as c → ∞. Pairing a function with the derivative of a smooth step ψ (c (y - a)) therefore recovers its Lebesgue value at a.

It also uses the smooth transition to cut a function off near zero. For m > 0 and a function g : ℝ → ℝ, TauCeti.positiveCutoff m g is the product of g with a smooth transition from 0 to 1 on [m/4, m/2]. It vanishes for t ≤ m/4 and agrees with g for t ≥ m/2, so it is a globally defined replacement for a function such as t ↦ 1/t or Real.log that is only well behaved on (0, ∞). If g is C¹ on (0, ∞) then the cutoff is C¹ on ℝ, and if g' is bounded on [m, ∞) then the derivative of the cutoff is bounded on ℝ; these are the hypotheses of chain rules for Sobolev functions. Finally, rescaling the smooth transition gives a smooth nonincreasing step from any value v ≥ 0 down to 0 across an interval [a, b]. A smooth plateau, built from two smooth transitions, is equal to 1 on [a + δ, b - δ] and vanishes outside (a, b); integrating it gives such a step with slope at most τ whenever v < τ (b - a), which is the best possible bound, since the mean slope of the step is v / (b - a).

Main declarations

• expNegInvGlue.lt_one: expNegInvGlue x < 1.
• expNegInvGlue.hasDerivAt: the derivative of expNegInvGlue at x is x⁻² expNegInvGlue x.
• Real.smoothTransition.abs_le_one: |Real.smoothTransition x| ≤ 1.
• Real.smoothTransition.deriv_of_neg: deriv Real.smoothTransition x = 0 for x < 0.
• Real.smoothTransition.deriv_of_one_lt: deriv Real.smoothTransition x = 0 for 1 < x.
• Real.smoothTransition.hasCompactSupport_deriv: the derivative is compactly supported.
• Real.smoothTransition.deriv_deriv_of_neg: the second derivative vanishes on the negative half-line.
• Real.smoothTransition.exists_forall_norm_deriv_le and Real.smoothTransition.exists_forall_norm_deriv_deriv_le: the first two derivatives are bounded.
• Real.smoothTransition.abs_deriv_mul_mul_le: |ψ'(a t) (a y)| ≤ M C when M bounds ψ', a ≥ 0 and |y| ≤ C |t|.
• Real.smoothTransition.integral_deriv: the derivative has integral one.
• Real.smoothTransition.setIntegral_Icc_deriv, Real.smoothTransition.setIntegral_deriv_le_one: its integral over an interval containing [0, 1] is one, and over any set at most one.
• Real.smoothTransition.lintegral_ofReal_mul_deriv: ∫_ℝ c ψ'(c (a - t)) dt = 1 for c > 0.
• Real.smoothTransition.integral_mul_deriv_mul_sub: ∫_ℝ c ψ'(c (y - a)) dy = 1 for c > 0.
• Real.smoothTransition.integral_deriv_mul_sub: ∫_ℝ ψ'(c y - a) dy = |c|⁻¹.
• Real.smoothTransition.lintegral_ofReal_deriv_mul_sub and Real.smoothTransition.lintegral_ofReal_deriv_sub_mul: ∫⁻_ℝ ψ'(± (c y - a)) dy = |c|⁻¹.
• Real.smoothTransition.tendsto_integral_deriv_mul_sub_mul: ∫_ℝ ψ'(c y - T) a y dy tends to |c|⁻¹ a₀ as T → ∞ when a (c⁻¹ σ) → a₀ as σ → ∞.
• Real.smoothTransition.integrable_mul_deriv_mul_sub_smul: its product with a function integrable on closedBall a c⁻¹ is integrable.
• Real.smoothTransition.tendsto_integral_mul_deriv_mul_sub_smul: at a Lebesgue point a of u with value v, ∫ c ψ'(c (y - a)) u y dy → v as c → ∞.
• HasFDerivAt.smoothTransition and HasDerivAt.smoothTransition: the chain rule for ψ ∘ f.
• LocallyLipschitzOn.smoothTransition_mul_sub: ψ (c (u - t)) is locally Lipschitz on s when u is.
• TauCeti.positiveCutoff: the cutoff of g near zero.
• TauCeti.contDiff_positiveCutoff: the cutoff of a function that is C¹ on (0, ∞) is C¹.
• TauCeti.exists_nnnorm_deriv_positiveCutoff_le: its derivative is bounded when g' is bounded on [m, ∞).
• TauCeti.exists_contDiff_antitone_cutoff: a smooth nonincreasing step from a value v ≥ 0 on (-∞, a] down to 0 on [b, ∞), positive on (-∞, b) when v > 0.
• TauCeti.exists_contDiff_plateau: a smooth function with values in [0, 1], vanishing outside (a, b) and equal to 1 on [a + δ, b - δ].
• TauCeti.exists_contDiff_antitone_cutoff_abs_deriv_le: such a step whose slope is at most τ, for every v < τ (b - a).

theorem expNegInvGlue.lt_one (x : ℝ) : expNegInvGlue x < 1

The function expNegInvGlue is less than 1 everywhere.

theorem expNegInvGlue.hasDerivAt (x : ℝ) : HasDerivAt expNegInvGlue (x⁻¹ ^ 2 * expNegInvGlue x) x

The derivative of expNegInvGlue at x is x⁻² expNegInvGlue x, also for x ≤ 0, where both sides vanish.

theorem Real.smoothTransition.abs_le_one (x : ℝ) : |x.smoothTransition| ≤ 1

The smooth transition function takes values of absolute value at most one.

theorem Real.smoothTransition.deriv_of_neg {x : ℝ} (hx : x < 0) : deriv smoothTransition x = 0

The smooth transition function has derivative zero to the left of 0, where it is identically zero.

theorem Real.smoothTransition.deriv_of_one_lt {x : ℝ} (hx : 1 < x) : deriv smoothTransition x = 0

The smooth transition function has derivative zero to the right of 1, where it is identically one.

theorem Real.smoothTransition.hasCompactSupport_deriv : HasCompactSupport (deriv smoothTransition)

The derivative of the smooth transition function is supported in [0, 1].

theorem Real.smoothTransition.deriv_deriv_of_neg {x : ℝ} (hx : x < 0) : deriv (deriv smoothTransition) x = 0

The second derivative of the smooth transition function is zero to the left of 0.

theorem Real.smoothTransition.exists_forall_norm_deriv_le : ∃ (L : ℝ), ∀ (τ : ℝ), ‖deriv smoothTransition τ‖ ≤ L

The derivative of the smooth transition function is bounded.

theorem Real.smoothTransition.exists_forall_norm_deriv_deriv_le : ∃ (L : ℝ), ∀ (τ : ℝ), ‖deriv (deriv smoothTransition) τ‖ ≤ L

The second derivative of the smooth transition function is bounded.

theorem Real.smoothTransition.abs_deriv_mul_mul_le {M C a t y : ℝ} (hM : ∀ (t : ℝ), ‖deriv smoothTransition t‖ ≤ M) (hC : 0 ≤ C) (ha : 0 ≤ a) (hy : |y| ≤ C * |t|) : |deriv smoothTransition (a * t) * (a * y)| ≤ M * C

A bound for the error term of a smooth transition rescaled by a ≥ 0: if M bounds the derivative of the smooth transition function ψ and |y| ≤ C |t|, then |ψ'(a t) (a y)| ≤ M C. The factor a y only matters where 0 ≤ a t ≤ 1, the support of ψ', and there |a y| ≤ C |a t| ≤ C.

theorem Real.smoothTransition.integrable_deriv : MeasureTheory.Integrable (deriv smoothTransition) MeasureTheory.volume

The derivative of the smooth transition function is integrable.

@[simp]

theorem Real.smoothTransition.integral_deriv : ∫ (x : ℝ), deriv smoothTransition x = 1

The derivative of the smooth transition function has integral one, the total increase of the function from 0 to 1.

theorem Real.smoothTransition.setIntegral_Icc_deriv {a b : ℝ} (ha : a ≤ 0) (hb : 1 ≤ b) : ∫ (x : ℝ) in Set.Icc a b, deriv smoothTransition x = 1

Over any interval [a, b] containing [0, 1], the derivative of the smooth transition function has integral one, its total increase.

theorem Real.smoothTransition.setIntegral_deriv_le_one (s : Set ℝ) : ∫ (x : ℝ) in s, deriv smoothTransition x ≤ 1

Over any set, the derivative of the smooth transition function has integral at most one.

@[simp]

theorem Real.smoothTransition.lintegral_ofReal_mul_deriv (a : ℝ) {c : ℝ} (hc : 0 < c) : ∫⁻ (t : ℝ), ENNReal.ofReal (c * deriv smoothTransition (c * (a - t))) = 1

The rescaled derivatives t ↦ c ψ'(c (a - t)) of the smooth transition function ψ integrate to one: ∫_ℝ c ψ'(c (a - t)) dt = 1 for c > 0.

@[simp]

theorem Real.smoothTransition.integral_mul_deriv_mul_sub (a : ℝ) {c : ℝ} (hc : 0 < c) : ∫ (y : ℝ), c * deriv smoothTransition (c * (y - a)) = 1

The rescaled derivatives y ↦ c ψ'(c (y - a)) of the smooth transition function ψ integrate to one: ∫_ℝ c ψ'(c (y - a)) dy = 1 for c > 0.

theorem Real.smoothTransition.integral_deriv_mul_sub (c a : ℝ) : ∫ (y : ℝ), deriv smoothTransition (c * y - a) = |c|⁻¹

The derivative of the smooth transition function ψ, composed with an affine map y ↦ c y - a, has integral |c|⁻¹: ∫_ℝ ψ'(c y - a) dy = |c|⁻¹.

theorem Real.smoothTransition.lintegral_ofReal_deriv_mul_sub (a : ℝ) {c : ℝ} (hc : c ≠ 0) : ∫⁻ (s : ℝ), ENNReal.ofReal (deriv smoothTransition (c * s - a)) = ENNReal.ofReal |c|⁻¹

The rescaled derivative s ↦ ψ'(c s - a) of the smooth transition function ψ has integral |c|⁻¹ for c ≠ 0, the total increase of ψ divided by the speed |c| at which it is traversed.

theorem Real.smoothTransition.lintegral_ofReal_deriv_sub_mul (a : ℝ) {c : ℝ} (hc : c ≠ 0) : ∫⁻ (y : ℝ), ENNReal.ofReal (deriv smoothTransition (a - c * y)) = ENNReal.ofReal |c|⁻¹

The derivative of the smooth transition function ψ, evaluated at the affine argument a - c y with c ≠ 0, has lower Lebesgue integral |c|⁻¹: ∫⁻_ℝ ψ'(a - c y) dy = |c|⁻¹.

theorem Real.smoothTransition.tendsto_integral_deriv_mul_sub_mul {c : ℝ} (hc : c ≠ 0) {a : ℝ → ℝ} {a₀ : ℝ} (ha : Filter.Tendsto (fun (σ : ℝ) => a (c⁻¹ * σ)) Filter.atTop (nhds a₀)) (hint : ∀ᶠ (T : ℝ) in Filter.atTop, MeasureTheory.Integrable (fun (y : ℝ) => deriv smoothTransition (c * y - T) * a y) MeasureTheory.volume) : Filter.Tendsto (fun (T : ℝ) => ∫ (y : ℝ), deriv smoothTransition (c * y - T) * a y) Filter.atTop (nhds (|c|⁻¹ * a₀))

Averaging a function a against the derivative ψ'(c y - T) of the smooth transition function ψ, for c ≠ 0, recovers |c|⁻¹ times its limit a₀ along the direction of c as T → ∞: the weight has integral |c|⁻¹ and is supported where c y ≥ T.

theorem Real.smoothTransition.deriv_mul_sub_eq_zero {a c y : ℝ} (hc : 0 < c) (hy : y ∉ Metric.closedBall a c⁻¹) : deriv smoothTransition (c * (y - a)) = 0

The rescaled derivative y ↦ ψ'(c (y - a)) of the smooth transition function ψ vanishes outside closedBall a c⁻¹; it is supported in [a, a + c⁻¹].

theorem Real.smoothTransition.integrable_mul_deriv_mul_sub_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {u : ℝ → E} {a c : ℝ} (hc : 0 < c) (hu : MeasureTheory.IntegrableOn u (Metric.closedBall a c⁻¹) MeasureTheory.volume) : MeasureTheory.Integrable (fun (y : ℝ) => (c * deriv smoothTransition (c * (y - a))) • u y) MeasureTheory.volume

The product of the rescaled derivative y ↦ c ψ'(c (y - a)) of the smooth transition function ψ with a function integrable on closedBall a c⁻¹ is integrable.

theorem Real.smoothTransition.tendsto_integral_mul_deriv_mul_sub_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {u : ℝ → E} {a : ℝ} {v : E} (hu : MeasureTheory.IntegrableAtFilter u (nhds a) MeasureTheory.volume) (hv : Filter.Tendsto (fun (r : ℝ) => ⨍ (y : ℝ) in Metric.closedBall a r, ‖u y - v‖) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) : Filter.Tendsto (fun (c : ℝ) => ∫ (y : ℝ), (c * deriv smoothTransition (c * (y - a))) • u y) Filter.atTop (nhds v)

The rescaled derivatives of the smooth transition function are an approximate identity at Lebesgue points. If u is integrable near a and its mean oscillation about v on closedBall a r tends to zero as r → 0, then ∫ c ψ'(c (y - a)) u y dy → v as c → ∞.

theorem Real.smoothTransition.tendsto_add_mul_add_deriv_mul {t d e k : ℝ} : Filter.Tendsto (fun (n : ℕ) => d + ((↑n + 1) * t).smoothTransition * e + deriv smoothTransition ((↑n + 1) * t) * ((↑n + 1) * k)) Filter.atTop (nhds (if t ≤ 0 then d else d + e))

The pointwise limit of d + ψ ((n + 1) t) e + ψ' ((n + 1) t) ((n + 1) k) for the smooth transition ψ: the sequence tends to d for t ≤ 0 and to d + e for 0 < t. At t = 0 the last term vanishes because ψ' 0 = 0, whatever k is.

theorem Real.smoothTransition.le_add_one_sub (x : ℝ) : x ≤ x + (1 - x.smoothTransition)

x + (1 - smoothTransition x) is at least x.

theorem Real.smoothTransition.add_one_sub_ne_zero {x : ℝ} (hx : 0 ≤ x) : x + (1 - x.smoothTransition) ≠ 0

x + (1 - smoothTransition x) is nonzero for x ≥ 0.

theorem HasFDerivAt.smoothTransition {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E →L[ℝ] ℝ} {x : E} (hf : HasFDerivAt f f' x) : HasFDerivAt (fun (y : E) => (f y).smoothTransition) (deriv Real.smoothTransition (f x) • f') x

The chain rule for the smooth transition function ψ: if f has derivative f' at x, then ψ ∘ f has derivative ψ'(f x) • f' there.

theorem HasDerivAt.smoothTransition {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) : HasDerivAt (fun (y : ℝ) => (f y).smoothTransition) (_root_.deriv Real.smoothTransition (f x) * f') x

The chain rule for the smooth transition function ψ in one variable: if f has derivative f' at x, then ψ ∘ f has derivative ψ'(f x) * f' there.

theorem LocallyLipschitzOn.smoothTransition_mul_sub {α : Type u_1} [PseudoEMetricSpace α] {s : Set α} {u : α → ℝ} (hu : LocallyLipschitzOn s u) (c t : ℝ) : LocallyLipschitzOn s fun (x : α) => (c * (u x - t)).smoothTransition

If u is locally Lipschitz on s, then so is ψ (c (u - t)) for the smooth transition function ψ.

noncomputable def TauCeti.positiveCutoff (m : ℝ) (g : ℝ → ℝ) (t : ℝ) : ℝ

The function t ↦ s((4t - m)/m) g(t), where s is Real.smoothTransition. For m > 0 it vanishes for t ≤ m/4 and agrees with g for t ≥ m/2, so it is a globally defined replacement for a function g that is only well behaved on (0, ∞).

@[simp]

theorem TauCeti.positiveCutoff_of_le {m : ℝ} (hm : 0 < m) (g : ℝ → ℝ) {t : ℝ} (ht : t ≤ m / 4) : positiveCutoff m g t = 0

The cutoff vanishes on (-∞, m/4].

@[simp]

theorem TauCeti.positiveCutoff_of_ge {m : ℝ} (hm : 0 < m) (g : ℝ → ℝ) {t : ℝ} (ht : m / 2 ≤ t) : positiveCutoff m g t = g t

The cutoff agrees with g on [m/2, ∞).

theorem TauCeti.positiveCutoff_eventuallyEq {m : ℝ} (hm : 0 < m) (g : ℝ → ℝ) {t : ℝ} (ht : m / 2 < t) : positiveCutoff m g =ᶠ[nhds t] g

The cutoff agrees with g near every point of (m/2, ∞).

theorem TauCeti.deriv_positiveCutoff {m : ℝ} (hm : 0 < m) (g : ℝ → ℝ) {t : ℝ} (ht : m / 2 < t) : deriv (positiveCutoff m g) t = deriv g t

On (m/2, ∞) the derivative of the cutoff is the derivative of g.

theorem TauCeti.positiveCutoff_nonneg {m : ℝ} (hm : 0 < m) {g : ℝ → ℝ} (hg : ∀ (t : ℝ), 0 < t → 0 ≤ g t) (t : ℝ) : 0 ≤ positiveCutoff m g t

The cutoff of a function that is nonnegative on (0, ∞) is nonnegative.

theorem TauCeti.contDiff_positiveCutoff {m : ℝ} (hm : 0 < m) {g : ℝ → ℝ} (hg : ∀ (t : ℝ), 0 < t → ContDiffAt ℝ 1 g t) : ContDiff ℝ 1 (positiveCutoff m g)

The cutoff of a function that is C¹ on (0, ∞) is C¹ on the whole line.

theorem TauCeti.exists_nnnorm_deriv_positiveCutoff_le {m : ℝ} (hm : 0 < m) {g : ℝ → ℝ} (hg : ∀ (t : ℝ), 0 < t → ContDiffAt ℝ 1 g t) {K : ℝ} (hK : ∀ (t : ℝ), m ≤ t → |deriv g t| ≤ K) : ∃ (M : NNReal), ∀ (t : ℝ), ‖deriv (positiveCutoff m g) t‖₊ ≤ M

If g is C¹ on (0, ∞) and |g'| ≤ K on [m, ∞), then the derivative of the cutoff is bounded on the whole line.

theorem TauCeti.exists_contDiff_antitone_cutoff {a b v : ℝ} (hab : a < b) (hv : 0 ≤ v) : ∃ (μ : ℝ → ℝ), ContDiff ℝ (↑⊤) μ ∧ Antitone μ ∧ (∀ (r : ℝ), 0 ≤ μ r) ∧ (∀ (r : ℝ), b ≤ r → μ r = 0) ∧ (∀ r ≤ a, μ r = v) ∧ (0 < v → ∀ r < b, 0 < μ r)

A smooth nonincreasing step down from a value v ≥ 0 to 0: for a < b there is a smooth antitone function μ ≥ 0 equal to v on (-∞, a] and to 0 on [b, ∞). When v > 0 it is positive on (-∞, b), so b is exactly where it reaches 0.

theorem TauCeti.exists_contDiff_plateau {a b δ : ℝ} (hδ : 0 < δ) : ∃ (ψ : ℝ → ℝ), ContDiff ℝ (↑⊤) ψ ∧ (∀ (r : ℝ), 0 ≤ ψ r) ∧ (∀ (r : ℝ), ψ r ≤ 1) ∧ (∀ r ∉ Set.Ioo a b, ψ r = 0) ∧ (∀ r ∈ Set.Icc (a + δ) (b - δ), ψ r = 1) ∧ b - a - 2 * δ ≤ ∫ (r : ℝ) in a..b, ψ r

A smooth plateau on [a, b]: for δ > 0 there is a smooth function with values in [0, 1], vanishing outside (a, b) and equal to 1 on [a + δ, b - δ]. Its integral over [a, b] is therefore at least b - a - 2δ.

theorem TauCeti.exists_contDiff_antitone_cutoff_abs_deriv_le {a b v τ : ℝ} (hab : a < b) (hv : 0 ≤ v) (hvτ : v < τ * (b - a)) : ∃ (μ : ℝ → ℝ), ContDiff ℝ (↑⊤) μ ∧ Antitone μ ∧ (∀ (r : ℝ), 0 ≤ μ r) ∧ (∀ (r : ℝ), b ≤ r → μ r = 0) ∧ (∀ r ≤ a, μ r = v) ∧ (∀ (r : ℝ), |deriv μ r| ≤ τ) ∧ ∀ r ∉ Set.Ioo a b, deriv μ r = 0

A smooth nonincreasing step down from v ≥ 0 to 0 across [a, b] with slope at most τ: if v < τ (b - a), there is a smooth antitone function μ ≥ 0 equal to v on (-∞, a] and to 0 on [b, ∞), with |μ'| ≤ τ everywhere and μ' = 0 outside (a, b).