From bb7f215d9c4b4ddc4e216f49a1af25a99f84009d Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Wed, 17 Jun 2026 10:45:52 +0200 Subject: [PATCH] cleanup: golf padicLog_mul_of_norm_lt_one (#1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove dead exp-ball witness: hbxy/jxy were defined but never used (hkey only needs hbx, hby via padicLog_mul), so N := max (max jx jy) jxy collapses to max jx jy. Golf the ‖x*y-1‖<1 ultrametric bound, inline hpN, drop redundant 'from', strip narrative comments. Statement byte-for-byte unchanged; #print axioms unchanged (propext, Classical.choice, Quot.sound). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../PadicLFunctions/ValuesAtOne.lean | 37 +++++++------------ 1 file changed, 13 insertions(+), 24 deletions(-) diff --git a/projects/PadicLFunctions/PadicLFunctions/ValuesAtOne.lean b/projects/PadicLFunctions/PadicLFunctions/ValuesAtOne.lean index 4d2f4f210..5c0fba7b1 100644 --- a/projects/PadicLFunctions/PadicLFunctions/ValuesAtOne.lean +++ b/projects/PadicLFunctions/PadicLFunctions/ValuesAtOne.lean @@ -544,48 +544,37 @@ theorem padicLog_pow_pPow_of_norm_lt_one {z : K} (hz : ‖z - 1‖ < 1) (N : ℕ omit [CharZero K] in include hp in -/-- T618: multiplicativity of `padicLog` on the WHOLE open unit ball -`‖x − 1‖, ‖y − 1‖ < 1` (descend to the exp ball: choose `N` with `x^{p^N}`, `y^{p^N}`, -`(xy)^{p^N}` all in the ball — `exists_pPow_pow_inExpBall` thrice with `N := max` — apply -the exp-ball `padicLog_mul` at level `p^N` and cancel the `p^N`-scalar). -/ +/-- T618: multiplicativity of `padicLog` on the whole open unit ball: +`padicLog p (x * y) = padicLog p x + padicLog p y` when `‖x − 1‖ < 1` and `‖y − 1‖ < 1`. -/ theorem padicLog_mul_of_norm_lt_one {x y : K} (hx : ‖x - 1‖ < 1) (hy : ‖y - 1‖ < 1) : padicLog p (x * y) = padicLog p x + padicLog p y := by have hxy : ‖x * y - 1‖ < 1 := by - rw [show x * y - 1 = (x - 1) * y + (y - 1) from by ring] + rw [show x * y - 1 = (x - 1) * y + (y - 1) by ring] have hy1 : ‖y‖ ≤ 1 := by - calc ‖y‖ = ‖(y - 1) + 1‖ := by rw [sub_add_cancel] - _ ≤ max ‖y - 1‖ ‖(1 : K)‖ := IsUltrametricDist.norm_add_le_max _ _ - _ ≤ 1 := by rw [norm_one]; exact max_le hy.le le_rfl - exact lt_of_le_of_lt (IsUltrametricDist.norm_add_le_max _ _) (max_lt - (by rw [norm_mul]; exact lt_of_le_of_lt (mul_le_of_le_one_right (norm_nonneg _) hy1) hx) hy) - -- a single `p^N` lands all three in the exp ball + rw [show y = (y - 1) + 1 by ring] + exact (IsUltrametricDist.norm_add_le_max _ _).trans (by simp [hy.le]) + refine lt_of_le_of_lt (IsUltrametricDist.norm_add_le_max _ _) (max_lt ?_ hy) + rw [norm_mul] + exact (mul_le_of_le_one_right (norm_nonneg _) hy1).trans_lt hx obtain ⟨jx, hjx⟩ := exists_pPow_pow_inExpBall (p := p) hx obtain ⟨jy, hjy⟩ := exists_pPow_pow_inExpBall (p := p) hy - obtain ⟨jxy, hjxy⟩ := exists_pPow_pow_inExpBall (p := p) hxy - -- the exp ball is closed under further `p`-powering have hpow_ball : ∀ {w : K} {j : ℕ} (d : ℕ), InExpBall p (w ^ p ^ j - 1) → - InExpBall p (w ^ p ^ (j + d) - 1) := by - intro w j d hwj + InExpBall p (w ^ p ^ (j + d) - 1) := fun d hwj => by rw [pow_add, pow_mul] exact pow_mem_expBall (p := p) hwj (p ^ d) - set N : ℕ := max (max jx jy) jxy with hN + set N : ℕ := max jx jy with hN have hbx : InExpBall p (x ^ p ^ N - 1) := by - rw [hN, show max (max jx jy) jxy = jx + (max (max jx jy) jxy - jx) from by omega] + rw [hN, show max jx jy = jx + (max jx jy - jx) by omega] exact hpow_ball _ hjx have hby : InExpBall p (y ^ p ^ N - 1) := by - rw [hN, show max (max jx jy) jxy = jy + (max (max jx jy) jxy - jy) from by omega] + rw [hN, show max jx jy = jy + (max jx jy - jy) by omega] exact hpow_ball _ hjy - have hbxy : InExpBall p (x ^ p ^ N * y ^ p ^ N - 1) := by - rw [← mul_pow, hN, show max (max jx jy) jxy = jxy + (max (max jx jy) jxy - jxy) from by omega] - exact hpow_ball _ hjxy - -- the exp-ball identity at level `p^N`, transported back through the `p^N`-power law have hkey : padicLog p ((x * y) ^ p ^ N) = padicLog p (x ^ p ^ N) + padicLog p (y ^ p ^ N) := by rw [mul_pow, padicLog_mul (p := p) hbx hby] rw [padicLog_pow_pPow_of_norm_lt_one (p := p) hxy, padicLog_pow_pPow_of_norm_lt_one (p := p) hx, padicLog_pow_pPow_of_norm_lt_one (p := p) hy, ← smul_add] at hkey - have hpN : ((p : K) ^ N) ≠ 0 := pow_ne_zero _ (natCast_p_ne_zero (L := K) p) - exact smul_right_injective K hpN hkey + exact smul_right_injective K (pow_ne_zero _ (natCast_p_ne_zero (L := K) p)) hkey omit [CharZero K] in include hp in