chore(algebra/order/field/basic): Rename pow_minus_two_nonneg (#18591)

YaelDillies · YaelDillies · commit acb3d204d4ee · 2023-03-16T13:33:54.000Z
Rename `pow_minus_two_nonneg` to `zpow_neg_two_nonneg` and move it to `algebra.order.field.power`.
diff --git a/src/algebra/order/field/basic.lean b/src/algebra/order/field/basic.lean
@@ -470,7 +470,7 @@ lemma strict_mono.div_const {β : Type*} [preorder β] {f : β → α} (hf : str
 by simpa only [div_eq_mul_inv] using hf.mul_const (inv_pos.2 hc)
 
 @[priority 100] -- see Note [lower instance priority]
-instance linear_ordered_field.to_densely_ordered : densely_ordered α :=
+instance linear_ordered_semifield.to_densely_ordered : densely_ordered α :=
 { dense := λ a₁ a₂ h, ⟨(a₁ + a₂) / 2,
   calc a₁ = (a₁ + a₁) / 2 : (add_self_div_two a₁).symm
       ... < (a₁ + a₂) / 2 : div_lt_div_of_lt zero_lt_two (add_lt_add_left h _),
@@ -810,12 +810,4 @@ lemma abs_inv (a : α) : |a⁻¹| = (|a|)⁻¹ := map_inv₀ (abs_hom : α →*
 lemma abs_div (a b : α) : |a / b| = |a| / |b| := map_div₀ (abs_hom : α →*₀ α) a b
 lemma abs_one_div (a : α) : |1 / a| = 1 / |a| := by rw [abs_div, abs_one]
 
-lemma pow_minus_two_nonneg : 0 ≤ a^(-2 : ℤ) :=
-begin
-  simp only [inv_nonneg, zpow_neg],
-  change 0 ≤ a ^ ((2 : ℕ) : ℤ),
-  rw zpow_coe_nat,
-  apply sq_nonneg,
-end
-
 end
diff --git a/src/algebra/order/field/power.lean b/src/algebra/order/field/power.lean
@@ -98,6 +98,7 @@ lemma zpow_bit0_nonneg (a : α) (n : ℤ) : 0 ≤ a ^ bit0 n :=
 (mul_self_nonneg _).trans_eq $ (zpow_bit0 _ _).symm
 
 lemma zpow_two_nonneg (a : α) : 0 ≤ a ^ (2 : ℤ) := zpow_bit0_nonneg _ _
+lemma zpow_neg_two_nonneg (a : α) : 0 ≤ a ^ (-2 : ℤ) := zpow_bit0_nonneg _ (-1)
 
 lemma zpow_bit0_pos (h : a ≠ 0) (n : ℤ) : 0 < a ^ bit0 n :=
 (zpow_bit0_nonneg a n).lt_of_ne (zpow_ne_zero _ h).symm
diff --git a/src/analysis/special_functions/bernstein.lean b/src/analysis/special_functions/bernstein.lean
@@ -228,7 +228,7 @@ begin
   have npos : 0 < (n:ℝ) := by exact_mod_cast npos',
   -- Two easy inequalities we'll need later:
   have w₁ : 0 ≤ 2 * ‖f‖ := mul_nonneg (by norm_num) (norm_nonneg f),
-  have w₂ : 0 ≤ 2 * ‖f‖ * δ^(-2 : ℤ) := mul_nonneg w₁ pow_minus_two_nonneg,
+  have w₂ : 0 ≤ 2 * ‖f‖ * δ^(-2 : ℤ) := mul_nonneg w₁ (zpow_neg_two_nonneg _),
   -- As `[0,1]` is compact, it suffices to check the inequality pointwise.
   rw (continuous_map.norm_lt_iff _ h),
   intro x,
@@ -293,7 +293,7 @@ begin
                                   : mul_le_mul_of_nonneg_left
                                       (finset.sum_le_univ_sum_of_nonneg
                                         (λ k, mul_nonneg
-                                          (mul_nonneg pow_minus_two_nonneg (sq_nonneg _))
+                                          (mul_nonneg (zpow_neg_two_nonneg _) (sq_nonneg _))
                                           bernstein_nonneg)) w₁
         ... = (2 * ‖f‖) * δ^(-2 : ℤ) * ∑ k : fin (n+1), (x - k/ₙ)^2 * bernstein n k x
                                   : by conv_rhs
