English
A structure (Galois coinsertion) exists linking z-powers with integer logarithms: base-b z-powers map to a log-map on positive reals, forming a Galois connection.
Русский
Существует структура, образующая когерентное зацепление между z-показателями и целочисленным логарифмом; основание-b задаёт связь между z^z и log_b.
LaTeX
$$$\text{zpowLogGi}_{b} = \text{GaloisCoinsertion}(\dots)\; (hb>1)$$$
Lean4
/-- Over suitable subtypes, `zpow` and `Int.log` form a Galois coinsertion -/
def zpowLogGi {b : ℕ} (hb : 1 < b) :
GaloisCoinsertion (fun z : ℤ => Subtype.mk ((b : R) ^ z) <| zpow_pos (mod_cast zero_lt_one.trans hb) z)
fun r : Set.Ioi (0 : R) => Int.log b (r : R) :=
GaloisCoinsertion.monotoneIntro (fun r₁ _ => log_mono_right r₁.2)
(fun _ _ hz => Subtype.coe_le_coe.mp <| (zpow_right_strictMono₀ <| mod_cast hb).monotone hz)
(fun r => Subtype.coe_le_coe.mp <| zpow_log_le_self hb r.2) fun _ => log_zpow (R := R) hb _
