feat: NNReal.coe_pos_iff_ne_zero

leanprover-community · Oct 19, 2024 · 8c84091 · 8c84091
1 parent 0d932ab
commit 8c84091
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 4 deletions.
diff --git a/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean b/Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
@@ -535,7 +535,8 @@ theorem eLpNorm_le_eLpNorm_fderiv_of_eq_inner  {u : E → F'}
   by_cases h3u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ = 0
   · rw [eLpNorm_nnreal_eq_lintegral h0p', h3u, ENNReal.zero_rpow_of_pos] <;> positivity
   have h4u : ∫⁻ x, ‖u x‖₊ ^ (p' : ℝ) ∂μ ≠ ∞ := by
-    refine lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top (pos_iff_ne_zero.mpr h0p') ?_ |>.ne
+    refine lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top (NNReal.coe_pos_iff_ne_zero.mpr h0p') ?_
+      |>.ne
     dsimp only
     rw [NNReal.val_eq_coe, ← eLpNorm_nnreal_eq_eLpNorm' h0p']
     exact hu.continuous.memℒp_of_hasCompactSupport (μ := μ) h2u |>.eLpNorm_lt_top

diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@@ -79,7 +79,7 @@ theorem one_rpow (x : ℝ) : (1 : ℝ≥0) ^ x = 1 :=
   NNReal.eq <| Real.one_rpow _
 
 theorem rpow_add {x : ℝ≥0} (hx : x ≠ 0) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z :=
-  NNReal.eq <| Real.rpow_add (pos_iff_ne_zero.2 hx) _ _
+  NNReal.eq <| Real.rpow_add (NNReal.coe_pos_iff_ne_zero.mpr hx) _ _
 
 theorem rpow_add' (h : y + z ≠ 0) (x : ℝ≥0) : x ^ (y + z) = x ^ y * x ^ z :=
   NNReal.eq <| Real.rpow_add' x.2 h
@@ -146,7 +146,7 @@ lemma rpow_mul_intCast (x : ℝ≥0) (y : ℝ) (n : ℤ) : x ^ (y * n) = (x ^ y)
 theorem rpow_neg_one (x : ℝ≥0) : x ^ (-1 : ℝ) = x⁻¹ := by simp [rpow_neg]
 
 theorem rpow_sub {x : ℝ≥0} (hx : x ≠ 0) (y z : ℝ) : x ^ (y - z) = x ^ y / x ^ z :=
-  NNReal.eq <| Real.rpow_sub (pos_iff_ne_zero.2 hx) y z
+  NNReal.eq <| Real.rpow_sub (NNReal.coe_pos_iff_ne_zero.mpr hx) y z
 
 theorem rpow_sub' (h : y - z ≠ 0) (x : ℝ≥0) : x ^ (y - z) = x ^ y / x ^ z :=
   NNReal.eq <| Real.rpow_sub' x.2 h

diff --git a/Mathlib/Data/NNReal/Basic.lean b/Mathlib/Data/NNReal/Basic.lean
@@ -336,6 +336,8 @@ noncomputable example : LinearOrder ℝ≥0 := by infer_instance
 
 @[bound] private alias ⟨_, Bound.coe_pos_of_pos⟩ := coe_pos
 
+lemma coe_pos_iff_ne_zero : (0 : ℝ) < r ↔ r ≠ 0 := coe_pos.trans pos_iff_ne_zero
+
 @[simp, norm_cast] lemma one_le_coe : 1 ≤ (r : ℝ) ↔ 1 ≤ r := by rw [← coe_le_coe, coe_one]
 @[simp, norm_cast] lemma one_lt_coe : 1 < (r : ℝ) ↔ 1 < r := by rw [← coe_lt_coe, coe_one]
 @[simp, norm_cast] lemma coe_le_one : (r : ℝ) ≤ 1 ↔ r ≤ 1 := by rw [← coe_le_coe, coe_one]

diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -139,7 +139,7 @@ alias lintegral_rpow_nnnorm_eq_rpow_snorm' := lintegral_rpow_nnnorm_eq_rpow_eLpN
 lemma eLpNorm_nnreal_pow_eq_lintegral {f : α → F} {p : ℝ≥0} (hp : p ≠ 0) :
     eLpNorm f p μ ^ (p : ℝ) = ∫⁻ x, ‖f x‖₊ ^ (p : ℝ) ∂μ := by
   simp [eLpNorm_eq_eLpNorm' (by exact_mod_cast hp) ENNReal.coe_ne_top,
-    lintegral_rpow_nnnorm_eq_rpow_eLpNorm' (show 0 < (p : ℝ) from pos_iff_ne_zero.mpr hp)]
+    lintegral_rpow_nnnorm_eq_rpow_eLpNorm' (NNReal.coe_pos_iff_ne_zero.mpr hp)]
 
 @[deprecated (since := "2024-07-27")]
 alias snorm_nnreal_pow_eq_lintegral := eLpNorm_nnreal_pow_eq_lintegral