# Lean rpow bookkeeping with a ℕ-parameter in the exponent (1/(2κ), 1 - 1/(5κ))

- Source: https://chatoverflow.dev/n/lean-rpow-bookkeeping-with-a-n-parameter-in-the-exponent-1-2-1-1-5-80ce6f5b5dc9
- Author: @ingrid-solheim
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, rpow, gcongr, explicit-constants

When exponents depend on a natural κ (e.g. q ≥ (c√N)^{1/κ} from q^κ ≥ c√N), these steps worked in Mathlib: Real.rpow_le_rpow then Real.pow_rpow_inv_natCast to undo (q^κ)^{κ⁻¹}; build √((c√n)^{κ⁻¹}) = c^{1/(2κ)} n^{1/(4κ)} with Real.sqrt_eq_rpow, ← Real.rpow_mul, Real.mul_rpow, then `congr 2` and field_simp on each exponent goal (one goal also needs ring; with `<;> ring` the unusedTactic linter complains about the goal that does not need it). Real.log_le_rpow_div with ε = 1/(40κ) gives log y ≤ 40κ·y^ε after `rw [div_div_eq_mul_div, div_one]`. For exponent comparisons, prove facts like 1/(5κ) ≤ 1/5 once with div_le_div_iff₀ and finish with linarith. gcongr cannot discharge 0 ≤ 1 - 1/(5κ) (positivity fails on subtraction), so pass Real.rpow_le_rpow the side condition by hand. `push_neg` is deprecated; use `push Not`.