Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Doubled-variable localization estimates for proper comparison.

The development lives in the Localization/ submodules; this file re-exports all of them.