English
There is a Galois connection between clog_b on positive reals and zpow by b, i.e., for r>0 and z∈ℤ, r ≤ b^z iff clog_b(r) ≤ z.
Русский
Существует связь Галуа между clog_b на положительных значениях и zpow базиса b: для r>0 и z∈ℤ выполняется r ≤ b^z тогда и только тогда clog_b(r) ≤ z.
LaTeX
$$$ r>0 \Rightarrow ( r \le b^{z} \iff \operatorname{clog}_b(r) \le z ), \quad z\in\mathbb{Z}$$$
Lean4
/-- Over suitable subtypes, `Int.clog` and `zpow` form a Galois insertion -/
def clogZPowGi {b : ℕ} (hb : 1 < b) :
GaloisInsertion (fun r : Set.Ioi (0 : R) => Int.clog b (r : R)) fun z : ℤ =>
⟨(b : R) ^ z, zpow_pos (mod_cast zero_lt_one.trans hb) z⟩ :=
GaloisInsertion.monotoneIntro
(fun _ _ hz => Subtype.coe_le_coe.mp <| (zpow_right_strictMono₀ <| mod_cast hb).monotone hz)
(fun r₁ _ => clog_mono_right r₁.2) (fun _ => Subtype.coe_le_coe.mp <| self_le_zpow_clog hb _) fun _ =>
clog_zpow (R := R) hb _
