Documentation

LeanPool.ViscositySolutionTheory.ViscositySolns.Analysis.SemiconvexJensen.Strictification

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.