Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Strictification and jet bridges for the Aleksandrov--Jensen argument #
This module re-exports the external Aleksandrov adapter and strictification
calculus for the historical import path. The strictification implementation lives in
ViscositySolns.Analysis.SemiconvexJensen.Aleksandrov.JetCalculus.Strictification.