A smooth convex profile vanishing on the nonpositive half-line

The energy of the comparison argument of lem:aniso:comparison measures the excess of the mollified solution over the barrier through a profile G applied pointwise. The manuscript uses G(y) = (y₊)² (eq:aniso:comparison:positive:energy); here G is the primitive G(y) = ∫₀^y smoothTransition of Mathlib's smooth monotone transition function. It has the three properties the argument uses of (y₊)²: it vanishes exactly on (-∞, 0], it is convex with 0 ≤ G' ≤ 1, and it is smooth, so that G ∘ w is an admissible test function whenever w is smooth with w < 0 off a compact set.

The last part of the file is the chain rule for G along a primitive c + ∫ₐᵗ h of an integrable function, obtained from absolute continuity.

noncomputable def CIV.comparisonProfile (y : ℝ) : ℝ

The comparison profile G(y) = ∫₀^y smoothTransition.

Equations

• CIV.comparisonProfile y = ∫ (t : ℝ) in 0..y, t.smoothTransition

theorem CIV.hasDerivAt_comparisonProfile (y : ℝ) : HasDerivAt comparisonProfile y.smoothTransition y

theorem CIV.differentiable_comparisonProfile : Differentiable ℝ comparisonProfile

theorem CIV.deriv_comparisonProfile : deriv comparisonProfile = Real.smoothTransition

theorem CIV.contDiff_comparisonProfile : ContDiff ℝ (↑⊤) comparisonProfile

theorem CIV.comparisonProfile_eq_zero_of_nonpos {y : ℝ} (hy : y ≤ 0) : comparisonProfile y = 0

theorem CIV.comparisonProfile_pos {y : ℝ} (hy : 0 < y) : 0 < comparisonProfile y

theorem CIV.comparisonProfile_nonneg (y : ℝ) : 0 ≤ comparisonProfile y

theorem CIV.comparisonProfile_eq_zero_iff {y : ℝ} : comparisonProfile y = 0 ↔ y ≤ 0

theorem CIV.lipschitzWith_comparisonProfile : LipschitzWith 1 comparisonProfile

G is 1-Lipschitz, since 0 ≤ G' ≤ 1.

theorem CIV.abs_comparisonProfile_sub_le (a b : ℝ) : |comparisonProfile a - comparisonProfile b| ≤ |a - b|

theorem CIV.comparisonProfile_add_intervalIntegral {h : ℝ → ℝ} {a b : ℝ} (hh : IntervalIntegrable h MeasureTheory.volume a b) (c : ℝ) : comparisonProfile (c + ∫ (s : ℝ) in a..b, h s) = comparisonProfile c + ∫ (s : ℝ) in a..b, (c + ∫ (r : ℝ) in a..s, h r).smoothTransition * h s

Chain rule for G along a primitive: if h is integrable on [a, b], then G(c + ∫ₐᵇ h) = G(c) + ∫ₐᵇ G'(c + ∫ₐˢ h) h(s) ds.