From 7e7aaccf9b0182576cabdde36cf1b5ad3585b70d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 12 Jan 2023 20:46:50 +0000 Subject: [PATCH] chore(*): remove some defeq abuse of `^` (#18136) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit There are various places where the proofs relied on the defeq of `^`, namely that * `rfl : x ^ 0 = 1` * `rfl : x ^ (n : ℕ) = x ^ (↑n : ℤ)` * `rfl : x ^ (n.succ : ℕ) = x * x ^ n` While exploiting defeq is not always a bad thing, in some of these cases it was clear that this wasn't intentional, and the author had not noticed that they were working with integer instead of natural powers. This change is motivated by two possible refactors: * Changing the definition of `monoid.npow_rec` to match `function.iterate` * Changing the definition of `real.has_pow` to be the elementwise power on the cauchy sequence (#8146) --- src/analysis/special_functions/bernstein.lean | 3 ++- src/analysis/special_functions/integrals.lean | 2 +- src/analysis/special_functions/pow.lean | 8 ++++---- src/analysis/special_functions/stirling.lean | 4 +++- src/data/real/cardinality.lean | 10 +++++++--- src/data/real/irrational.lean | 2 +- src/number_theory/padics/padic_integers.lean | 2 +- src/topology/metric_space/lipschitz.lean | 4 ++-- src/topology/metric_space/pi_nat.lean | 1 + 9 files changed, 22 insertions(+), 14 deletions(-) diff --git a/src/analysis/special_functions/bernstein.lean b/src/analysis/special_functions/bernstein.lean index e84fbc01ca3d0..67df5d5c9e191 100644 --- a/src/analysis/special_functions/bernstein.lean +++ b/src/analysis/special_functions/bernstein.lean @@ -192,7 +192,8 @@ lemma le_of_mem_S_compl (1 : ℝ) ≤ (δ f ε h)^(-2 : ℤ) * (x - k/ₙ) ^ 2 := begin simp only [finset.mem_compl, not_lt, set.mem_to_finset, set.mem_set_of_eq, S] at m, - erw [zpow_neg, ← div_eq_inv_mul, one_le_div (pow_pos δ_pos 2), sq_le_sq, abs_of_pos δ_pos], + rw [zpow_neg, ← div_eq_inv_mul, zpow_two, ←pow_two, one_le_div (pow_pos δ_pos 2), sq_le_sq, + abs_of_pos δ_pos], rwa [dist_comm] at m end diff --git a/src/analysis/special_functions/integrals.lean b/src/analysis/special_functions/integrals.lean index 444560c44e200..efd34ff0461cc 100644 --- a/src/analysis/special_functions/integrals.lean +++ b/src/analysis/special_functions/integrals.lean @@ -265,7 +265,7 @@ begin end @[simp] lemma integral_pow : ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) := -by simpa using integral_zpow (or.inl (int.coe_nat_nonneg n)) +by simpa only [←int.coe_nat_succ, zpow_coe_nat] using integral_zpow (or.inl (int.coe_nat_nonneg n)) /-- Integral of `|x - a| ^ n` over `Ι a b`. This integral appears in the proof of the Picard-Lindelöf/Cauchy-Lipschitz theorem. -/ diff --git a/src/analysis/special_functions/pow.lean b/src/analysis/special_functions/pow.lean index 4f46b791aee68..4fd66dc7d3314 100644 --- a/src/analysis/special_functions/pow.lean +++ b/src/analysis/special_functions/pow.lean @@ -570,13 +570,13 @@ by rw [rpow_def, complex.of_real_add, complex.cpow_add _ _ (complex.of_real_ne_z complex.of_real_mul_re, ← rpow_def, mul_comm] lemma rpow_add_nat {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y + n) = x ^ y * x ^ n := -rpow_add_int hx y n +by simpa using rpow_add_int hx y n lemma rpow_sub_int {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y - n) = x ^ y / x ^ n := by simpa using rpow_add_int hx y (-n) lemma rpow_sub_nat {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - n) = x ^ y / x ^ n := -rpow_sub_int hx y n +by simpa using rpow_sub_int hx y n lemma rpow_add_one {x : ℝ} (hx : x ≠ 0) (y : ℝ) : x ^ (y + 1) = x ^ y * x := by simpa using rpow_add_nat hx y 1 @@ -589,7 +589,7 @@ by simp only [rpow_def, ← complex.of_real_zpow, complex.cpow_int_cast, complex.of_real_int_cast, complex.of_real_re] @[simp, norm_cast] lemma rpow_nat_cast (x : ℝ) (n : ℕ) : x ^ (n : ℝ) = x ^ n := -rpow_int_cast x n +by simpa using rpow_int_cast x n @[simp] lemma rpow_two (x : ℝ) : x ^ (2 : ℝ) = x ^ 2 := by { rw ← rpow_nat_cast, simp only [nat.cast_bit0, nat.cast_one] } @@ -1121,7 +1121,7 @@ by simpa only [rpow_int_cast] using is_o_rpow_exp_pos_mul_at_top k hb /-- `x ^ k = o(exp(b * x))` as `x → ∞` for any natural `k` and positive `b`. -/ lemma is_o_pow_exp_pos_mul_at_top (k : ℕ) {b : ℝ} (hb : 0 < b) : (λ x : ℝ, x ^ k) =o[at_top] (λ x, exp (b * x)) := -is_o_zpow_exp_pos_mul_at_top k hb +by simpa using is_o_zpow_exp_pos_mul_at_top k hb /-- `x ^ s = o(exp x)` as `x → ∞` for any real `s`. -/ lemma is_o_rpow_exp_at_top (s : ℝ) : (λ x : ℝ, x ^ s) =o[at_top] exp := diff --git a/src/analysis/special_functions/stirling.lean b/src/analysis/special_functions/stirling.lean index ae5e25a3b556b..01a297e311410 100644 --- a/src/analysis/special_functions/stirling.lean +++ b/src/analysis/special_functions/stirling.lean @@ -104,7 +104,9 @@ begin have h_nonneg : 0 ≤ ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) := sq_nonneg _, have g : has_sum (λ k : ℕ, ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) ^ k.succ) ((1 / (2 * n.succ + 1)) ^ 2 / (1 - (1 / (2 * n.succ + 1)) ^ 2)), - { refine (has_sum_geometric_of_lt_1 h_nonneg _).mul_left ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2), + { have := (has_sum_geometric_of_lt_1 h_nonneg _).mul_left ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2), + { simp_rw ←pow_succ at this, + exact this, }, rw [one_div, inv_pow], exact inv_lt_one (one_lt_pow ((lt_add_iff_pos_left 1).mpr $ by positivity) two_ne_zero) }, have hab : ∀ (k : ℕ), (1 / (2 * (k.succ : ℝ) + 1)) * ((1 / (2 * n.succ + 1)) ^ 2) ^ k.succ ≤ diff --git a/src/data/real/cardinality.lean b/src/data/real/cardinality.lean index 58db59e8ab65a..74c5933f30a7f 100644 --- a/src/data/real/cardinality.lean +++ b/src/data/real/cardinality.lean @@ -66,6 +66,10 @@ lemma cantor_function_aux_eq (h : f n = g n) : cantor_function_aux c f n = cantor_function_aux c g n := by simp [cantor_function_aux, h] +lemma cantor_function_aux_zero (f : ℕ → bool) : + cantor_function_aux c f 0 = cond (f 0) 1 0 := +by { cases h : f 0; simp [h] } + lemma cantor_function_aux_succ (f : ℕ → bool) : (λ n, cantor_function_aux c f (n + 1)) = λ n, c * cantor_function_aux c (λ n, f (n + 1)) n := by { ext n, cases h : f (n + 1); simp [h, pow_succ] } @@ -122,9 +126,9 @@ begin { rw [cantor_function_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ←tsum_geometric_of_lt_1 (le_of_lt h1) h3], apply zero_add }, - { convert tsum_eq_single 0 _, - { apply_instance }, - { intros n hn, cases n, contradiction, refl } } }, + { refine (tsum_eq_single 0 _).trans _, + { intros n hn, cases n, contradiction, refl }, + { exact cantor_function_aux_zero _ }, } }, rw [cantor_function_succ f (le_of_lt h1) h3, cantor_function_succ g (le_of_lt h1) h3], rw [hn 0 $ zero_lt_succ n], apply add_lt_add_left, rw mul_lt_mul_left h1, exact ih (λ k hk, hn _ $ nat.succ_lt_succ hk) fn gn diff --git a/src/data/real/irrational.lean b/src/data/real/irrational.lean index 6c67f6fbc36ef..c2463026fe019 100644 --- a/src/data/real/irrational.lean +++ b/src/data/real/irrational.lean @@ -351,7 +351,7 @@ theorem of_pow : ∀ n : ℕ, irrational (x^n) → irrational x | (n+1) := λ h, by { rw pow_succ at h, exact h.mul_cases.elim id (of_pow n) } theorem of_zpow : ∀ m : ℤ, irrational (x^m) → irrational x -| (n:ℕ) := of_pow n +| (n:ℕ) := λ h, by { rw zpow_coe_nat at h, exact h.of_pow _ } | -[1+n] := λ h, by { rw zpow_neg_succ_of_nat at h, exact h.of_inv.of_pow _ } end irrational diff --git a/src/number_theory/padics/padic_integers.lean b/src/number_theory/padics/padic_integers.lean index 5b025a364f284..b70cfcbe73956 100644 --- a/src/number_theory/padics/padic_integers.lean +++ b/src/number_theory/padics/padic_integers.lean @@ -314,7 +314,7 @@ begin { simp [hx] }, have h : (1 : ℝ) < p := by exact_mod_cast hp.1.one_lt, rw [← neg_nonpos, ← (zpow_strict_mono h).le_iff_le], - show (p : ℝ) ^ -valuation x ≤ p ^ 0, + show (p : ℝ) ^ -valuation x ≤ p ^ (0 : ℤ), rw [← norm_eq_pow_val hx], simpa using x.property end diff --git a/src/topology/metric_space/lipschitz.lean b/src/topology/metric_space/lipschitz.lean index 724a89cbada33..4f33443074d1e 100644 --- a/src/topology/metric_space/lipschitz.lean +++ b/src/topology/metric_space/lipschitz.lean @@ -240,7 +240,7 @@ end protected lemma iterate {f : α → α} (hf : lipschitz_with K f) : ∀n, lipschitz_with (K ^ n) (f^[n]) -| 0 := lipschitz_with.id +| 0 := by simpa only [pow_zero] using lipschitz_with.id | (n + 1) := by rw [pow_succ']; exact (iterate n).comp hf lemma edist_iterate_succ_le_geometric {f : α → α} (hf : lipschitz_with K f) (x n) : @@ -265,7 +265,7 @@ protected lemma list_prod (f : ι → function.End α) (K : ι → ℝ≥0) protected lemma pow {f : function.End α} {K} (h : lipschitz_with K f) : ∀ n : ℕ, lipschitz_with (K^n) (f^n : function.End α) -| 0 := lipschitz_with.id +| 0 := by simpa only [pow_zero] using lipschitz_with.id | (n + 1) := by { rw [pow_succ, pow_succ], exact h.mul (pow n) } end emetric diff --git a/src/topology/metric_space/pi_nat.lean b/src/topology/metric_space/pi_nat.lean index 0a7287c0e7b4f..ba35f8bb48a1a 100644 --- a/src/topology/metric_space/pi_nat.lean +++ b/src/topology/metric_space/pi_nat.lean @@ -709,6 +709,7 @@ begin apply apply_first_diff_ne hne', rw [le_zero_iff.1 h], apply apply_eq_of_dist_lt _ le_rfl, + rw pow_zero, exact hxy }, have hn : first_diff x.1 y.1 = n + 1 := (nat.succ_pred_eq_of_pos diff_pos).symm, rw [dist', dist_eq_of_ne hne', hn],