The Differentiable Sandwich Lemma

A function squeezed between two functions that are differentiable at a point, and agreeing with both at that point, is itself differentiable there, with the same derivative.

This is Lemma 1 of Clausen and Strub (2020), "Reverse Calculus and Nested Optimization", Journal of Economic Theory 187, 105019, and it is the foundation of their approach to envelope theorems. Their point is that it needs neither concavity nor interiority, so it applies where Benveniste–Scheinkman does not — in particular where a constraint binds, which in a Bewley economy is exactly the states that matter, since the borrowing constraint is where the whole ergodic argument lives.

The proof is two moves. The gap U - L is nonnegative near the point and vanishes at it, so it has a local minimum there and its derivative is zero, which forces the two derivatives to agree. Then the difference quotients of F are squeezed between those of L and U.

Mathlib has the local-minimum step (IsLocalMin.hasDerivAt_eq_zero) but not this lemma.

theorem hasDerivAt_of_sandwich {F L U : ℝ → ℝ} {c l u : ℝ} {N : Set ℝ} (hN : N ∈ nhds c) (hLF : ∀ x ∈ N, L x ≤ F x) (hFU : ∀ x ∈ N, F x ≤ U x) (hLc : L c = F c) (hUc : U c = F c) (hL : HasDerivAt L l c) (hU : HasDerivAt U u c) : l = u ∧ HasDerivAt F l c

Differentiable Sandwich Lemma (Clausen–Strub 2020, Lemma 1). If F is squeezed between L and U near c, all three agree at c, and L and U are differentiable at c, then the two derivatives coincide and F is differentiable at c with that derivative.

The supporting line

The upper half of the sandwich, for a concave function of one real variable. Mathlib has no subgradient or supporting-hyperplane theory for convex or concave FUNCTIONS, but in one dimension the slope API suffices: ConcaveOn.slope_anti says secant slopes through a point are antitone, so every slope to the left is at least every slope to the right, and the infimum of the left slopes separates them.

Clausen and Strub note that concavity is needed only for this half — the lower bound in the sandwich need not be concave, which is where they improve on Rockafellar's antecedent. For a value function that matters: concavity is available here, and the lazy agent's lower bound would not have to be concave in the state.

theorem ConcaveOn.exists_supportingLine {f : ℝ → ℝ} {s : Set ℝ} (hf : ConcaveOn ℝ s f) {x : ℝ} (hx : x ∈ s) (hlt : ∃ y ∈ s, y < x) (hgt : ∃ y ∈ s, x < y) : ∃ (m : ℝ), ∀ y ∈ s, f y ≤ f x + m * (y - x)

A concave function has a supporting line at any point with neighbours on both sides. The slope is the infimum of the secant slopes to the left.

theorem ConcaveOn.hasDerivAt_of_lowerBound {f L : ℝ → ℝ} {s : Set ℝ} {x l : ℝ} (hf : ConcaveOn ℝ s f) (hx : x ∈ s) (hs : s ∈ nhds x) (hlt : ∃ y ∈ s, y < x) (hgt : ∃ y ∈ s, x < y) (hLf : ∀ y ∈ s, L y ≤ f y) (hLx : L x = f x) (hL : HasDerivAt L l x) : HasDerivAt f l x

A concave function with a differentiable lower bound touching at a point is differentiable there, with the lower bound's derivative.

This is the form the envelope theorem uses: concavity supplies the upper half of the sandwich automatically, so only the lower bound has to be produced, and Clausen and Strub produce it with the lazy agent — freeze the optimal choice and vary the state, which is differentiable because the state then enters only through the reward.