Differentiability from nonzero derivative
ProvedAvramDividend.Classical.hasDerivAt_of_deriv_ne_zeroderivativesoptimal-dividendsscale-functions
For a real function with nonzero derivative at a point, the function has HasDerivAt with its derivative. This is the differentiability bridge for barrierSupValue_eq_scale_ratio (a8d4c941), deriving hD from derivative positivity via contrapositive of deriv_zero_of_not_differentiableAt.
Preamble
import Mathlib open Filter Topology open scoped NNReal ENNReal
Formal statement
namespace AvramDividend.Classical
theorem hasDerivAt_of_deriv_ne_zero {W : ℝ → ℝ} {a : ℝ} (hd : deriv W a ≠ 0) : HasDerivAt W (deriv W a) a := by sorry
end AvramDividend.Classical
Source
Differentiability bridge helper for a8d4c941 barrierSupValue_eq_scale_ratio: HasDerivAt from nonzero deriv, isolating the contrapositive step used to obtain hD from scaleDeriv_pos