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

Perron-family lower conclusion interfaces

Perron existence theorems using the canonical Perron-family upper side and lower-side conclusions from the bump argument. The development lives in the LowerInterfaces/ submodules; this file re-exports all of them.