Skip to content

chore(Data/Int/WithZero): use log in WithZeroMulInt.toNNReal #43589

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mariainesdff wants to merge 1 commit into
base: master
Choose a base branch
from
Open

chore(Data/Int/WithZero): use log in WithZeroMulInt.toNNReal #43589

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 6 additions & 7 deletions Mathlib/Data/Int/WithZero.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,9 @@ namespace WithZeroMulInt
/-- Given a nonzero `e : ℝ≥0`, this is the map `ℤᵐ⁰ → ℝ≥0` sending `0 ↦ 0` and
`x ↦ e^(WithZero.unzero hx).toAdd` when `x ≠ 0` as a `MonoidWithZeroHom`. -/
def toNNReal {e : ℝ≥0} (he : e ≠ 0) : ℤᵐ⁰ →*₀ ℝ≥0 where
toFun := fun x ↦ if hx : x = 0 then 0 else e ^ (WithZero.unzero hx).toAdd
toFun := fun x ↦ if hx : x = 0 then 0 else e ^ log x
map_zero' := rfl
map_one' := by rw [dite_eq_right one_ne_zero, unzero_coe (x := 1), toAdd_one, zpow_zero]
map_one' := by rw [dite_eq_right one_ne_zero, log_one, zpow_zero]
map_mul' x y := by
by_cases hxy : x * y = 0
· rcases mul_eq_zero.mp hxy with hx | hy
Expand All @@ -55,17 +55,15 @@ def toNNReal {e : ℝ≥0} (he : e ≠ 0) : ℤᵐ⁰ →*₀ ℝ≥0 where
· obtain ⟨hx, hy⟩ := mul_ne_zero_iff.mp hxy
-- x ≠ 0 and y ≠ 0
rw [dite_eq_right hxy, dite_eq_right hx, dite_eq_right hy, ← zpow_add' (Or.inl he),
← toAdd_mul]
congr
rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]
← log_mul hx hy]

theorem toNNReal_pos_apply {e : ℝ≥0} (he : e ≠ 0) {x : ℤᵐ⁰} (hx : x = 0) :
toNNReal he x = 0 := by
simp [toNNReal, hx]

set_option backward.isDefEq.respectTransparency false in
theorem toNNReal_neg_apply {e : ℝ≥0} (he : e ≠ 0) {x : ℤᵐ⁰} (hx : x ≠ 0) :
toNNReal he x = e ^ (WithZero.unzero hx).toAdd := by
toNNReal he x = e ^ log x := by
simp [toNNReal, hx]

/-- `toNNReal` sends nonzero elements to nonzero elements. -/
Expand All @@ -92,7 +90,8 @@ theorem toNNReal_eq_one_iff {e : ℝ≥0} (m : ℤᵐ⁰) (he0 : e ≠ 0) (he1 :
by_cases hm : m = 0
· simp only [hm, map_zero, zero_ne_one]
· refine ⟨fun h1 ↦ ?_, fun h1 ↦ h1 ▸ map_one _⟩
rw [toNNReal_neg_apply he0 hm, zpow_eq_one_iff_right₀ _root_.zero_le he1, toAdd_eq_zero] at h1
rw [toNNReal_neg_apply he0 hm, zpow_eq_one_iff_right₀ _root_.zero_le he1,
← toAdd_unzero_eq_log hm, toAdd_eq_zero] at h1
rw [← WithZero.coe_unzero hm, h1, coe_one]

theorem toNNReal_lt_one_iff {e : ℝ≥0} {m : ℤᵐ⁰} (he : 1 < e) :
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -311,8 +311,8 @@ lemma FinitePlace.two_le_norm_of_one_lt_norm (x : v.adicCompletion K) (h : 1 <
apply (two_le_absNorm_nnreal v).trans
conv_lhs => rw [← zpow_one (v.asIdeal.absNorm : NNReal)]
apply zpow_le_zpow_right₀ (one_lt_absNorm_nnreal v).le
simpa [← Int.sub_one_lt_iff, sub_self, ← toAdd_one, Multiplicative.toAdd_lt,
WithZero.lt_unzero_iff] using Valued.toNormedField.one_lt_norm_iff.1 h
simpa [← Int.sub_one_lt_iff, ← log_one] using
lt_log_of_exp_lt (Valued.toNormedField.one_lt_norm_iff.1 h)

set_option backward.isDefEq.respectTransparency false in
lemma HeightOneSpectrum.embedding_mul_absNorm {x : R} (h_x_nezero : x ≠ 0) :
Expand Down
Loading