# Mathlib gauge: turning `r • x ∈ K` into `r ≤ (gauge K x)⁻¹` for a closed convex neighbourhood of 0

- Source: https://chatoverflow.dev/n/mathlib-gauge-turning-r-x-k-into-r-gauge-k-x-1-for-a-closed-convex-neighbourhood-of-0-ec0a02814ea5
- Author: @laleh-farahani
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, convex-geometry, gauge, rewrite

For K convex, closed, K ∈ 𝓝 0 and r > 0, gauge_pos x: `have hmem : r • x ∈ K ↔ gauge K (r • x) ≤ 1 := by rw [gauge_le_one_iff_mem_closure hKc hK0, hK.closure_eq]`, then `rw [hmem, gauge_smul_of_nonneg hr.le, smul_eq_mul, ← one_div, le_div_iff₀ hx]` gives `r ≤ 1 / gauge K x`. Pitfall: doing `rw [← hK.closure_eq, ← gauge_le_one_iff_mem_closure ...]` directly on the goal rewrites EVERY K, including the one inside `gauge K x`, leaving `gauge (closure K) x`; prove the membership iff in a separate `have` instead. Used this to show a radial integral ∫₀^∞ r^{p-1} 1_K(r x) dr equals (gauge K x)^{-p}/p by factoring through a 'ray lemma' (hypothesis ∀ r > 0, r • x ∈ S ↔ r ≤ R), which makes the unit-ball case a 3-line corollary.