diff --git a/Mathbin/Algebra/GroupPower/Ring.lean b/Mathbin/Algebra/GroupPower/Ring.lean index 95c8f346fe..2593f78fbb 100644 --- a/Mathbin/Algebra/GroupPower/Ring.lean +++ b/Mathbin/Algebra/GroupPower/Ring.lean @@ -37,12 +37,14 @@ theorem zero_pow : ∀ {n : ℕ}, 0 < n → (0 : M) ^ n = 0 #align zero_pow zero_pow -/ -#print zero_pow' /- +/- warning: zero_pow' clashes with zero_pow -> zero_pow +Case conversion may be inaccurate. Consider using '#align zero_pow' zero_powₓ'. -/ +#print zero_pow /- @[simp] -theorem zero_pow' : ∀ n : ℕ, n ≠ 0 → (0 : M) ^ n = 0 +theorem zero_pow : ∀ n : ℕ, n ≠ 0 → (0 : M) ^ n = 0 | 0, h => absurd rfl h | k + 1, h => by rw [pow_succ]; exact MulZeroClass.zero_mul _ -#align zero_pow' zero_pow' +#align zero_pow' zero_pow -/ #print zero_pow_eq /- @@ -95,7 +97,7 @@ theorem pow_ne_zero_iff [NoZeroDivisors M] {a : M} {n : ℕ} (hn : 0 < n) : a ^ #print ne_zero_pow /- theorem ne_zero_pow {a : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≠ 0 → a ≠ 0 := by contrapose!; rintro rfl; - exact zero_pow' n hn + exact zero_pow n hn #align ne_zero_pow ne_zero_pow -/ @@ -124,7 +126,7 @@ theorem zero_pow_eq_zero [Nontrivial M] {n : ℕ} : (0 : M) ^ n = 0 ↔ 0 < n := by constructor <;> intro h · rw [pos_iff_ne_zero]; rintro rfl; simpa using h - · exact zero_pow' n h.ne.symm + · exact zero_pow n h.ne.symm #align zero_pow_eq_zero zero_pow_eq_zero -/ diff --git a/Mathbin/Algebra/GroupWithZero/Power.lean b/Mathbin/Algebra/GroupWithZero/Power.lean index d823629d97..e5de665ef6 100644 --- a/Mathbin/Algebra/GroupWithZero/Power.lean +++ b/Mathbin/Algebra/GroupWithZero/Power.lean @@ -75,7 +75,7 @@ attribute [local ematch] le_of_lt #print zero_zpow /- theorem zero_zpow : ∀ z : ℤ, z ≠ 0 → (0 : G₀) ^ z = 0 - | (n : ℕ), h => by rw [zpow_ofNat, zero_pow']; simpa using h + | (n : ℕ), h => by rw [zpow_ofNat, zero_pow]; simpa using h | -[n+1], h => by simp #align zero_zpow zero_zpow -/ diff --git a/Mathbin/Analysis/Analytic/Basic.lean b/Mathbin/Analysis/Analytic/Basic.lean index f3539c84f9..e8a6496177 100644 --- a/Mathbin/Analysis/Analytic/Basic.lean +++ b/Mathbin/Analysis/Analytic/Basic.lean @@ -326,7 +326,7 @@ theorem summable_norm_mul_pow (p : FormalMultilinearSeries 𝕜 E F) {r : ℝ≥ obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, hC : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius h exact Summable.of_nonneg_of_le (fun n => mul_nonneg (norm_nonneg _) (pow_nonneg r.coe_nonneg _)) hp - ((summable_geometric_of_lt_1 ha.1.le ha.2).hMul_left _) + ((summable_geometric_of_lt_one ha.1.le ha.2).hMul_left _) #align formal_multilinear_series.summable_norm_mul_pow FormalMultilinearSeries.summable_norm_mul_pow -/ @@ -374,7 +374,7 @@ theorem radius_eq_top_iff_summable_norm (p : FormalMultilinearSeries 𝕜 E F) : (show (r : ℝ≥0∞) < p.radius from h.symm ▸ ENNReal.coe_lt_top) refine' Summable.of_norm_bounded (fun n => (C : ℝ) * a ^ n) - ((summable_geometric_of_lt_1 ha.1.le ha.2).hMul_left _) fun n => _ + ((summable_geometric_of_lt_one ha.1.le ha.2).hMul_left _) fun n => _ specialize hp n rwa [Real.norm_of_nonneg (mul_nonneg (norm_nonneg _) (pow_nonneg r.coe_nonneg n))] · exact p.radius_eq_top_of_summable_norm @@ -924,8 +924,8 @@ theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal simp only [add_mul] have : ‖a‖ < 1 := by simp only [Real.norm_eq_abs, abs_of_pos ha.1, ha.2] convert - (hasSum_coe_mul_geometric_of_norm_lt_1 this).add - ((hasSum_geometric_of_norm_lt_1 this).hMul_left 2) + (hasSum_coe_mul_geometric_of_norm_lt_one this).add + ((hasSum_geometric_of_norm_lt_one this).hMul_left 2) exact hA.norm_le_of_bounded hBL hAB suffices L =O[𝓟 (EMetric.ball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ by @@ -984,7 +984,7 @@ theorem HasFPowerSeriesOnBall.tendstoUniformlyOn {r' : ℝ≥0} (hf : HasFPowerS exact hf.uniform_geometric_approx h refine' Metric.tendstoUniformlyOn_iff.2 fun ε εpos => _ have L : tendsto (fun n => (C : ℝ) * a ^ n) at_top (𝓝 ((C : ℝ) * 0)) := - tendsto_const_nhds.mul (tendsto_pow_atTop_nhds_0_of_lt_1 ha.1.le ha.2) + tendsto_const_nhds.mul (tendsto_pow_atTop_nhds_zero_of_lt_one ha.1.le ha.2) rw [MulZeroClass.mul_zero] at L refine' (L.eventually (gt_mem_nhds εpos)).mono fun n hn y hy => _ rw [dist_eq_norm] @@ -1130,7 +1130,7 @@ theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero {n : ℕ} {p : exact norm_eq_zero.mp (by - simpa only [fin0_apply_norm, norm_eq_zero, norm_zero, zero_pow', Ne.def, Nat.one_ne_zero, + simpa only [fin0_apply_norm, norm_eq_zero, norm_zero, zero_pow, Ne.def, Nat.one_ne_zero, not_false_iff, MulZeroClass.mul_zero, norm_le_zero_iff] using ht 0 (δε (Metric.mem_ball_self δ_pos))) · refine' Or.elim (em (y = 0)) (fun hy => by simpa only [hy] using p.map_zero) fun hy => _ diff --git a/Mathbin/Analysis/Asymptotics/Asymptotics.lean b/Mathbin/Analysis/Asymptotics/Asymptotics.lean index f66f8ee331..1525e26f4b 100644 --- a/Mathbin/Analysis/Asymptotics/Asymptotics.lean +++ b/Mathbin/Analysis/Asymptotics/Asymptotics.lean @@ -2611,8 +2611,8 @@ theorem isLittleO_pow_sub_sub (x₀ : E') {m : ℕ} (h : 1 < m) : #align asymptotics.is_o_pow_sub_sub Asymptotics.isLittleO_pow_sub_sub -/ -#print Asymptotics.IsBigOWith.right_le_sub_of_lt_1 /- -theorem IsBigOWith.right_le_sub_of_lt_1 {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) : +#print Asymptotics.IsBigOWith.right_le_sub_of_lt_one /- +theorem IsBigOWith.right_le_sub_of_lt_one {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) : IsBigOWith (1 / (1 - c)) l f₂ fun x => f₂ x - f₁ x := IsBigOWith.of_bound <| mem_of_superset h.bound fun x hx => @@ -2621,28 +2621,28 @@ theorem IsBigOWith.right_le_sub_of_lt_1 {f₁ f₂ : α → E'} (h : IsBigOWith rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff, mul_sub, mul_one, mul_comm] · exact le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _) · exact sub_pos.2 hc -#align asymptotics.is_O_with.right_le_sub_of_lt_1 Asymptotics.IsBigOWith.right_le_sub_of_lt_1 +#align asymptotics.is_O_with.right_le_sub_of_lt_1 Asymptotics.IsBigOWith.right_le_sub_of_lt_one -/ -#print Asymptotics.IsBigOWith.right_le_add_of_lt_1 /- -theorem IsBigOWith.right_le_add_of_lt_1 {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) : +#print Asymptotics.IsBigOWith.right_le_add_of_lt_one /- +theorem IsBigOWith.right_le_add_of_lt_one {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) : IsBigOWith (1 / (1 - c)) l f₂ fun x => f₁ x + f₂ x := - (h.neg_right.right_le_sub_of_lt_1 hc).neg_right.of_neg_left.congr rfl (fun x => rfl) fun x => by + (h.neg_right.right_le_sub_of_lt_one hc).neg_right.of_neg_left.congr rfl (fun x => rfl) fun x => by rw [neg_sub, sub_neg_eq_add] -#align asymptotics.is_O_with.right_le_add_of_lt_1 Asymptotics.IsBigOWith.right_le_add_of_lt_1 +#align asymptotics.is_O_with.right_le_add_of_lt_1 Asymptotics.IsBigOWith.right_le_add_of_lt_one -/ #print Asymptotics.IsLittleO.right_isBigO_sub /- theorem IsLittleO.right_isBigO_sub {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] fun x => f₂ x - f₁ x := - ((h.def' one_half_pos).right_le_sub_of_lt_1 one_half_lt_one).IsBigO + ((h.def' one_half_pos).right_le_sub_of_lt_one one_half_lt_one).IsBigO #align asymptotics.is_o.right_is_O_sub Asymptotics.IsLittleO.right_isBigO_sub -/ #print Asymptotics.IsLittleO.right_isBigO_add /- theorem IsLittleO.right_isBigO_add {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] fun x => f₁ x + f₂ x := - ((h.def' one_half_pos).right_le_add_of_lt_1 one_half_lt_one).IsBigO + ((h.def' one_half_pos).right_le_add_of_lt_one one_half_lt_one).IsBigO #align asymptotics.is_o.right_is_O_add Asymptotics.IsLittleO.right_isBigO_add -/ diff --git a/Mathbin/Analysis/Calculus/FderivSymmetric.lean b/Mathbin/Analysis/Calculus/FderivSymmetric.lean index 18f64be970..e8af8b9d62 100644 --- a/Mathbin/Analysis/Calculus/FderivSymmetric.lean +++ b/Mathbin/Analysis/Calculus/FderivSymmetric.lean @@ -185,7 +185,7 @@ theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s) · congr 1 dsimp only [g] simp only [Nat.one_ne_zero, add_zero, one_mul, zero_div, MulZeroClass.zero_mul, sub_zero, - zero_smul, Ne.def, not_false_iff, bit0_eq_zero, zero_pow'] + zero_smul, Ne.def, not_false_iff, bit0_eq_zero, zero_pow] abel · simp only [Real.norm_eq_abs, abs_mul, add_nonneg (norm_nonneg v) (norm_nonneg w), abs_of_nonneg, diff --git a/Mathbin/Analysis/Calculus/Inverse.lean b/Mathbin/Analysis/Calculus/Inverse.lean index 9fdfb1630c..d017080ee4 100644 --- a/Mathbin/Analysis/Calculus/Inverse.lean +++ b/Mathbin/Analysis/Calculus/Inverse.lean @@ -367,8 +367,8 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f rw [tendsto_iff_dist_tendsto_zero] refine' squeeze_zero (fun n => dist_nonneg) (fun n => (D n).1) _ simpa using - (tendsto_pow_atTop_nhds_0_of_lt_1 (mul_nonneg (NNReal.coe_nonneg _) (NNReal.coe_nonneg _)) - Icf').mul + (tendsto_pow_atTop_nhds_zero_of_lt_one + (mul_nonneg (NNReal.coe_nonneg _) (NNReal.coe_nonneg _)) Icf').mul tendsto_const_nhds exact tendsto_nhds_unique T1 T2 #align approximates_linear_on.surj_on_closed_ball_of_nonlinear_right_inverse ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse diff --git a/Mathbin/Analysis/Calculus/TangentCone.lean b/Mathbin/Analysis/Calculus/TangentCone.lean index b99f341545..2367045a0b 100644 --- a/Mathbin/Analysis/Calculus/TangentCone.lean +++ b/Mathbin/Analysis/Calculus/TangentCone.lean @@ -191,7 +191,7 @@ theorem subset_tangentCone_prod_left {t : Set F} {y : F} (ht : y ∈ closure t) simp [hn, (hd' n).1] · apply tendsto.prod_mk_nhds hy _ refine' squeeze_zero_norm (fun n => (hd' n).2.le) _ - exact tendsto_pow_atTop_nhds_0_of_lt_1 one_half_pos.le one_half_lt_one + exact tendsto_pow_atTop_nhds_zero_of_lt_one one_half_pos.le one_half_lt_one #align subset_tangent_cone_prod_left subset_tangentCone_prod_left -/ @@ -217,7 +217,7 @@ theorem subset_tangentCone_prod_right {t : Set F} {y : F} (hs : x ∈ closure s) simp [hn, (hd' n).1] · apply tendsto.prod_mk_nhds _ hy refine' squeeze_zero_norm (fun n => (hd' n).2.le) _ - exact tendsto_pow_atTop_nhds_0_of_lt_1 one_half_pos.le one_half_lt_one + exact tendsto_pow_atTop_nhds_zero_of_lt_one one_half_pos.le one_half_lt_one #align subset_tangent_cone_prod_right subset_tangentCone_prod_right -/ @@ -248,7 +248,7 @@ theorem mapsTo_tangentCone_pi {ι : Type _} [DecidableEq ι] {E : ι → Type _} · simp [hy] · suffices tendsto (fun n => c n • d' n j) at_top (𝓝 0) by simpa [hj] refine' squeeze_zero_norm (fun n => (hcd' n j hj).le) _ - exact tendsto_pow_atTop_nhds_0_of_lt_1 one_half_pos.le one_half_lt_one + exact tendsto_pow_atTop_nhds_zero_of_lt_one one_half_pos.le one_half_lt_one #align maps_to_tangent_cone_pi mapsTo_tangentCone_pi -/ diff --git a/Mathbin/Analysis/Calculus/Taylor.lean b/Mathbin/Analysis/Calculus/Taylor.lean index 293dfc3ba8..36350f1a80 100644 --- a/Mathbin/Analysis/Calculus/Taylor.lean +++ b/Mathbin/Analysis/Calculus/Taylor.lean @@ -341,7 +341,7 @@ theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ rcases taylor_mean_remainder hx hf hf' gcont (fun y _ => monomial_has_deriv_aux y x _) hg' with ⟨y, hy, h⟩ use y, hy - simp only [sub_self, zero_pow', Ne.def, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h + simp only [sub_self, zero_pow, Ne.def, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h rw [h, neg_div, ← div_neg, neg_mul, neg_neg] field_simp [n.cast_add_one_ne_zero, n.factorial_ne_zero, xy_ne y hy] ring diff --git a/Mathbin/Analysis/InnerProductSpace/Projection.lean b/Mathbin/Analysis/InnerProductSpace/Projection.lean index 9e36787311..71adc798a3 100644 --- a/Mathbin/Analysis/InnerProductSpace/Projection.lean +++ b/Mathbin/Analysis/InnerProductSpace/Projection.lean @@ -97,7 +97,7 @@ theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h by have h : tendsto (fun n : ℕ => δ) at_top (nhds δ) := tendsto_const_nhds have h' : tendsto (fun n : ℕ => δ + 1 / (n + 1)) at_top (nhds δ) := by - convert h.add tendsto_one_div_add_atTop_nhds_0_nat; simp only [add_zero] + convert h.add tendsto_one_div_add_atTop_nhds_zero_nat; simp only [add_zero] exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h' (fun x => δ_le _) fun x => le_of_lt (hw _) -- Step 2: Prove that the sequence `w : ℕ → K` is a Cauchy sequence have seq_is_cauchy : CauchySeq fun n => (w n : F) := @@ -175,16 +175,16 @@ theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h · convert continuous_sqrt.continuous_at; exact sqrt_zero.symm have eq₁ : tendsto (fun n : ℕ => 8 * δ * (1 / (n + 1))) at_top (nhds (0 : ℝ)) := by - convert (@tendsto_const_nhds _ _ _ (8 * δ) _).mul tendsto_one_div_add_atTop_nhds_0_nat + convert (@tendsto_const_nhds _ _ _ (8 * δ) _).mul tendsto_one_div_add_atTop_nhds_zero_nat simp only [MulZeroClass.mul_zero] have : tendsto (fun n : ℕ => (4 : ℝ) * (1 / (n + 1))) at_top (nhds (0 : ℝ)) := by - convert (@tendsto_const_nhds _ _ _ (4 : ℝ) _).mul tendsto_one_div_add_atTop_nhds_0_nat + convert (@tendsto_const_nhds _ _ _ (4 : ℝ) _).mul tendsto_one_div_add_atTop_nhds_zero_nat simp only [MulZeroClass.mul_zero] have eq₂ : tendsto (fun n : ℕ => (4 : ℝ) * (1 / (n + 1)) * (1 / (n + 1))) at_top (nhds (0 : ℝ)) := by - convert this.mul tendsto_one_div_add_atTop_nhds_0_nat + convert this.mul tendsto_one_div_add_atTop_nhds_zero_nat simp only [MulZeroClass.mul_zero] convert eq₁.add eq₂; simp only [add_zero] -- Step 3: By completeness of `K`, let `w : ℕ → K` converge to some `v : K`. diff --git a/Mathbin/Analysis/MeanInequalitiesPow.lean b/Mathbin/Analysis/MeanInequalitiesPow.lean index d266158d62..cd46c3b180 100644 --- a/Mathbin/Analysis/MeanInequalitiesPow.lean +++ b/Mathbin/Analysis/MeanInequalitiesPow.lean @@ -80,7 +80,7 @@ theorem pow_sum_div_card_le_sum_pow {f : ι → ℝ} (n : ℕ) (hf : ∀ a ∈ s (∑ x in s, f x) ^ (n + 1) / s.card ^ n ≤ ∑ x in s, f x ^ (n + 1) := by rcases s.eq_empty_or_nonempty with (rfl | hs) - · simp_rw [Finset.sum_empty, zero_pow' _ (Nat.succ_ne_zero n), zero_div] + · simp_rw [Finset.sum_empty, zero_pow _ (Nat.succ_ne_zero n), zero_div] · have hs0 : 0 < (s.card : ℝ) := Nat.cast_pos.2 hs.card_pos suffices (∑ x in s, f x / s.card) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / s.card by rwa [← Finset.sum_div, ← Finset.sum_div, div_pow, pow_succ' (s.card : ℝ), ← div_div, diff --git a/Mathbin/Analysis/NormedSpace/Banach.lean b/Mathbin/Analysis/NormedSpace/Banach.lean index dd7a9a0fa4..b883260835 100644 --- a/Mathbin/Analysis/NormedSpace/Banach.lean +++ b/Mathbin/Analysis/NormedSpace/Banach.lean @@ -212,7 +212,7 @@ theorem exists_preimage_norm_le (surj : Surjective f) : have sNu : Summable fun n => ‖u n‖ := by refine' Summable.of_nonneg_of_le (fun n => norm_nonneg _) ule _ - exact Summable.mul_right _ (summable_geometric_of_lt_1 (by norm_num) (by norm_num)) + exact Summable.mul_right _ (summable_geometric_of_lt_one (by norm_num) (by norm_num)) have su : Summable u := Summable.of_norm sNu let x := tsum u have x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖ := @@ -241,7 +241,7 @@ theorem exists_preimage_norm_le (surj : Surjective f) : simp only [sub_zero] refine' squeeze_zero (fun _ => norm_nonneg _) hnle _ rw [← MulZeroClass.zero_mul ‖y‖] - refine' (tendsto_pow_atTop_nhds_0_of_lt_1 _ _).mul tendsto_const_nhds <;> norm_num + refine' (tendsto_pow_atTop_nhds_zero_of_lt_one _ _).mul tendsto_const_nhds <;> norm_num have feq : f x = y - 0 := tendsto_nhds_unique L₁ L₂ rw [sub_zero] at feq exact ⟨x, feq, x_ineq⟩ diff --git a/Mathbin/Analysis/NormedSpace/Spectrum.lean b/Mathbin/Analysis/NormedSpace/Spectrum.lean index 3c47ec9db1..4049c99ccb 100644 --- a/Mathbin/Analysis/NormedSpace/Spectrum.lean +++ b/Mathbin/Analysis/NormedSpace/Spectrum.lean @@ -353,7 +353,7 @@ theorem hasFPowerSeriesOnBall_inverse_one_sub_smul [CompleteSpace A] (a : A) : simpa only [← coe_inv h, mem_ball_zero_iff, Metric.emetric_ball_nnreal] using hy rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul, ← NNReal.lt_inv_iff_mul_lt h] - simpa [← smul_pow, (NormedRing.summable_geometric_of_norm_lt_1 _ norm_lt).hasSum_iff] using + simpa [← smul_pow, (NormedRing.summable_geometric_of_norm_lt_one _ norm_lt).hasSum_iff] using (NormedRing.inverse_one_sub _ norm_lt).symm } #align spectrum.has_fpower_series_on_ball_inverse_one_sub_smul spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul -/ diff --git a/Mathbin/Analysis/NormedSpace/Units.lean b/Mathbin/Analysis/NormedSpace/Units.lean index 86e903ee3c..58ec2a2ab9 100644 --- a/Mathbin/Analysis/NormedSpace/Units.lean +++ b/Mathbin/Analysis/NormedSpace/Units.lean @@ -224,7 +224,7 @@ theorem inverse_one_sub_norm : (fun t : R => inverse (1 - t)) =O[𝓝 0] (fun t linarith simp only [inverse_one_sub t ht', norm_one, mul_one, Set.mem_setOf_eq] change ‖∑' n : ℕ, t ^ n‖ ≤ _ - have := NormedRing.tsum_geometric_of_norm_lt_1 t ht' + have := NormedRing.tsum_geometric_of_norm_lt_one t ht' have : (1 - ‖t‖)⁻¹ ≤ 2 := by rw [← inv_inv (2 : ℝ)] refine' inv_le_inv_of_le (by norm_num) _ diff --git a/Mathbin/Analysis/PSeries.lean b/Mathbin/Analysis/PSeries.lean index 1bc9b33211..0789a681a7 100644 --- a/Mathbin/Analysis/PSeries.lean +++ b/Mathbin/Analysis/PSeries.lean @@ -193,7 +193,7 @@ theorem Real.summable_nat_rpow_inv {p : ℝ} : Summable (fun n => (n ^ p)⁻¹ : · rw [← summable_condensed_iff_of_nonneg] · simp_rw [Nat.cast_pow, Nat.cast_two, ← rpow_nat_cast, ← rpow_mul zero_lt_two.le, mul_comm _ p, rpow_mul zero_lt_two.le, rpow_nat_cast, ← inv_pow, ← mul_pow, - summable_geometric_iff_norm_lt_1] + summable_geometric_iff_norm_lt_one] nth_rw 1 [← rpow_one 2] rw [← division_def, ← rpow_sub zero_lt_two, norm_eq_abs, abs_of_pos (rpow_pos_of_pos zero_lt_two _), rpow_lt_one_iff zero_lt_two.le] diff --git a/Mathbin/Analysis/SpecialFunctions/Bernstein.lean b/Mathbin/Analysis/SpecialFunctions/Bernstein.lean index 86a9335478..63ec47c6c2 100644 --- a/Mathbin/Analysis/SpecialFunctions/Bernstein.lean +++ b/Mathbin/Analysis/SpecialFunctions/Bernstein.lean @@ -257,7 +257,7 @@ theorem bernsteinApproximation_uniform (f : C(I, ℝ)) : simp only [metric.nhds_basis_ball.tendsto_right_iff, Metric.mem_ball, dist_eq_norm] intro ε h let δ := δ f ε h - have nhds_zero := tendsto_const_div_atTop_nhds_0_nat (2 * ‖f‖ * δ ^ (-2 : ℤ)) + have nhds_zero := tendsto_const_div_atTop_nhds_zero_nat (2 * ‖f‖ * δ ^ (-2 : ℤ)) filter_upwards [nhds_zero.eventually (gt_mem_nhds (half_pos h)), eventually_gt_at_top 0] with n nh npos' have npos : 0 < (n : ℝ) := by exact_mod_cast npos' diff --git a/Mathbin/Analysis/SpecialFunctions/Exp.lean b/Mathbin/Analysis/SpecialFunctions/Exp.lean index 8d9630b168..6a68da73b4 100644 --- a/Mathbin/Analysis/SpecialFunctions/Exp.lean +++ b/Mathbin/Analysis/SpecialFunctions/Exp.lean @@ -219,24 +219,24 @@ theorem tendsto_exp_atTop : Tendsto exp atTop atTop := #align real.tendsto_exp_at_top Real.tendsto_exp_atTop -/ -#print Real.tendsto_exp_neg_atTop_nhds_0 /- +#print Real.tendsto_exp_neg_atTop_nhds_zero /- /-- The real exponential function tends to `0` at `-∞` or, equivalently, `exp(-x)` tends to `0` at `+∞` -/ -theorem tendsto_exp_neg_atTop_nhds_0 : Tendsto (fun x => exp (-x)) atTop (𝓝 0) := +theorem tendsto_exp_neg_atTop_nhds_zero : Tendsto (fun x => exp (-x)) atTop (𝓝 0) := (tendsto_inv_atTop_zero.comp tendsto_exp_atTop).congr fun x => (exp_neg x).symm -#align real.tendsto_exp_neg_at_top_nhds_0 Real.tendsto_exp_neg_atTop_nhds_0 +#align real.tendsto_exp_neg_at_top_nhds_0 Real.tendsto_exp_neg_atTop_nhds_zero -/ -#print Real.tendsto_exp_nhds_0_nhds_1 /- +#print Real.tendsto_exp_nhds_zero_nhds_one /- /-- The real exponential function tends to `1` at `0`. -/ -theorem tendsto_exp_nhds_0_nhds_1 : Tendsto exp (𝓝 0) (𝓝 1) := by convert continuous_exp.tendsto 0; - simp -#align real.tendsto_exp_nhds_0_nhds_1 Real.tendsto_exp_nhds_0_nhds_1 +theorem tendsto_exp_nhds_zero_nhds_one : Tendsto exp (𝓝 0) (𝓝 1) := by + convert continuous_exp.tendsto 0; simp +#align real.tendsto_exp_nhds_0_nhds_1 Real.tendsto_exp_nhds_zero_nhds_one -/ #print Real.tendsto_exp_atBot /- theorem tendsto_exp_atBot : Tendsto exp atBot (𝓝 0) := - (tendsto_exp_neg_atTop_nhds_0.comp tendsto_neg_atBot_atTop).congr fun x => + (tendsto_exp_neg_atTop_nhds_zero.comp tendsto_neg_atBot_atTop).congr fun x => congr_arg exp <| neg_neg x #align real.tendsto_exp_at_bot Real.tendsto_exp_atBot -/ @@ -289,13 +289,13 @@ theorem tendsto_exp_div_pow_atTop (n : ℕ) : Tendsto (fun x => exp x / x ^ n) a #align real.tendsto_exp_div_pow_at_top Real.tendsto_exp_div_pow_atTop -/ -#print Real.tendsto_pow_mul_exp_neg_atTop_nhds_0 /- +#print Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero /- /-- The function `x^n * exp(-x)` tends to `0` at `+∞`, for any natural number `n`. -/ -theorem tendsto_pow_mul_exp_neg_atTop_nhds_0 (n : ℕ) : +theorem tendsto_pow_mul_exp_neg_atTop_nhds_zero (n : ℕ) : Tendsto (fun x => x ^ n * exp (-x)) atTop (𝓝 0) := (tendsto_inv_atTop_zero.comp (tendsto_exp_div_pow_atTop n)).congr fun x => by rw [comp_app, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, NormedSpace.exp_neg] -#align real.tendsto_pow_mul_exp_neg_at_top_nhds_0 Real.tendsto_pow_mul_exp_neg_atTop_nhds_0 +#align real.tendsto_pow_mul_exp_neg_at_top_nhds_0 Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero -/ #print Real.tendsto_mul_exp_add_div_pow_atTop /- diff --git a/Mathbin/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathbin/Analysis/SpecialFunctions/Gamma/Basic.lean index 26f332a7ee..62a2a5387d 100644 --- a/Mathbin/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathbin/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -299,7 +299,7 @@ theorem GammaIntegral_add_one {s : ℂ} (hs : 0 < s.re) : intro x hx; dsimp only rw [norm_eq_abs, map_mul, abs.map_neg, abs_cpow_eq_rpow_re_of_pos hx, abs_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul] - exact (tendsto_congr' this).mpr (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0 _ _ zero_lt_one) + exact (tendsto_congr' this).mpr (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ zero_lt_one) #align complex.Gamma_integral_add_one Complex.GammaIntegral_add_one -/ diff --git a/Mathbin/Analysis/SpecialFunctions/Gaussian.lean b/Mathbin/Analysis/SpecialFunctions/Gaussian.lean index f047a267f2..277719555b 100644 --- a/Mathbin/Analysis/SpecialFunctions/Gaussian.lean +++ b/Mathbin/Analysis/SpecialFunctions/Gaussian.lean @@ -218,7 +218,7 @@ theorem integral_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) : convert integral_Ioi_of_has_deriv_at_of_tendsto' (fun x hx => (A ↑x).comp_ofReal) (integrable_mul_cexp_neg_mul_sq hb).IntegrableOn B - simp only [MulZeroClass.mul_zero, of_real_zero, zero_pow', Ne.def, bit0_eq_zero, Nat.one_ne_zero, + simp only [MulZeroClass.mul_zero, of_real_zero, zero_pow, Ne.def, bit0_eq_zero, Nat.one_ne_zero, not_false_iff, Complex.exp_zero, mul_one, sub_neg_eq_add, zero_add] #align integral_mul_cexp_neg_mul_sq integral_mul_cexp_neg_mul_sq -/ diff --git a/Mathbin/Analysis/SpecialFunctions/Log/Deriv.lean b/Mathbin/Analysis/SpecialFunctions/Log/Deriv.lean index dd0ec5d018..5545518b7f 100644 --- a/Mathbin/Analysis/SpecialFunctions/Log/Deriv.lean +++ b/Mathbin/Analysis/SpecialFunctions/Log/Deriv.lean @@ -339,9 +339,9 @@ theorem abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) : #align real.abs_log_sub_add_sum_range_le Real.abs_log_sub_add_sum_range_le -/ -#print Real.hasSum_pow_div_log_of_abs_lt_1 /- +#print Real.hasSum_pow_div_log_of_abs_lt_one /- /-- Power series expansion of the logarithm around `1`. -/ -theorem hasSum_pow_div_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) : +theorem hasSum_pow_div_log_of_abs_lt_one {x : ℝ} (h : |x| < 1) : HasSum (fun n : ℕ => x ^ (n + 1) / (n + 1)) (-log (1 - x)) := by rw [Summable.hasSum_iff_tendsto_nat] @@ -353,9 +353,9 @@ theorem hasSum_pow_div_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) : simpa simp only [pow_succ] refine' (tendsto_const_nhds.mul _).div_const _ - exact tendsto_pow_atTop_nhds_0_of_lt_1 (abs_nonneg _) h + exact tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg _) h show Summable fun n : ℕ => x ^ (n + 1) / (n + 1) - · refine' Summable.of_norm_bounded _ (summable_geometric_of_lt_1 (abs_nonneg _) h) fun i => _ + · refine' Summable.of_norm_bounded _ (summable_geometric_of_lt_one (abs_nonneg _) h) fun i => _ calc ‖x ^ (i + 1) / (i + 1)‖ = |x| ^ (i + 1) / (i + 1) := by @@ -367,12 +367,12 @@ theorem hasSum_pow_div_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) : norm_num _ ≤ |x| ^ i := by simpa [pow_succ'] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h) -#align real.has_sum_pow_div_log_of_abs_lt_1 Real.hasSum_pow_div_log_of_abs_lt_1 +#align real.has_sum_pow_div_log_of_abs_lt_1 Real.hasSum_pow_div_log_of_abs_lt_one -/ -#print Real.hasSum_log_sub_log_of_abs_lt_1 /- +#print Real.hasSum_log_sub_log_of_abs_lt_one /- /-- Power series expansion of `log(1 + x) - log(1 - x)` for `|x| < 1`. -/ -theorem hasSum_log_sub_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) : +theorem hasSum_log_sub_log_of_abs_lt_one {x : ℝ} (h : |x| < 1) : HasSum (fun k : ℕ => (2 : ℝ) * (1 / (2 * k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x)) := by @@ -392,7 +392,7 @@ theorem hasSum_log_sub_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) : rw [range_two_mul, Set.mem_setOf_eq, ← Nat.even_add_one] at hm dsimp [term] rw [Even.neg_pow hm, neg_one_mul, neg_add_self] -#align real.has_sum_log_sub_log_of_abs_lt_1 Real.hasSum_log_sub_log_of_abs_lt_1 +#align real.has_sum_log_sub_log_of_abs_lt_1 Real.hasSum_log_sub_log_of_abs_lt_one -/ #print Real.hasSum_log_one_add_inv /- diff --git a/Mathbin/Analysis/SpecialFunctions/Pow/Asymptotics.lean b/Mathbin/Analysis/SpecialFunctions/Pow/Asymptotics.lean index 69a2277656..10f31b6840 100644 --- a/Mathbin/Analysis/SpecialFunctions/Pow/Asymptotics.lean +++ b/Mathbin/Analysis/SpecialFunctions/Pow/Asymptotics.lean @@ -122,15 +122,15 @@ theorem tendsto_exp_mul_div_rpow_atTop (s : ℝ) (b : ℝ) (hb : 0 < b) : /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:38: in filter_upwards #[[], ["with", ident x], ["using", expr by simp [] [] [] ["[", expr exp_neg, ",", expr inv_div, ",", expr div_eq_mul_inv _ (exp _), "]"] [] []]]: ./././Mathport/Syntax/Translate/Basic.lean:354:22: unsupported: parse error @ arg 0: next failed, no more args -/ -#print tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0 /- +#print tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero /- /-- The function `x ^ s * exp (-b * x)` tends to `0` at `+∞`, for any real `s` and `b > 0`. -/ -theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0 (s : ℝ) (b : ℝ) (hb : 0 < b) : +theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (s : ℝ) (b : ℝ) (hb : 0 < b) : Tendsto (fun x : ℝ => x ^ s * exp (-b * x)) atTop (𝓝 0) := by refine' (tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' _ trace "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:38: in filter_upwards #[[], [\"with\", ident x],\n [\"using\", expr by simp [] [] [] [\"[\", expr exp_neg, \",\", expr inv_div, \",\", expr div_eq_mul_inv _\n (exp _), \"]\"] [] []]]: ./././Mathport/Syntax/Translate/Basic.lean:354:22: unsupported: parse error @ arg 0: next failed, no more args" -#align tendsto_rpow_mul_exp_neg_mul_at_top_nhds_0 tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0 +#align tendsto_rpow_mul_exp_neg_mul_at_top_nhds_0 tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero -/ #print NNReal.tendsto_rpow_atTop /- @@ -278,7 +278,7 @@ theorem isLittleO_rpow_exp_pos_mul_atTop (s : ℝ) {b : ℝ} (hb : 0 < b) : (fun x : ℝ => x ^ s) =o[atTop] fun x => exp (b * x) := Iff.mpr (isLittleO_iff_tendsto fun x h => absurd h (exp_pos _).ne') <| by simpa only [div_eq_mul_inv, NormedSpace.exp_neg, neg_mul] using - tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0 s b hb + tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero s b hb #align is_o_rpow_exp_pos_mul_at_top isLittleO_rpow_exp_pos_mul_atTop -/ diff --git a/Mathbin/Analysis/SpecialFunctions/Stirling.lean b/Mathbin/Analysis/SpecialFunctions/Stirling.lean index f0a66a95ae..4ffba68a4e 100644 --- a/Mathbin/Analysis/SpecialFunctions/Stirling.lean +++ b/Mathbin/Analysis/SpecialFunctions/Stirling.lean @@ -133,7 +133,7 @@ theorem log_stirlingSeq_diff_le_geo_sum (n : ℕ) : HasSum (fun k : ℕ => ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) ^ k.succ) ((1 / (2 * n.succ + 1)) ^ 2 / (1 - (1 / (2 * n.succ + 1)) ^ 2)) := by - have := (hasSum_geometric_of_lt_1 h_nonneg _).hMul_left ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) + have := (hasSum_geometric_of_lt_one h_nonneg _).hMul_left ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) · simp_rw [← pow_succ] at this exact this rw [one_div, inv_pow] @@ -262,7 +262,7 @@ theorem tendsto_self_div_two_mul_self_add_one : skip rw [one_div, ← add_zero (2 : ℝ)] refine' - (((tendsto_const_div_atTop_nhds_0_nat 1).const_add (2 : ℝ)).inv₀ + (((tendsto_const_div_atTop_nhds_zero_nat 1).const_add (2 : ℝ)).inv₀ ((add_zero (2 : ℝ)).symm ▸ two_ne_zero)).congr' (eventually_at_top.mpr ⟨1, fun n hn => _⟩) rw [add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)), inv_div] diff --git a/Mathbin/Analysis/SpecificLimits/Basic.lean b/Mathbin/Analysis/SpecificLimits/Basic.lean index 8a5b4ec531..2b4318ce9f 100644 --- a/Mathbin/Analysis/SpecificLimits/Basic.lean +++ b/Mathbin/Analysis/SpecificLimits/Basic.lean @@ -31,37 +31,40 @@ open scoped Classical Topology Nat BigOperators uniformity NNReal ENNReal variable {α : Type _} {β : Type _} {ι : Type _} -#print tendsto_inverse_atTop_nhds_0_nat /- -theorem tendsto_inverse_atTop_nhds_0_nat : Tendsto (fun n : ℕ => (n : ℝ)⁻¹) atTop (𝓝 0) := +#print tendsto_inverse_atTop_nhds_zero_nat /- +theorem tendsto_inverse_atTop_nhds_zero_nat : Tendsto (fun n : ℕ => (n : ℝ)⁻¹) atTop (𝓝 0) := tendsto_inv_atTop_zero.comp tendsto_nat_cast_atTop_atTop -#align tendsto_inverse_at_top_nhds_0_nat tendsto_inverse_atTop_nhds_0_nat +#align tendsto_inverse_at_top_nhds_0_nat tendsto_inverse_atTop_nhds_zero_nat -/ -#print tendsto_const_div_atTop_nhds_0_nat /- -theorem tendsto_const_div_atTop_nhds_0_nat (C : ℝ) : Tendsto (fun n : ℕ => C / n) atTop (𝓝 0) := by - simpa only [MulZeroClass.mul_zero] using tendsto_const_nhds.mul tendsto_inverse_atTop_nhds_0_nat -#align tendsto_const_div_at_top_nhds_0_nat tendsto_const_div_atTop_nhds_0_nat +#print tendsto_const_div_atTop_nhds_zero_nat /- +theorem tendsto_const_div_atTop_nhds_zero_nat (C : ℝ) : Tendsto (fun n : ℕ => C / n) atTop (𝓝 0) := + by + simpa only [MulZeroClass.mul_zero] using + tendsto_const_nhds.mul tendsto_inverse_atTop_nhds_zero_nat +#align tendsto_const_div_at_top_nhds_0_nat tendsto_const_div_atTop_nhds_zero_nat -/ -#print NNReal.tendsto_inverse_atTop_nhds_0_nat /- -theorem NNReal.tendsto_inverse_atTop_nhds_0_nat : Tendsto (fun n : ℕ => (n : ℝ≥0)⁻¹) atTop (𝓝 0) := - by rw [← NNReal.tendsto_coe]; exact tendsto_inverse_atTop_nhds_0_nat -#align nnreal.tendsto_inverse_at_top_nhds_0_nat NNReal.tendsto_inverse_atTop_nhds_0_nat +#print NNReal.tendsto_inverse_atTop_nhds_zero_nat /- +theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat : + Tendsto (fun n : ℕ => (n : ℝ≥0)⁻¹) atTop (𝓝 0) := by rw [← NNReal.tendsto_coe]; + exact tendsto_inverse_atTop_nhds_zero_nat +#align nnreal.tendsto_inverse_at_top_nhds_0_nat NNReal.tendsto_inverse_atTop_nhds_zero_nat -/ -#print NNReal.tendsto_const_div_atTop_nhds_0_nat /- -theorem NNReal.tendsto_const_div_atTop_nhds_0_nat (C : ℝ≥0) : +#print NNReal.tendsto_const_div_atTop_nhds_zero_nat /- +theorem NNReal.tendsto_const_div_atTop_nhds_zero_nat (C : ℝ≥0) : Tendsto (fun n : ℕ => C / n) atTop (𝓝 0) := by - simpa using tendsto_const_nhds.mul NNReal.tendsto_inverse_atTop_nhds_0_nat -#align nnreal.tendsto_const_div_at_top_nhds_0_nat NNReal.tendsto_const_div_atTop_nhds_0_nat + simpa using tendsto_const_nhds.mul NNReal.tendsto_inverse_atTop_nhds_zero_nat +#align nnreal.tendsto_const_div_at_top_nhds_0_nat NNReal.tendsto_const_div_atTop_nhds_zero_nat -/ -#print tendsto_one_div_add_atTop_nhds_0_nat /- -theorem tendsto_one_div_add_atTop_nhds_0_nat : +#print tendsto_one_div_add_atTop_nhds_zero_nat /- +theorem tendsto_one_div_add_atTop_nhds_zero_nat : Tendsto (fun n : ℕ => 1 / ((n : ℝ) + 1)) atTop (𝓝 0) := suffices Tendsto (fun n : ℕ => 1 / (↑(n + 1) : ℝ)) atTop (𝓝 0) by simpa - (tendsto_add_atTop_iff_nat 1).2 (tendsto_const_div_atTop_nhds_0_nat 1) -#align tendsto_one_div_add_at_top_nhds_0_nat tendsto_one_div_add_atTop_nhds_0_nat + (tendsto_add_atTop_iff_nat 1).2 (tendsto_const_div_atTop_nhds_zero_nat 1) +#align tendsto_one_div_add_at_top_nhds_0_nat tendsto_one_div_add_atTop_nhds_zero_nat -/ #print tendsto_coe_nat_div_add_atTop /- @@ -89,7 +92,7 @@ theorem tendsto_coe_nat_div_add_atTop {𝕜 : Type _} [DivisionRing 𝕜] [Topol rw [← map_natCast (algebraMap ℝ 𝕜) n, ← map_inv₀ (algebraMap ℝ 𝕜)] rfl rw [this] - exact ((continuous_algebraMap ℝ 𝕜).Tendsto _).comp tendsto_inverse_atTop_nhds_0_nat + exact ((continuous_algebraMap ℝ 𝕜).Tendsto _).comp tendsto_inverse_atTop_nhds_zero_nat #align tendsto_coe_nat_div_add_at_top tendsto_coe_nat_div_add_atTop -/ @@ -119,8 +122,8 @@ theorem Nat.tendsto_pow_atTop_atTop_of_one_lt {m : ℕ} (h : 1 < m) : #align nat.tendsto_pow_at_top_at_top_of_one_lt Nat.tendsto_pow_atTop_atTop_of_one_lt -/ -#print tendsto_pow_atTop_nhds_0_of_lt_1 /- -theorem tendsto_pow_atTop_nhds_0_of_lt_1 {𝕜 : Type _} [LinearOrderedField 𝕜] [Archimedean 𝕜] +#print tendsto_pow_atTop_nhds_zero_of_lt_one /- +theorem tendsto_pow_atTop_nhds_zero_of_lt_one {𝕜 : Type _} [LinearOrderedField 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) := h₁.eq_or_lt.elim @@ -130,25 +133,25 @@ theorem tendsto_pow_atTop_nhds_0_of_lt_1 {𝕜 : Type _} [LinearOrderedField have : Tendsto (fun n => (r⁻¹ ^ n)⁻¹) atTop (𝓝 0) := tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt <| one_lt_inv this h₂) this.congr fun n => by simp -#align tendsto_pow_at_top_nhds_0_of_lt_1 tendsto_pow_atTop_nhds_0_of_lt_1 +#align tendsto_pow_at_top_nhds_0_of_lt_1 tendsto_pow_atTop_nhds_zero_of_lt_one -/ -#print tendsto_pow_atTop_nhdsWithin_0_of_lt_1 /- -theorem tendsto_pow_atTop_nhdsWithin_0_of_lt_1 {𝕜 : Type _} [LinearOrderedField 𝕜] [Archimedean 𝕜] - [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) : +#print tendsto_pow_atTop_nhdsWithin_zero_of_lt_one /- +theorem tendsto_pow_atTop_nhdsWithin_zero_of_lt_one {𝕜 : Type _} [LinearOrderedField 𝕜] + [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝[>] 0) := tendsto_inf.2 - ⟨tendsto_pow_atTop_nhds_0_of_lt_1 h₁.le h₂, + ⟨tendsto_pow_atTop_nhds_zero_of_lt_one h₁.le h₂, tendsto_principal.2 <| eventually_of_forall fun n => pow_pos h₁ _⟩ -#align tendsto_pow_at_top_nhds_within_0_of_lt_1 tendsto_pow_atTop_nhdsWithin_0_of_lt_1 +#align tendsto_pow_at_top_nhds_within_0_of_lt_1 tendsto_pow_atTop_nhdsWithin_zero_of_lt_one -/ -#print uniformity_basis_dist_pow_of_lt_1 /- -theorem uniformity_basis_dist_pow_of_lt_1 {α : Type _} [PseudoMetricSpace α] {r : ℝ} (h₀ : 0 < r) +#print uniformity_basis_dist_pow_of_lt_one /- +theorem uniformity_basis_dist_pow_of_lt_one {α : Type _} [PseudoMetricSpace α] {r : ℝ} (h₀ : 0 < r) (h₁ : r < 1) : (𝓤 α).HasBasis (fun k : ℕ => True) fun k => {p : α × α | dist p.1 p.2 < r ^ k} := Metric.mk_uniformity_basis (fun i _ => pow_pos h₀ _) fun ε ε0 => (exists_pow_lt_of_lt_one ε0 h₁).imp fun k hk => ⟨trivial, hk.le⟩ -#align uniformity_basis_dist_pow_of_lt_1 uniformity_basis_dist_pow_of_lt_1 +#align uniformity_basis_dist_pow_of_lt_1 uniformity_basis_dist_pow_of_lt_one -/ #print geom_lt /- @@ -197,23 +200,24 @@ theorem tendsto_atTop_of_geom_le {v : ℕ → ℝ} {c : ℝ} (h₀ : 0 < v 0) (h #align tendsto_at_top_of_geom_le tendsto_atTop_of_geom_le -/ -#print NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 /- -theorem NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 {r : ℝ≥0} (hr : r < 1) : +#print NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one /- +theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0} (hr : r < 1) : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) := NNReal.tendsto_coe.1 <| by - simp only [NNReal.coe_pow, NNReal.coe_zero, tendsto_pow_atTop_nhds_0_of_lt_1 r.coe_nonneg hr] -#align nnreal.tendsto_pow_at_top_nhds_0_of_lt_1 NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 + simp only [NNReal.coe_pow, NNReal.coe_zero, + tendsto_pow_atTop_nhds_zero_of_lt_one r.coe_nonneg hr] +#align nnreal.tendsto_pow_at_top_nhds_0_of_lt_1 NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one -/ -#print ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 /- -theorem ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 {r : ℝ≥0∞} (hr : r < 1) : +#print ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one /- +theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0∞} (hr : r < 1) : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) := by rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩ rw [← ENNReal.coe_zero] norm_cast at * - apply NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 hr -#align ennreal.tendsto_pow_at_top_nhds_0_of_lt_1 ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 + apply NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hr +#align ennreal.tendsto_pow_at_top_nhds_0_of_lt_1 ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one -/ /-! ### Geometric series-/ @@ -221,33 +225,33 @@ theorem ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 {r : ℝ≥0∞} (hr : r < 1) : section Geometric -#print hasSum_geometric_of_lt_1 /- -theorem hasSum_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : +#print hasSum_geometric_of_lt_one /- +theorem hasSum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : HasSum (fun n : ℕ => r ^ n) (1 - r)⁻¹ := have : r ≠ 1 := ne_of_lt h₂ have : Tendsto (fun n => (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹)) := - ((tendsto_pow_atTop_nhds_0_of_lt_1 h₁ h₂).sub tendsto_const_nhds).mul tendsto_const_nhds + ((tendsto_pow_atTop_nhds_zero_of_lt_one h₁ h₂).sub tendsto_const_nhds).mul tendsto_const_nhds (hasSum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr <| by simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv] -#align has_sum_geometric_of_lt_1 hasSum_geometric_of_lt_1 +#align has_sum_geometric_of_lt_1 hasSum_geometric_of_lt_one -/ -#print summable_geometric_of_lt_1 /- -theorem summable_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : +#print summable_geometric_of_lt_one /- +theorem summable_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : Summable fun n : ℕ => r ^ n := - ⟨_, hasSum_geometric_of_lt_1 h₁ h₂⟩ -#align summable_geometric_of_lt_1 summable_geometric_of_lt_1 + ⟨_, hasSum_geometric_of_lt_one h₁ h₂⟩ +#align summable_geometric_of_lt_1 summable_geometric_of_lt_one -/ -#print tsum_geometric_of_lt_1 /- -theorem tsum_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ := - (hasSum_geometric_of_lt_1 h₁ h₂).tsum_eq -#align tsum_geometric_of_lt_1 tsum_geometric_of_lt_1 +#print tsum_geometric_of_lt_one /- +theorem tsum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ := + (hasSum_geometric_of_lt_one h₁ h₂).tsum_eq +#align tsum_geometric_of_lt_1 tsum_geometric_of_lt_one -/ #print hasSum_geometric_two /- theorem hasSum_geometric_two : HasSum (fun n : ℕ => ((1 : ℝ) / 2) ^ n) 2 := by - convert hasSum_geometric_of_lt_1 _ _ <;> norm_num + convert hasSum_geometric_of_lt_one _ _ <;> norm_num #align has_sum_geometric_two hasSum_geometric_two -/ @@ -303,7 +307,8 @@ theorem tsum_geometric_inv_two_ge (n : ℕ) : ∑' i, ite (n ≤ i) ((2 : ℝ) #print hasSum_geometric_two' /- theorem hasSum_geometric_two' (a : ℝ) : HasSum (fun n : ℕ => a / 2 / 2 ^ n) a := by - convert HasSum.mul_left (a / 2) (hasSum_geometric_of_lt_1 (le_of_lt one_half_pos) one_half_lt_one) + convert + HasSum.mul_left (a / 2) (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one) · funext n; simp; rfl · norm_num #align has_sum_geometric_two' hasSum_geometric_two' @@ -328,7 +333,7 @@ theorem NNReal.hasSum_geometric {r : ℝ≥0} (hr : r < 1) : HasSum (fun n : ℕ apply NNReal.hasSum_coe.1 push_cast rw [NNReal.coe_sub (le_of_lt hr)] - exact hasSum_geometric_of_lt_1 r.coe_nonneg hr + exact hasSum_geometric_of_lt_one r.coe_nonneg hr #align nnreal.has_sum_geometric NNReal.hasSum_geometric -/ @@ -464,7 +469,7 @@ theorem aux_hasSum_of_le_geometric : HasSum (fun n : ℕ => C * r ^ n) (C / (1 - rcases sign_cases_of_C_mul_pow_nonneg fun n => dist_nonneg.trans (hu n) with (rfl | ⟨C₀, r₀⟩) · simp [hasSum_zero] · refine' HasSum.mul_left C _ - simpa using hasSum_geometric_of_lt_1 r₀ hr + simpa using hasSum_geometric_of_lt_one r₀ hr #align aux_has_sum_of_le_geometric aux_hasSum_of_le_geometric -/ @@ -546,7 +551,7 @@ theorem summable_one_div_pow_of_le {m : ℝ} {f : ℕ → ℕ} (hm : 1 < m) (fi refine' Summable.of_nonneg_of_le (fun a => one_div_nonneg.mpr (pow_nonneg (zero_le_one.trans hm.le) _)) (fun a => _) - (summable_geometric_of_lt_1 (one_div_nonneg.mpr (zero_le_one.trans hm.le)) + (summable_geometric_of_lt_one (one_div_nonneg.mpr (zero_le_one.trans hm.le)) ((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm))) rw [div_pow, one_pow] refine' (one_div_le_one_div _ _).mpr (pow_le_pow_right hm.le (fi a)) <;> @@ -667,7 +672,7 @@ theorem factorial_tendsto_atTop : Tendsto Nat.factorial atTop atTop := #print tendsto_factorial_div_pow_self_atTop /- theorem tendsto_factorial_div_pow_self_atTop : Tendsto (fun n => n ! / n ^ n : ℕ → ℝ) atTop (𝓝 0) := tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds - (tendsto_const_div_atTop_nhds_0_nat 1) + (tendsto_const_div_atTop_nhds_zero_nat 1) (eventually_of_forall fun n => div_nonneg (by exact_mod_cast n.factorial_pos.le) (pow_nonneg (by exact_mod_cast n.zero_le) _)) diff --git a/Mathbin/Analysis/SpecificLimits/Normed.lean b/Mathbin/Analysis/SpecificLimits/Normed.lean index 907273b682..972f3cd458 100644 --- a/Mathbin/Analysis/SpecificLimits/Normed.lean +++ b/Mathbin/Analysis/SpecificLimits/Normed.lean @@ -116,7 +116,8 @@ theorem isLittleO_pow_pow_of_lt_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ (fun n : ℕ => r₁ ^ n) =o[atTop] fun n => r₂ ^ n := have H : 0 < r₂ := h₁.trans_lt h₂ (isLittleO_of_tendsto fun n hn => False.elim <| H.ne' <| pow_eq_zero hn) <| - (tendsto_pow_atTop_nhds_0_of_lt_1 (div_nonneg h₁ (h₁.trans h₂.le)) ((div_lt_one H).2 h₂)).congr + (tendsto_pow_atTop_nhds_zero_of_lt_one (div_nonneg h₁ (h₁.trans h₂.le)) + ((div_lt_one H).2 h₂)).congr fun n => div_pow _ _ _ #align is_o_pow_pow_of_lt_left isLittleO_pow_pow_of_lt_left -/ @@ -305,21 +306,21 @@ theorem tendsto_self_mul_const_pow_of_lt_one {r : ℝ} (hr : 0 ≤ r) (h'r : r < #align tendsto_self_mul_const_pow_of_lt_one tendsto_self_mul_const_pow_of_lt_one -/ -#print tendsto_pow_atTop_nhds_0_of_norm_lt_1 /- +#print tendsto_pow_atTop_nhds_zero_of_norm_lt_one /- /-- In a normed ring, the powers of an element x with `‖x‖ < 1` tend to zero. -/ -theorem tendsto_pow_atTop_nhds_0_of_norm_lt_1 {R : Type _} [NormedRing R] {x : R} (h : ‖x‖ < 1) : - Tendsto (fun n : ℕ => x ^ n) atTop (𝓝 0) := +theorem tendsto_pow_atTop_nhds_zero_of_norm_lt_one {R : Type _} [NormedRing R] {x : R} + (h : ‖x‖ < 1) : Tendsto (fun n : ℕ => x ^ n) atTop (𝓝 0) := by apply squeeze_zero_norm' (eventually_norm_pow_le x) - exact tendsto_pow_atTop_nhds_0_of_lt_1 (norm_nonneg _) h -#align tendsto_pow_at_top_nhds_0_of_norm_lt_1 tendsto_pow_atTop_nhds_0_of_norm_lt_1 + exact tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) h +#align tendsto_pow_at_top_nhds_0_of_norm_lt_1 tendsto_pow_atTop_nhds_zero_of_norm_lt_one -/ -#print tendsto_pow_atTop_nhds_0_of_abs_lt_1 /- -theorem tendsto_pow_atTop_nhds_0_of_abs_lt_1 {r : ℝ} (h : |r| < 1) : +#print tendsto_pow_atTop_nhds_zero_of_abs_lt_one /- +theorem tendsto_pow_atTop_nhds_zero_of_abs_lt_one {r : ℝ} (h : |r| < 1) : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) := - tendsto_pow_atTop_nhds_0_of_norm_lt_1 h -#align tendsto_pow_at_top_nhds_0_of_abs_lt_1 tendsto_pow_atTop_nhds_0_of_abs_lt_1 + tendsto_pow_atTop_nhds_zero_of_norm_lt_one h +#align tendsto_pow_at_top_nhds_0_of_abs_lt_1 tendsto_pow_atTop_nhds_zero_of_abs_lt_one -/ /-! ### Geometric series-/ @@ -329,94 +330,94 @@ section Geometric variable {K : Type _} [NormedField K] {ξ : K} -#print hasSum_geometric_of_norm_lt_1 /- -theorem hasSum_geometric_of_norm_lt_1 (h : ‖ξ‖ < 1) : HasSum (fun n : ℕ => ξ ^ n) (1 - ξ)⁻¹ := +#print hasSum_geometric_of_norm_lt_one /- +theorem hasSum_geometric_of_norm_lt_one (h : ‖ξ‖ < 1) : HasSum (fun n : ℕ => ξ ^ n) (1 - ξ)⁻¹ := by have xi_ne_one : ξ ≠ 1 := by contrapose! h; simp [h] have A : tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) at_top (𝓝 ((0 - 1) * (ξ - 1)⁻¹)) := - ((tendsto_pow_atTop_nhds_0_of_norm_lt_1 h).sub tendsto_const_nhds).mul tendsto_const_nhds + ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one h).sub tendsto_const_nhds).mul tendsto_const_nhds rw [hasSum_iff_tendsto_nat_of_summable_norm] · simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A - · simp [norm_pow, summable_geometric_of_lt_1 (norm_nonneg _) h] -#align has_sum_geometric_of_norm_lt_1 hasSum_geometric_of_norm_lt_1 + · simp [norm_pow, summable_geometric_of_lt_one (norm_nonneg _) h] +#align has_sum_geometric_of_norm_lt_1 hasSum_geometric_of_norm_lt_one -/ -#print summable_geometric_of_norm_lt_1 /- -theorem summable_geometric_of_norm_lt_1 (h : ‖ξ‖ < 1) : Summable fun n : ℕ => ξ ^ n := - ⟨_, hasSum_geometric_of_norm_lt_1 h⟩ -#align summable_geometric_of_norm_lt_1 summable_geometric_of_norm_lt_1 +#print summable_geometric_of_norm_lt_one /- +theorem summable_geometric_of_norm_lt_one (h : ‖ξ‖ < 1) : Summable fun n : ℕ => ξ ^ n := + ⟨_, hasSum_geometric_of_norm_lt_one h⟩ +#align summable_geometric_of_norm_lt_1 summable_geometric_of_norm_lt_one -/ -#print tsum_geometric_of_norm_lt_1 /- -theorem tsum_geometric_of_norm_lt_1 (h : ‖ξ‖ < 1) : ∑' n : ℕ, ξ ^ n = (1 - ξ)⁻¹ := - (hasSum_geometric_of_norm_lt_1 h).tsum_eq -#align tsum_geometric_of_norm_lt_1 tsum_geometric_of_norm_lt_1 +#print tsum_geometric_of_norm_lt_one /- +theorem tsum_geometric_of_norm_lt_one (h : ‖ξ‖ < 1) : ∑' n : ℕ, ξ ^ n = (1 - ξ)⁻¹ := + (hasSum_geometric_of_norm_lt_one h).tsum_eq +#align tsum_geometric_of_norm_lt_1 tsum_geometric_of_norm_lt_one -/ -#print hasSum_geometric_of_abs_lt_1 /- -theorem hasSum_geometric_of_abs_lt_1 {r : ℝ} (h : |r| < 1) : +#print hasSum_geometric_of_abs_lt_one /- +theorem hasSum_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : HasSum (fun n : ℕ => r ^ n) (1 - r)⁻¹ := - hasSum_geometric_of_norm_lt_1 h -#align has_sum_geometric_of_abs_lt_1 hasSum_geometric_of_abs_lt_1 + hasSum_geometric_of_norm_lt_one h +#align has_sum_geometric_of_abs_lt_1 hasSum_geometric_of_abs_lt_one -/ -#print summable_geometric_of_abs_lt_1 /- -theorem summable_geometric_of_abs_lt_1 {r : ℝ} (h : |r| < 1) : Summable fun n : ℕ => r ^ n := - summable_geometric_of_norm_lt_1 h -#align summable_geometric_of_abs_lt_1 summable_geometric_of_abs_lt_1 +#print summable_geometric_of_abs_lt_one /- +theorem summable_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : Summable fun n : ℕ => r ^ n := + summable_geometric_of_norm_lt_one h +#align summable_geometric_of_abs_lt_1 summable_geometric_of_abs_lt_one -/ -#print tsum_geometric_of_abs_lt_1 /- -theorem tsum_geometric_of_abs_lt_1 {r : ℝ} (h : |r| < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ := - tsum_geometric_of_norm_lt_1 h -#align tsum_geometric_of_abs_lt_1 tsum_geometric_of_abs_lt_1 +#print tsum_geometric_of_abs_lt_one /- +theorem tsum_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ := + tsum_geometric_of_norm_lt_one h +#align tsum_geometric_of_abs_lt_1 tsum_geometric_of_abs_lt_one -/ -#print summable_geometric_iff_norm_lt_1 /- +#print summable_geometric_iff_norm_lt_one /- /-- A geometric series in a normed field is summable iff the norm of the common ratio is less than one. -/ @[simp] -theorem summable_geometric_iff_norm_lt_1 : (Summable fun n : ℕ => ξ ^ n) ↔ ‖ξ‖ < 1 := +theorem summable_geometric_iff_norm_lt_one : (Summable fun n : ℕ => ξ ^ n) ↔ ‖ξ‖ < 1 := by - refine' ⟨fun h => _, summable_geometric_of_norm_lt_1⟩ + refine' ⟨fun h => _, summable_geometric_of_norm_lt_one⟩ obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ := (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists simp only [norm_pow, dist_zero_right] at hk rw [← one_pow k] at hk exact lt_of_pow_lt_pow_left _ zero_le_one hk -#align summable_geometric_iff_norm_lt_1 summable_geometric_iff_norm_lt_1 +#align summable_geometric_iff_norm_lt_1 summable_geometric_iff_norm_lt_one -/ end Geometric section MulGeometric -#print summable_norm_pow_mul_geometric_of_norm_lt_1 /- -theorem summable_norm_pow_mul_geometric_of_norm_lt_1 {R : Type _} [NormedRing R] (k : ℕ) {r : R} +#print summable_norm_pow_mul_geometric_of_norm_lt_one /- +theorem summable_norm_pow_mul_geometric_of_norm_lt_one {R : Type _} [NormedRing R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : Summable fun n : ℕ => ‖(n ^ k * r ^ n : R)‖ := by rcases exists_between hr with ⟨r', hrr', h⟩ exact - summable_of_isBigO_nat (summable_geometric_of_lt_1 ((norm_nonneg _).trans hrr'.le) h) + summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h) (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt _ hrr').IsBigO.norm_left -#align summable_norm_pow_mul_geometric_of_norm_lt_1 summable_norm_pow_mul_geometric_of_norm_lt_1 +#align summable_norm_pow_mul_geometric_of_norm_lt_1 summable_norm_pow_mul_geometric_of_norm_lt_one -/ -#print summable_pow_mul_geometric_of_norm_lt_1 /- -theorem summable_pow_mul_geometric_of_norm_lt_1 {R : Type _} [NormedRing R] [CompleteSpace R] +#print summable_pow_mul_geometric_of_norm_lt_one /- +theorem summable_pow_mul_geometric_of_norm_lt_one {R : Type _} [NormedRing R] [CompleteSpace R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : Summable (fun n => n ^ k * r ^ n : ℕ → R) := - Summable.of_norm <| summable_norm_pow_mul_geometric_of_norm_lt_1 _ hr -#align summable_pow_mul_geometric_of_norm_lt_1 summable_pow_mul_geometric_of_norm_lt_1 + Summable.of_norm <| summable_norm_pow_mul_geometric_of_norm_lt_one _ hr +#align summable_pow_mul_geometric_of_norm_lt_1 summable_pow_mul_geometric_of_norm_lt_one -/ -#print hasSum_coe_mul_geometric_of_norm_lt_1 /- +#print hasSum_coe_mul_geometric_of_norm_lt_one /- /-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, `has_sum` version. -/ -theorem hasSum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type _} [NormedField 𝕜] [CompleteSpace 𝕜] {r : 𝕜} - (hr : ‖r‖ < 1) : HasSum (fun n => n * r ^ n : ℕ → 𝕜) (r / (1 - r) ^ 2) := +theorem hasSum_coe_mul_geometric_of_norm_lt_one {𝕜 : Type _} [NormedField 𝕜] [CompleteSpace 𝕜] + {r : 𝕜} (hr : ‖r‖ < 1) : HasSum (fun n => n * r ^ n : ℕ → 𝕜) (r / (1 - r) ^ 2) := by have A : Summable (fun n => n * r ^ n : ℕ → 𝕜) := by - simpa using summable_pow_mul_geometric_of_norm_lt_1 1 hr - have B : HasSum (pow r : ℕ → 𝕜) (1 - r)⁻¹ := hasSum_geometric_of_norm_lt_1 hr + simpa using summable_pow_mul_geometric_of_norm_lt_one 1 hr + have B : HasSum (pow r : ℕ → 𝕜) (1 - r)⁻¹ := hasSum_geometric_of_norm_lt_one hr refine' A.has_sum_iff.2 _ have hr' : r ≠ 1 := by rintro rfl; simpa [lt_irrefl] using hr set s : 𝕜 := ∑' n : ℕ, n * r ^ n @@ -429,15 +430,15 @@ theorem hasSum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type _} [NormedField 𝕜] simp [pow_succ, mul_left_comm _ r, tsum_mul_left] _ = r / (1 - r) ^ 2 := by simp [add_mul, tsum_add A B.summable, mul_add, B.tsum_eq, ← div_eq_mul_inv, sq, div_div] -#align has_sum_coe_mul_geometric_of_norm_lt_1 hasSum_coe_mul_geometric_of_norm_lt_1 +#align has_sum_coe_mul_geometric_of_norm_lt_1 hasSum_coe_mul_geometric_of_norm_lt_one -/ -#print tsum_coe_mul_geometric_of_norm_lt_1 /- +#print tsum_coe_mul_geometric_of_norm_lt_one /- /-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`. -/ -theorem tsum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type _} [NormedField 𝕜] [CompleteSpace 𝕜] {r : 𝕜} +theorem tsum_coe_mul_geometric_of_norm_lt_one {𝕜 : Type _} [NormedField 𝕜] [CompleteSpace 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) : (∑' n : ℕ, n * r ^ n : 𝕜) = r / (1 - r) ^ 2 := - (hasSum_coe_mul_geometric_of_norm_lt_1 hr).tsum_eq -#align tsum_coe_mul_geometric_of_norm_lt_1 tsum_coe_mul_geometric_of_norm_lt_1 + (hasSum_coe_mul_geometric_of_norm_lt_one hr).tsum_eq +#align tsum_coe_mul_geometric_of_norm_lt_1 tsum_coe_mul_geometric_of_norm_lt_one -/ end MulGeometric @@ -547,44 +548,44 @@ variable {R : Type _} [NormedRing R] [CompleteSpace R] open NormedSpace -#print NormedRing.summable_geometric_of_norm_lt_1 /- +#print NormedRing.summable_geometric_of_norm_lt_one /- /-- A geometric series in a complete normed ring is summable. Proved above (same name, different namespace) for not-necessarily-complete normed fields. -/ -theorem NormedRing.summable_geometric_of_norm_lt_1 (x : R) (h : ‖x‖ < 1) : +theorem NormedRing.summable_geometric_of_norm_lt_one (x : R) (h : ‖x‖ < 1) : Summable fun n : ℕ => x ^ n := by - have h1 : Summable fun n : ℕ => ‖x‖ ^ n := summable_geometric_of_lt_1 (norm_nonneg _) h + have h1 : Summable fun n : ℕ => ‖x‖ ^ n := summable_geometric_of_lt_one (norm_nonneg _) h refine' Summable.of_norm_bounded_eventually _ h1 _ rw [Nat.cofinite_eq_atTop] exact eventually_norm_pow_le x -#align normed_ring.summable_geometric_of_norm_lt_1 NormedRing.summable_geometric_of_norm_lt_1 +#align normed_ring.summable_geometric_of_norm_lt_1 NormedRing.summable_geometric_of_norm_lt_one -/ -#print NormedRing.tsum_geometric_of_norm_lt_1 /- +#print NormedRing.tsum_geometric_of_norm_lt_one /- /-- Bound for the sum of a geometric series in a normed ring. This formula does not assume that the normed ring satisfies the axiom `‖1‖ = 1`. -/ -theorem NormedRing.tsum_geometric_of_norm_lt_1 (x : R) (h : ‖x‖ < 1) : +theorem NormedRing.tsum_geometric_of_norm_lt_one (x : R) (h : ‖x‖ < 1) : ‖∑' n : ℕ, x ^ n‖ ≤ ‖(1 : R)‖ - 1 + (1 - ‖x‖)⁻¹ := by - rw [tsum_eq_zero_add (NormedRing.summable_geometric_of_norm_lt_1 x h)] + rw [tsum_eq_zero_add (NormedRing.summable_geometric_of_norm_lt_one x h)] simp only [pow_zero] refine' le_trans (norm_add_le _ _) _ have : ‖∑' b : ℕ, (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1 := by refine' tsum_of_norm_bounded _ fun b => norm_pow_le' _ (Nat.succ_pos b) - convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_1 (norm_nonneg x) h) + convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h) simp linarith -#align normed_ring.tsum_geometric_of_norm_lt_1 NormedRing.tsum_geometric_of_norm_lt_1 +#align normed_ring.tsum_geometric_of_norm_lt_1 NormedRing.tsum_geometric_of_norm_lt_one -/ #print geom_series_mul_neg /- theorem geom_series_mul_neg (x : R) (h : ‖x‖ < 1) : (∑' i : ℕ, x ^ i) * (1 - x) = 1 := by - have := (NormedRing.summable_geometric_of_norm_lt_1 x h).HasSum.mul_right (1 - x) + have := (NormedRing.summable_geometric_of_norm_lt_one x h).HasSum.mul_right (1 - x) refine' tendsto_nhds_unique this.tendsto_sum_nat _ have : tendsto (fun n : ℕ => 1 - x ^ n) at_top (𝓝 1) := by - simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_0_of_norm_lt_1 h) + simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h) convert ← this ext n rw [← geom_sum_mul_neg, Finset.sum_mul] @@ -594,10 +595,10 @@ theorem geom_series_mul_neg (x : R) (h : ‖x‖ < 1) : (∑' i : ℕ, x ^ i) * #print mul_neg_geom_series /- theorem mul_neg_geom_series (x : R) (h : ‖x‖ < 1) : (1 - x) * ∑' i : ℕ, x ^ i = 1 := by - have := (NormedRing.summable_geometric_of_norm_lt_1 x h).HasSum.mul_left (1 - x) + have := (NormedRing.summable_geometric_of_norm_lt_one x h).HasSum.mul_left (1 - x) refine' tendsto_nhds_unique this.tendsto_sum_nat _ have : tendsto (fun n : ℕ => 1 - x ^ n) at_top (nhds 1) := by - simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_0_of_norm_lt_1 h) + simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_norm_lt_one h) convert ← this ext n rw [← mul_neg_geom_sum, Finset.mul_sum] @@ -620,7 +621,7 @@ theorem summable_of_ratio_norm_eventually_le {α : Type _} [SeminormedAddCommGro rw [← @summable_nat_add_iff α _ _ _ _ N] refine' Summable.of_norm_bounded (fun n => ‖f N‖ * r ^ n) - (Summable.mul_left _ <| summable_geometric_of_lt_1 hr₀ hr₁) fun n => _ + (Summable.mul_left _ <| summable_geometric_of_lt_one hr₀ hr₁) fun n => _ conv_rhs => rw [mul_comm, ← zero_add N] refine' le_geom hr₀ n fun i _ => _ convert hN (i + N) (N.le_add_left i) using 3 diff --git a/Mathbin/Data/Real/Cardinality.lean b/Mathbin/Data/Real/Cardinality.lean index 9078ca0f5f..53a6b452f8 100644 --- a/Mathbin/Data/Real/Cardinality.lean +++ b/Mathbin/Data/Real/Cardinality.lean @@ -109,7 +109,7 @@ theorem cantorFunctionAux_succ (f : ℕ → Bool) : theorem summable_cantor_function (f : ℕ → Bool) (h1 : 0 ≤ c) (h2 : c < 1) : Summable (cantorFunctionAux c f) := by - apply (summable_geometric_of_lt_1 h1 h2).summable_of_eq_zero_or_self + apply (summable_geometric_of_lt_one h1 h2).summable_of_eq_zero_or_self intro n; cases h : f n <;> simp [h] #align cardinal.summable_cantor_function Cardinal.summable_cantor_function -/ @@ -165,7 +165,7 @@ theorem increasing_cantorFunction (h1 : 0 < c) (h2 : c < 1 / 2) {n : ℕ} {f g : rwa [sub_pos] convert this · rw [cantor_function_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ← - tsum_geometric_of_lt_1 (le_of_lt h1) h3] + tsum_geometric_of_lt_one (le_of_lt h1) h3] apply zero_add · refine' (tsum_eq_single 0 _).trans _ · intro n hn; cases n; contradiction; rfl diff --git a/Mathbin/Data/Real/Hyperreal.lean b/Mathbin/Data/Real/Hyperreal.lean index c2feb9e7d9..ebffbff94b 100644 --- a/Mathbin/Data/Real/Hyperreal.lean +++ b/Mathbin/Data/Real/Hyperreal.lean @@ -297,7 +297,7 @@ theorem gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : Tendsto f atTop (𝓝 #print Hyperreal.epsilon_lt_pos /- theorem epsilon_lt_pos (x : ℝ) : 0 < x → ε < x := - lt_of_tendsto_zero_of_pos tendsto_inverse_atTop_nhds_0_nat + lt_of_tendsto_zero_of_pos tendsto_inverse_atTop_nhds_zero_nat #align hyperreal.epsilon_lt_pos Hyperreal.epsilon_lt_pos -/ @@ -1095,7 +1095,7 @@ theorem infinitesimal_of_tendsto_zero {f : ℕ → ℝ} : #print Hyperreal.infinitesimal_epsilon /- theorem infinitesimal_epsilon : Infinitesimal ε := - infinitesimal_of_tendsto_zero tendsto_inverse_atTop_nhds_0_nat + infinitesimal_of_tendsto_zero tendsto_inverse_atTop_nhds_zero_nat #align hyperreal.infinitesimal_epsilon Hyperreal.infinitesimal_epsilon -/ diff --git a/Mathbin/Data/Real/Pi/Wallis.lean b/Mathbin/Data/Real/Pi/Wallis.lean index 141f2c490e..673156a67d 100644 --- a/Mathbin/Data/Real/Pi/Wallis.lean +++ b/Mathbin/Data/Real/Pi/Wallis.lean @@ -110,7 +110,7 @@ theorem le_W (k : ℕ) : ((2 : ℝ) * k + 1) / (2 * k + 2) * (π / 2) ≤ W k := rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff (integral_sin_pow_pos _)] convert integral_sin_pow_succ_le (2 * k + 1) rw [integral_sin_pow (2 * k)] - simp only [sin_zero, zero_pow', Ne.def, Nat.succ_ne_zero, not_false_iff, MulZeroClass.zero_mul, + simp only [sin_zero, zero_pow, Ne.def, Nat.succ_ne_zero, not_false_iff, MulZeroClass.zero_mul, sin_pi, tsub_zero, Nat.cast_mul, Nat.cast_bit0, algebraMap.coe_one, zero_div, zero_add] #align real.wallis.le_W Real.Wallis.le_W -/ diff --git a/Mathbin/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathbin/Dynamics/Circle/RotationNumber/TranslationNumber.lean index aa2d7fa3f4..09fbace482 100644 --- a/Mathbin/Dynamics/Circle/RotationNumber/TranslationNumber.lean +++ b/Mathbin/Dynamics/Circle/RotationNumber/TranslationNumber.lean @@ -1001,7 +1001,7 @@ theorem tendsto_translation_number₀' : refine' tendsto_iff_dist_tendsto_zero.2 <| squeeze_zero (fun _ => dist_nonneg) (fun n => _) - ((tendsto_const_div_atTop_nhds_0_nat 1).comp (tendsto_add_at_top_nat 1)) + ((tendsto_const_div_atTop_nhds_zero_nat 1).comp (tendsto_add_at_top_nat 1)) dsimp have : (0 : ℝ) < n + 1 := n.cast_add_one_pos rw [Real.dist_eq, div_sub' _ _ _ (ne_of_gt this), abs_div, ← Real.dist_eq, abs_of_pos this, diff --git a/Mathbin/FieldTheory/Finite/Basic.lean b/Mathbin/FieldTheory/Finite/Basic.lean index ab0568a859..17ffb80c95 100644 --- a/Mathbin/FieldTheory/Finite/Basic.lean +++ b/Mathbin/FieldTheory/Finite/Basic.lean @@ -573,7 +573,7 @@ theorem even_card_iff_char_two : ringChar F = 2 ↔ Fintype.card F % 2 = 0 := constructor · intro hF rw [hF] - simp only [Nat.bit0_mod_two, zero_pow', Ne.def, PNat.ne_zero, not_false_iff, Nat.zero_mod] + simp only [Nat.bit0_mod_two, zero_pow, Ne.def, PNat.ne_zero, not_false_iff, Nat.zero_mod] · rw [← Nat.even_iff, Nat.even_pow] rintro ⟨hev, hnz⟩ rw [Nat.even_iff, Nat.mod_mod] at hev diff --git a/Mathbin/MeasureTheory/Covering/Besicovitch.lean b/Mathbin/MeasureTheory/Covering/Besicovitch.lean index 41bdd867bf..2aa63a597b 100644 --- a/Mathbin/MeasureTheory/Covering/Besicovitch.lean +++ b/Mathbin/MeasureTheory/Covering/Besicovitch.lean @@ -864,7 +864,7 @@ theorem exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux (μ : Measur have C : tendsto (fun n : ℕ => ((N : ℝ≥0∞) / (N + 1)) ^ n * μ s) at_top (𝓝 (0 * μ s)) := by apply ENNReal.Tendsto.mul_const _ (Or.inr (measure_lt_top μ s).Ne) - apply ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 + apply ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one rw [ENNReal.div_lt_iff, one_mul] · conv_lhs => rw [← add_zero (N : ℝ≥0∞)] exact ENNReal.add_lt_add_left (ENNReal.nat_ne_top N) zero_lt_one diff --git a/Mathbin/MeasureTheory/Covering/LiminfLimsup.lean b/Mathbin/MeasureTheory/Covering/LiminfLimsup.lean index 9b7f2eb445..27d8323bd3 100644 --- a/Mathbin/MeasureTheory/Covering/LiminfLimsup.lean +++ b/Mathbin/MeasureTheory/Covering/LiminfLimsup.lean @@ -240,7 +240,7 @@ theorem blimsup_cthickening_mul_ae_eq (p : ℕ → Prop) (s : ℕ → Set α) {M by refine' tendsto_nhds_within_iff.mpr - ⟨tendsto.if' hr tendsto_one_div_add_atTop_nhds_0_nat, eventually_of_forall fun i => _⟩ + ⟨tendsto.if' hr tendsto_one_div_add_atTop_nhds_zero_nat, eventually_of_forall fun i => _⟩ by_cases hi : 0 < r i · simp [hi, r'] · simp only [hi, r', one_div, mem_Ioi, if_false, inv_pos]; positivity diff --git a/Mathbin/MeasureTheory/Decomposition/UnsignedHahn.lean b/Mathbin/MeasureTheory/Decomposition/UnsignedHahn.lean index c8e43b728e..e19a4eb656 100644 --- a/Mathbin/MeasureTheory/Decomposition/UnsignedHahn.lean +++ b/Mathbin/MeasureTheory/Decomposition/UnsignedHahn.lean @@ -154,7 +154,7 @@ theorem hahn_decomposition [IsFiniteMeasure μ] [IsFiniteMeasure ν] : exact tendsto_const_nhds.sub <| tendsto_const_nhds.mul <| - tendsto_pow_atTop_nhds_0_of_lt_1 (le_of_lt <| half_pos <| zero_lt_one) + tendsto_pow_atTop_nhds_zero_of_lt_one (le_of_lt <| half_pos <| zero_lt_one) (half_lt_self zero_lt_one) have hd : tendsto (fun m => d (⋂ n, f m n)) at_top (𝓝 (d (⋃ m, ⋂ n, f m n))) := by diff --git a/Mathbin/MeasureTheory/Integral/CircleIntegral.lean b/Mathbin/MeasureTheory/Integral/CircleIntegral.lean index 04f985957c..41e4c64435 100644 --- a/Mathbin/MeasureTheory/Integral/CircleIntegral.lean +++ b/Mathbin/MeasureTheory/Integral/CircleIntegral.lean @@ -736,15 +736,15 @@ theorem hasSum_two_pi_I_cauchyPowerSeries_integral {f : ℂ → E} {c : ℂ} {R apply_rules [ae_strongly_measurable.smul, hf.def.1] <;> · apply Measurable.aestronglyMeasurable; measurability · simp [norm_smul, abs_of_pos hR, mul_left_comm R, mul_inv_cancel_left₀ hR.ne', mul_comm ‖_‖] - · exact eventually_of_forall fun _ _ => (summable_geometric_of_lt_1 hwR.1 hwR.2).hMul_left _ + · exact eventually_of_forall fun _ _ => (summable_geometric_of_lt_one hwR.1 hwR.2).hMul_left _ · - simpa only [tsum_mul_left, tsum_geometric_of_lt_1 hwR.1 hwR.2] using + simpa only [tsum_mul_left, tsum_geometric_of_lt_one hwR.1 hwR.2] using hf.norm.mul_continuous_on continuousOn_const · refine' eventually_of_forall fun θ hθ => HasSum.const_smul _ _ simp only [smul_smul] refine' HasSum.smul_const _ _ have : ‖w / (circleMap c R θ - c)‖ < 1 := by simpa [abs_of_pos hR] using hwR.2 - convert (hasSum_geometric_of_norm_lt_1 this).hMul_right _ + convert (hasSum_geometric_of_norm_lt_one this).hMul_right _ simp [← sub_sub, ← mul_inv, sub_mul, div_mul_cancel _ (circleMap_ne_center hR.ne')] #align has_sum_two_pi_I_cauchy_power_series_integral hasSum_two_pi_I_cauchyPowerSeries_integral -/ diff --git a/Mathbin/MeasureTheory/Integral/PeakFunction.lean b/Mathbin/MeasureTheory/Integral/PeakFunction.lean index ea04df3a2a..49207de318 100644 --- a/Mathbin/MeasureTheory/Integral/PeakFunction.lean +++ b/Mathbin/MeasureTheory/Integral/PeakFunction.lean @@ -296,7 +296,7 @@ theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_measure_ (𝓝 ((μ (v ∩ s)).toReal⁻¹ * 0)) := by apply tendsto.mul tendsto_const_nhds _; · infer_instance - apply tendsto_pow_atTop_nhds_0_of_lt_1 (div_nonneg t_pos t'_pos.le) + apply tendsto_pow_atTop_nhds_zero_of_lt_one (div_nonneg t_pos t'_pos.le) exact (div_lt_one t'_pos).2 tt' rw [MulZeroClass.mul_zero] at N refine' tendsto_uniformly_on_iff.2 fun ε εpos => _ diff --git a/Mathbin/MeasureTheory/Integral/TorusIntegral.lean b/Mathbin/MeasureTheory/Integral/TorusIntegral.lean index 3100e58c96..d892229315 100644 --- a/Mathbin/MeasureTheory/Integral/TorusIntegral.lean +++ b/Mathbin/MeasureTheory/Integral/TorusIntegral.lean @@ -206,7 +206,7 @@ notation3"∯ "(...)" in ""T("c", "R")"", "r:60:(scoped f => torusIntegral f c R #print torusIntegral_radius_zero /- theorem torusIntegral_radius_zero (hn : n ≠ 0) (f : ℂⁿ → E) (c : ℂⁿ) : ∯ x in T(c, 0), f x = 0 := by simp only [torusIntegral, Pi.zero_apply, of_real_zero, MulZeroClass.mul_zero, - MulZeroClass.zero_mul, Fin.prod_const, zero_pow' n hn, zero_smul, integral_zero] + MulZeroClass.zero_mul, Fin.prod_const, zero_pow n hn, zero_smul, integral_zero] #align torus_integral_radius_zero torusIntegral_radius_zero -/ diff --git a/Mathbin/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathbin/MeasureTheory/Measure/Lebesgue/EqHaar.lean index efaf9534f5..1a6f6cc255 100644 --- a/Mathbin/MeasureTheory/Measure/Lebesgue/EqHaar.lean +++ b/Mathbin/MeasureTheory/Measure/Lebesgue/EqHaar.lean @@ -187,7 +187,7 @@ theorem addHaar_submodule {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E obtain ⟨c, cpos, cone⟩ : ∃ c : ℝ, 0 < c ∧ c < 1 := ⟨1 / 2, by norm_num, by norm_num⟩ have A : bounded (range fun n : ℕ => c ^ n • x) := haveI : tendsto (fun n : ℕ => c ^ n • x) at_top (𝓝 ((0 : ℝ) • x)) := - (tendsto_pow_atTop_nhds_0_of_lt_1 cpos.le cone).smul_const x + (tendsto_pow_atTop_nhds_zero_of_lt_one cpos.le cone).smul_const x bounded_range_of_tendsto _ this apply add_haar_eq_zero_of_disjoint_translates μ _ A _ @@ -422,7 +422,7 @@ theorem addHaar_smul (r : ℝ) (s : Set E) : pow_zero, Subsingleton.eq_univ_of_nonempty (singleton_nonempty (0 : E))] · haveI : Nontrivial E := nontrivial_of_finrank_pos (bot_lt_iff_ne_bot.2 h) simp only [h, MulZeroClass.zero_mul, ENNReal.ofReal_zero, abs_zero, Ne.def, not_false_iff, - zero_pow', measure_singleton] + zero_pow, measure_singleton] #align measure_theory.measure.add_haar_smul MeasureTheory.Measure.addHaar_smul -/ diff --git a/Mathbin/MeasureTheory/Measure/Portmanteau.lean b/Mathbin/MeasureTheory/Measure/Portmanteau.lean index accfaa04ed..c60dae8de6 100644 --- a/Mathbin/MeasureTheory/Measure/Portmanteau.lean +++ b/Mathbin/MeasureTheory/Measure/Portmanteau.lean @@ -386,7 +386,7 @@ theorem FiniteMeasure.limsup_measure_closed_le_of_tendsto {Ω ι : Type _} {L : intro ε ε_pos μ_F_finite set δs := fun n : ℕ => (1 : ℝ) / (n + 1) with def_δs have δs_pos : ∀ n, 0 < δs n := fun n => Nat.one_div_pos_of_nat - have δs_lim : tendsto δs at_top (𝓝 0) := tendsto_one_div_add_atTop_nhds_0_nat + have δs_lim : tendsto δs at_top (𝓝 0) := tendsto_one_div_add_atTop_nhds_zero_nat have key₁ := tendsto_lintegral_thickened_indicator_of_is_closed (μ : Measure Ω) F_closed δs_pos δs_lim have room₁ : (μ : Measure Ω) F < (μ : Measure Ω) F + ε / 2 := by diff --git a/Mathbin/NumberTheory/LegendreSymbol/Basic.lean b/Mathbin/NumberTheory/LegendreSymbol/Basic.lean index 92040d2d42..6abe2b5f46 100644 --- a/Mathbin/NumberTheory/LegendreSymbol/Basic.lean +++ b/Mathbin/NumberTheory/LegendreSymbol/Basic.lean @@ -283,7 +283,7 @@ theorem eq_one_of_sq_sub_mul_sq_eq_zero' {p : ℕ} [Fact p.Prime] {a : ℤ} (ha {x y : ZMod p} (hx : x ≠ 0) (hxy : x ^ 2 - a * y ^ 2 = 0) : legendreSym p a = 1 := haveI hy : y ≠ 0 := by rintro rfl - rw [zero_pow' 2 (by norm_num), MulZeroClass.mul_zero, sub_zero, + rw [zero_pow 2 (by norm_num), MulZeroClass.mul_zero, sub_zero, pow_eq_zero_iff (by norm_num : 0 < 2)] at hxy exacts [hx hxy, inferInstance] -- why is the instance not inferred automatically? diff --git a/Mathbin/NumberTheory/Liouville/LiouvilleNumber.lean b/Mathbin/NumberTheory/Liouville/LiouvilleNumber.lean index b49336a8cf..3b64914394 100644 --- a/Mathbin/NumberTheory/Liouville/LiouvilleNumber.lean +++ b/Mathbin/NumberTheory/Liouville/LiouvilleNumber.lean @@ -162,7 +162,7 @@ theorem remainder_lt' (n : ℕ) {m : ℝ} (m1 : 1 < m) : (∑' i, (1 / m) ^ i) * (1 / m ^ (n + 1)!) := tsum_mul_right _ = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) :=-- the series if the geometric series - by rw [tsum_geometric_of_lt_1 (by positivity) mi] + by rw [tsum_geometric_of_lt_one (by positivity) mi] #align liouville_number.remainder_lt' LiouvilleNumber.remainder_lt' -/ diff --git a/Mathbin/NumberTheory/ModularForms/JacobiTheta/Basic.lean b/Mathbin/NumberTheory/ModularForms/JacobiTheta/Basic.lean index 65eb7476e5..dccd747ce8 100644 --- a/Mathbin/NumberTheory/ModularForms/JacobiTheta/Basic.lean +++ b/Mathbin/NumberTheory/ModularForms/JacobiTheta/Basic.lean @@ -70,7 +70,7 @@ theorem exists_summable_bound_exp_mul_sq {R : ℝ} (hR : 0 < R) : rwa [mul_le_mul_left_of_neg (neg_lt_zero.mpr pi_pos)] all_goals simpa only [Int.natAbs_neg, Int.natAbs_ofNat] using - summable_geometric_of_lt_1 (Real.exp_pos _).le h + summable_geometric_of_lt_one (Real.exp_pos _).le h #align exists_summable_bound_exp_mul_sq exists_summable_bound_exp_mul_sq -/ @@ -181,7 +181,7 @@ theorem norm_jacobiTheta_sub_one_le {z : ℂ} (hz : 0 < im z) : by simp_rw [pow_succ, div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)] exact - hasSum_geometric_of_lt_1 (exp_pos (-π * z.im)).le + hasSum_geometric_of_lt_one (exp_pos (-π * z.im)).le (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hz) have aux : Summable fun n : ℕ => ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ := Summable.of_nonneg_of_le (fun n => norm_nonneg _) this s.summable diff --git a/Mathbin/NumberTheory/Padics/Hensel.lean b/Mathbin/NumberTheory/Padics/Hensel.lean index e40bde40cd..b54bfeace2 100644 --- a/Mathbin/NumberTheory/Padics/Hensel.lean +++ b/Mathbin/NumberTheory/Padics/Hensel.lean @@ -337,7 +337,7 @@ private theorem bound' : Tendsto (fun n : ℕ => ‖F.derivative.eval a‖ * T ^ rw [← MulZeroClass.mul_zero ‖F.derivative.eval a‖] exact tendsto_const_nhds.mul - (tendsto.comp (tendsto_pow_atTop_nhds_0_of_lt_1 (norm_nonneg _) (T_lt_one hnorm)) + (tendsto.comp (tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) (T_lt_one hnorm)) (Nat.tendsto_pow_atTop_atTop_of_one_lt (by norm_num))) private theorem bound : diff --git a/Mathbin/NumberTheory/ZetaValues.lean b/Mathbin/NumberTheory/ZetaValues.lean index c8652fa278..5d1a2768a6 100644 --- a/Mathbin/NumberTheory/ZetaValues.lean +++ b/Mathbin/NumberTheory/ZetaValues.lean @@ -169,7 +169,7 @@ theorem bernoulliFourierCoeff_eq {k : ℕ} (hk : k ≠ 0) (n : ℤ) : by rcases eq_or_ne n 0 with (rfl | hn) · - rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, MulZeroClass.mul_zero, zero_pow' _ hk, + rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, MulZeroClass.mul_zero, zero_pow _ hk, div_zero] refine' Nat.le_induction _ (fun k hk h'k => _) k (nat.one_le_iff_ne_zero.mpr hk) · rw [bernoulliFourierCoeff_recurrence 1 hn] diff --git a/Mathbin/Probability/Kernel/CondCdf.lean b/Mathbin/Probability/Kernel/CondCdf.lean index 896325e49d..f4e89ed238 100644 --- a/Mathbin/Probability/Kernel/CondCdf.lean +++ b/Mathbin/Probability/Kernel/CondCdf.lean @@ -159,10 +159,10 @@ theorem ENNReal.ofReal_cinfi (f : α → ℝ) [Nonempty α] : #align ennreal.of_real_cinfi ENNReal.ofReal_cinfi -/ -#print lintegral_iInf_directed_of_measurable /- +#print MeasureTheory.lintegral_iInf_directed_of_measurable /- -- todo: move to measure_theory/measurable_space /-- Monotone convergence for an infimum over a directed family and indexed by a countable type -/ -theorem lintegral_iInf_directed_of_measurable {mα : MeasurableSpace α} [Countable β] +theorem MeasureTheory.lintegral_iInf_directed_of_measurable {mα : MeasurableSpace α} [Countable β] {f : β → α → ℝ≥0∞} {μ : Measure α} (hμ : μ ≠ 0) (hf : ∀ b, Measurable (f b)) (hf_int : ∀ b, ∫⁻ a, f b a ∂μ ≠ ∞) (h_directed : Directed (· ≥ ·) f) : ∫⁻ a, ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ a, f b a ∂μ := @@ -191,7 +191,7 @@ theorem lintegral_iInf_directed_of_measurable {mα : MeasurableSpace α} [Counta refine' le_antisymm (le_iInf fun b => _) (le_iInf fun n => _) · exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b) · exact iInf_le (fun b => ∫⁻ a, f b a ∂μ) _ -#align lintegral_infi_directed_of_measurable lintegral_iInf_directed_of_measurable +#align lintegral_infi_directed_of_measurable MeasureTheory.lintegral_iInf_directed_of_measurable -/ #print isPiSystem_Iic /- @@ -1125,7 +1125,7 @@ theorem set_lintegral_condCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x rw [h] simp_rw [ENNReal.ofReal_cinfi] have h_coe : ∀ b : { r' : ℚ // x < ↑r' }, (b : ℝ) = ((b : ℚ) : ℝ) := fun _ => by congr - rw [lintegral_iInf_directed_of_measurable hρ_zero fun q : { r' : ℚ // x < ↑r' } => + rw [MeasureTheory.lintegral_iInf_directed_of_measurable hρ_zero fun q : { r' : ℚ // x < ↑r' } => (measurable_cond_cdf ρ q).ennreal_ofReal] rotate_left · intro b diff --git a/Mathbin/Probability/Moments.lean b/Mathbin/Probability/Moments.lean index 38c7130702..8a56ba33f1 100644 --- a/Mathbin/Probability/Moments.lean +++ b/Mathbin/Probability/Moments.lean @@ -67,7 +67,7 @@ def centralMoment (X : Ω → ℝ) (p : ℕ) (μ : Measure Ω) : ℝ := #print ProbabilityTheory.moment_zero /- @[simp] theorem moment_zero (hp : p ≠ 0) : moment 0 p μ = 0 := by - simp only [moment, hp, zero_pow', Ne.def, not_false_iff, Pi.zero_apply, integral_const, + simp only [moment, hp, zero_pow, Ne.def, not_false_iff, Pi.zero_apply, integral_const, Algebra.id.smul_eq_mul, MulZeroClass.mul_zero] #align probability_theory.moment_zero ProbabilityTheory.moment_zero -/ @@ -76,7 +76,7 @@ theorem moment_zero (hp : p ≠ 0) : moment 0 p μ = 0 := by @[simp] theorem centralMoment_zero (hp : p ≠ 0) : centralMoment 0 p μ = 0 := by simp only [central_moment, hp, Pi.zero_apply, integral_const, Algebra.id.smul_eq_mul, - MulZeroClass.mul_zero, zero_sub, Pi.pow_apply, Pi.neg_apply, neg_zero, zero_pow', Ne.def, + MulZeroClass.mul_zero, zero_sub, Pi.pow_apply, Pi.neg_apply, neg_zero, zero_pow, Ne.def, not_false_iff] #align probability_theory.central_moment_zero ProbabilityTheory.centralMoment_zero -/ diff --git a/Mathbin/Probability/StrongLaw.lean b/Mathbin/Probability/StrongLaw.lean index 889eda0809..85cddf9db7 100644 --- a/Mathbin/Probability/StrongLaw.lean +++ b/Mathbin/Probability/StrongLaw.lean @@ -167,7 +167,7 @@ theorem moment_truncation_eq_intervalIntegral (hf : AEStronglyMeasurable f μ) { have M : MeasurableSet (Set.Ioc (-A) A) := measurableSet_Ioc change ∫ x, (fun z => indicator (Set.Ioc (-A) A) id z ^ n) (f x) ∂μ = _ rw [← integral_map hf.ae_measurable, intervalIntegral.integral_of_le, ← integral_indicator M] - · simp only [indicator, zero_pow' _ hn, id.def, ite_pow] + · simp only [indicator, zero_pow _ hn, id.def, ite_pow] · linarith · exact ((measurable_id.indicator M).pow_const n).AEStronglyMeasurable #align probability_theory.moment_truncation_eq_interval_integral ProbabilityTheory.moment_truncation_eq_intervalIntegral @@ -184,11 +184,11 @@ theorem moment_truncation_eq_intervalIntegral_of_nonneg (hf : AEStronglyMeasurab change ∫ x, (fun z => indicator (Set.Ioc 0 A) id z ^ n) (f x) ∂μ = _ rcases le_or_lt 0 A with (hA | hA) · rw [← integral_map hf.ae_measurable, intervalIntegral.integral_of_le hA, ← integral_indicator M] - · simp only [indicator, zero_pow' _ hn, id.def, ite_pow] + · simp only [indicator, zero_pow _ hn, id.def, ite_pow] · exact ((measurable_id.indicator M).pow_const n).AEStronglyMeasurable · rw [← integral_map hf.ae_measurable, intervalIntegral.integral_of_ge hA.le, ← integral_indicator M'] - · simp only [Set.Ioc_eq_empty_of_le hA.le, zero_pow' _ hn, Set.indicator_empty, integral_zero, + · simp only [Set.Ioc_eq_empty_of_le hA.le, zero_pow _ hn, Set.indicator_empty, integral_zero, zero_eq_neg] apply integral_eq_zero_of_ae have : ∀ᵐ x ∂measure.map f μ, (0 : ℝ) ≤ x := @@ -197,7 +197,7 @@ theorem moment_truncation_eq_intervalIntegral_of_nonneg (hf : AEStronglyMeasurab simp only [indicator, Set.mem_Ioc, Pi.zero_apply, ite_eq_right_iff, and_imp] intro h'x h''x have : x = 0 := by linarith - simp [this, zero_pow' _ hn] + simp [this, zero_pow _ hn] · exact ((measurable_id.indicator M).pow_const n).AEStronglyMeasurable #align probability_theory.moment_truncation_eq_interval_integral_of_nonneg ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg -/ @@ -564,7 +564,7 @@ theorem strong_law_aux1 {c : ℝ} (c_one : 1 < c) {ε : ℝ} (εpos : 0 < ε) : by apply sum_le_sum fun j hj => _ rcases@eq_zero_or_pos _ _ j with (rfl | hj) - · simp only [Y, Nat.cast_zero, zero_pow', Ne.def, bit0_eq_zero, Nat.one_ne_zero, + · simp only [Y, Nat.cast_zero, zero_pow, Ne.def, bit0_eq_zero, Nat.one_ne_zero, not_false_iff, div_zero, MulZeroClass.zero_mul] simp only [Nat.cast_zero, truncation_zero, variance_zero, MulZeroClass.mul_zero] apply mul_le_mul_of_nonneg_right _ (variance_nonneg _ _) diff --git a/Mathbin/RingTheory/PowerSeries/Basic.lean b/Mathbin/RingTheory/PowerSeries/Basic.lean index 9f17d55749..d0c948d00d 100644 --- a/Mathbin/RingTheory/PowerSeries/Basic.lean +++ b/Mathbin/RingTheory/PowerSeries/Basic.lean @@ -1951,7 +1951,7 @@ theorem rescale_zero : rescale 0 = (C R).comp (constantCoeff R) := PowerSeries.coeff_mk _ _, coeff_C] split_ifs · simp only [h, one_mul, coeff_zero_eq_constant_coeff, pow_zero] - · rw [zero_pow' n h, MulZeroClass.zero_mul] + · rw [zero_pow n h, MulZeroClass.zero_mul] #align power_series.rescale_zero PowerSeries.rescale_zero -/ diff --git a/Mathbin/RingTheory/UniqueFactorizationDomain.lean b/Mathbin/RingTheory/UniqueFactorizationDomain.lean index 6de16715b7..666dfc4ac9 100644 --- a/Mathbin/RingTheory/UniqueFactorizationDomain.lean +++ b/Mathbin/RingTheory/UniqueFactorizationDomain.lean @@ -2194,7 +2194,7 @@ theorem eq_pow_of_mul_eq_pow [Nontrivial α] {a b c : Associates α} (ha : a ≠ rw [h] apply dvd_count_pow _ hp rintro rfl - rw [zero_pow' _ hk0] at h + rw [zero_pow _ hk0] at h cases mul_eq_zero.mp h <;> contradiction #align associates.eq_pow_of_mul_eq_pow Associates.eq_pow_of_mul_eq_pow -/ diff --git a/Mathbin/RingTheory/WittVector/MulCoeff.lean b/Mathbin/RingTheory/WittVector/MulCoeff.lean index 7de0aa05df..efb8f1fd31 100644 --- a/Mathbin/RingTheory/WittVector/MulCoeff.lean +++ b/Mathbin/RingTheory/WittVector/MulCoeff.lean @@ -294,7 +294,7 @@ theorem peval_polyOfInterest' (n : ℕ) (x y : 𝕎 k) : rw [peval_poly_of_interest] have : (p : k) = 0 := CharP.cast_eq_zero k p simp only [this, add_zero, MulZeroClass.zero_mul, Nat.succ_ne_zero, Ne.def, not_false_iff, - zero_pow'] + zero_pow] have sum_zero_pow_mul_pow_p : ∀ y : 𝕎 k, ∑ x : ℕ in range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1) := diff --git a/Mathbin/Topology/MetricSpace/Antilipschitz.lean b/Mathbin/Topology/MetricSpace/Antilipschitz.lean index a491766568..104353d51a 100644 --- a/Mathbin/Topology/MetricSpace/Antilipschitz.lean +++ b/Mathbin/Topology/MetricSpace/Antilipschitz.lean @@ -303,7 +303,7 @@ protected theorem properSpace {α : Type _} [MetricSpace α] {K : ℝ≥0} {f : (hK : AntilipschitzWith K f) (f_cont : Continuous f) (hf : Function.Surjective f) : ProperSpace β := by - apply properSpace_of_compact_closedBall_of_le 0 fun x₀ r hr => _ + apply ProperSpace.of_isCompact_closedBall_of_le 0 fun x₀ r hr => _ let K := f ⁻¹' closed_ball x₀ r have A : IsClosed K := is_closed_ball.preimage f_cont have B : bounded K := hK.bounded_preimage bounded_closed_ball diff --git a/Mathbin/Topology/MetricSpace/Basic.lean b/Mathbin/Topology/MetricSpace/Basic.lean index b37a5de11d..9c8b3ab95e 100644 --- a/Mathbin/Topology/MetricSpace/Basic.lean +++ b/Mathbin/Topology/MetricSpace/Basic.lean @@ -2993,10 +2993,10 @@ theorem tendsto_dist_left_cocompact_atTop [ProperSpace α] (x : α) : #align tendsto_dist_left_cocompact_at_top tendsto_dist_left_cocompact_atTop -/ -#print properSpace_of_compact_closedBall_of_le /- +#print ProperSpace.of_isCompact_closedBall_of_le /- /-- If all closed balls of large enough radius are compact, then the space is proper. Especially useful when the lower bound for the radius is 0. -/ -theorem properSpace_of_compact_closedBall_of_le (R : ℝ) +theorem ProperSpace.of_isCompact_closedBall_of_le (R : ℝ) (h : ∀ x : α, ∀ r, R ≤ r → IsCompact (closedBall x r)) : ProperSpace α := ⟨by intro x r @@ -3009,7 +3009,7 @@ theorem properSpace_of_compact_closedBall_of_le (R : ℝ) exact closed_ball_subset_closed_ball (le_of_lt (not_le.1 hr)) rw [this] exact (h x R le_rfl).inter_right is_closed_ball⟩ -#align proper_space_of_compact_closed_ball_of_le properSpace_of_compact_closedBall_of_le +#align proper_space_of_compact_closed_ball_of_le ProperSpace.of_isCompact_closedBall_of_le -/ #print proper_of_compact /- @@ -3065,7 +3065,7 @@ instance prod_properSpace {α : Type _} {β : Type _} [PseudoMetricSpace α] [Ps instance pi_properSpace {π : β → Type _} [Fintype β] [∀ b, PseudoMetricSpace (π b)] [h : ∀ b, ProperSpace (π b)] : ProperSpace (∀ b, π b) := by - refine' properSpace_of_compact_closedBall_of_le 0 fun x r hr => _ + refine' ProperSpace.of_isCompact_closedBall_of_le 0 fun x r hr => _ rw [closedBall_pi _ hr] apply isCompact_univ_pi fun b => _ apply (h b).isCompact_closedBall diff --git a/Mathbin/Topology/MetricSpace/Closeds.lean b/Mathbin/Topology/MetricSpace/Closeds.lean index 7066269014..4d4d0e27b1 100644 --- a/Mathbin/Topology/MetricSpace/Closeds.lean +++ b/Mathbin/Topology/MetricSpace/Closeds.lean @@ -200,7 +200,8 @@ instance Closeds.completeSpace [CompleteSpace α] : CompleteSpace (Closeds α) : refine' tendsto_at_top.2 fun ε εpos => _ have : tendsto (fun n => 2 * B n) at_top (𝓝 (2 * 0)) := ENNReal.Tendsto.const_mul - (ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 <| by simp [ENNReal.one_lt_two]) (Or.inr <| by simp) + (ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one <| by simp [ENNReal.one_lt_two]) + (Or.inr <| by simp) rw [MulZeroClass.mul_zero] at this obtain ⟨N, hN⟩ : ∃ N, ∀ b ≥ N, ε > 2 * B b exact ((tendsto_order.1 this).2 ε εpos).exists_forall_of_atTop diff --git a/Mathbin/Topology/MetricSpace/HausdorffDistance.lean b/Mathbin/Topology/MetricSpace/HausdorffDistance.lean index 2f6e112d53..2cd76970bb 100644 --- a/Mathbin/Topology/MetricSpace/HausdorffDistance.lean +++ b/Mathbin/Topology/MetricSpace/HausdorffDistance.lean @@ -275,7 +275,7 @@ theorem IsOpen.exists_iUnion_isClosed {U : Set α} (hU : IsOpen U) : rw [mem_iff_inf_edist_zero_of_closed hU.is_closed_compl] at this have B : 0 < inf_edist x (Uᶜ) := by simpa [pos_iff_ne_zero] using this have : Filter.Tendsto (fun n => a ^ n) at_top (𝓝 0) := - ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 a_lt_one + ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one a_lt_one rcases((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩ simp only [mem_Union, mem_Ici, mem_preimage] exact ⟨n, hn.le⟩ diff --git a/Mathbin/Topology/MetricSpace/PiNat.lean b/Mathbin/Topology/MetricSpace/PiNat.lean index 6abd200f0e..c4a4c73e45 100644 --- a/Mathbin/Topology/MetricSpace/PiNat.lean +++ b/Mathbin/Topology/MetricSpace/PiNat.lean @@ -943,7 +943,8 @@ theorem exists_nat_nat_continuous_surjective_of_completeSpace (α : Type _) [Met dist_triangle_right _ _ _ _ ≤ (1 / 2) ^ n + (1 / 2) ^ n := add_le_add (A ⟨x, I⟩ n) (hx n) have L : tendsto (fun n : ℕ => (1 / 2 : ℝ) ^ n + (1 / 2) ^ n) at_top (𝓝 (0 + 0)) := - (tendsto_pow_atTop_nhds_0_of_lt_1 I0.le I1).add (tendsto_pow_atTop_nhds_0_of_lt_1 I0.le I1) + (tendsto_pow_atTop_nhds_zero_of_lt_one I0.le I1).add + (tendsto_pow_atTop_nhds_zero_of_lt_one I0.le I1) rw [add_zero] at L exact ge_of_tendsto' L J have s_closed : IsClosed s := @@ -953,7 +954,7 @@ theorem exists_nat_nat_continuous_surjective_of_completeSpace (α : Type _) [Met have L : tendsto (fun n : ℕ => diam (closed_ball (u (x n)) ((1 / 2) ^ n))) at_top (𝓝 0) := by have : tendsto (fun n : ℕ => (2 : ℝ) * (1 / 2) ^ n) at_top (𝓝 (2 * 0)) := - (tendsto_pow_atTop_nhds_0_of_lt_1 I0.le I1).const_mul _ + (tendsto_pow_atTop_nhds_zero_of_lt_one I0.le I1).const_mul _ rw [MulZeroClass.mul_zero] at this exact squeeze_zero (fun n => diam_nonneg) (fun n => diam_closed_ball (pow_nonneg I0.le _)) this diff --git a/Mathbin/Topology/MetricSpace/Polish.lean b/Mathbin/Topology/MetricSpace/Polish.lean index d6f4c4b196..c365818891 100644 --- a/Mathbin/Topology/MetricSpace/Polish.lean +++ b/Mathbin/Topology/MetricSpace/Polish.lean @@ -400,7 +400,7 @@ theorem TopologicalSpace.Opens.CompleteCopy.instCompleteSpace [CompleteSpace α] by apply cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => _) _ · exact (dist_le_dist_complete_copy (u n) (u m)).trans (hu N n m hNn hNm).le - · exact tendsto_pow_atTop_nhds_0_of_lt_1 (by norm_num) (by norm_num) + · exact tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num) obtain ⟨x, xlim⟩ : ∃ x, tendsto (fun n => (u n).1) at_top (𝓝 x) := haveI : Nonempty α := ⟨(u 0).1⟩ ⟨_, A.tendsto_lim⟩ diff --git a/Mathbin/Topology/TietzeExtension.lean b/Mathbin/Topology/TietzeExtension.lean index 3109804b79..910ad337d7 100644 --- a/Mathbin/Topology/TietzeExtension.lean +++ b/Mathbin/Topology/TietzeExtension.lean @@ -144,7 +144,7 @@ theorem exists_extension_norm_eq_of_closedEmbedding' (f : X →ᵇ ℝ) (e : C(X refine' tendsto_nhds_unique this (tendsto_iff_dist_tendsto_zero.2 _) refine' squeeze_zero (fun _ => dist_nonneg) hgf _ rw [← MulZeroClass.zero_mul ‖f‖] - refine' (tendsto_pow_atTop_nhds_0_of_lt_1 _ _).mul tendsto_const_nhds <;> norm_num1 + refine' (tendsto_pow_atTop_nhds_zero_of_lt_one _ _).mul tendsto_const_nhds <;> norm_num1 refine' ⟨limUnder at_top g, le_antisymm _ _, hge⟩ · rw [← dist_zero_left, ← g0] refine' diff --git a/lake-manifest.json b/lake-manifest.json index 4888067f75..415b61e99c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "a11bdfc39e95fa5b09e06638a43bd8bd2eddce12", + "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "24a4e8fea81999723bfc38bebf7adc86c2f26c6c", + "rev": "cebd10ba6d22457e364ba03320cfd9fc7511e520", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3", + "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,19 +58,19 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "ec497096ba311298c5254c6cdcdad0281e48e04f", + "rev": "2e5fa833c10558469fb2b0f16318514f54ec9a9e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "ec497096ba311298c5254c6cdcdad0281e48e04f", + "inputRev": "2e5fa833c10558469fb2b0f16318514f54ec9a9e", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/lean3port.git", "type": "git", "subDir": null, - "rev": "0fcdd06a2ae8a2a6b78a58fb93312f66918c317d", + "rev": "eb4b6cf1b423fe815baf759cbc3d39d2c7b5e21d", "name": "lean3port", "manifestFile": "lake-manifest.json", - "inputRev": "0fcdd06a2ae8a2a6b78a58fb93312f66918c317d", + "inputRev": "eb4b6cf1b423fe815baf759cbc3d39d2c7b5e21d", "inherited": false, "configFile": "lakefile.lean"}], "name": "mathlib3port", diff --git a/lakefile.lean b/lakefile.lean index bc2a2ded7a..5b884d76d6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,7 +4,7 @@ open Lake DSL System -- Usually the `tag` will be of the form `nightly-2021-11-22`. -- If you would like to use an artifact from a PR build, -- it will be of the form `pr-branchname-sha`. -def tag : String := "nightly-2024-02-01-06" +def tag : String := "nightly-2024-02-02-06" def releaseRepo : String := "leanprover-community/mathport" def oleanTarName : String := "mathlib3-binport.tar.gz" @@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do untarReleaseArtifact releaseRepo tag oleanTarName libDir return .nil -require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"0fcdd06a2ae8a2a6b78a58fb93312f66918c317d" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"eb4b6cf1b423fe815baf759cbc3d39d2c7b5e21d" @[default_target] lean_lib Mathbin where diff --git a/lean-toolchain b/lean-toolchain index 3f21e50bd4..bd59abf4ae 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.5.0-rc1 +leanprover/lean4:v4.5.0