diff --git a/Mathlib.lean b/Mathlib.lean
index 4a43a773e7dbb..2c50da983709f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1992,7 +1992,7 @@ import Mathlib.Data.Rbtree.MinMax
 import Mathlib.Data.Real.Archimedean
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.Cardinality
-import Mathlib.Data.Real.ConjugateExponents
+import Mathlib.Data.Real.ConjExponents
 import Mathlib.Data.Real.ENatENNReal
 import Mathlib.Data.Real.EReal
 import Mathlib.Data.Real.GoldenRatio
diff --git a/Mathlib/Analysis/InnerProductSpace/l2Space.lean b/Mathlib/Analysis/InnerProductSpace/l2Space.lean
index 94b3354377dc0..de14ea6abd97c 100644
--- a/Mathlib/Analysis/InnerProductSpace/l2Space.lean
+++ b/Mathlib/Analysis/InnerProductSpace/l2Space.lean
@@ -110,7 +110,7 @@ namespace lp
 theorem summable_inner (f g : lp G 2) : Summable fun i => ⟪f i, g i⟫ := by
   -- Apply the Direct Comparison Test, comparing with ∑' i, ‖f i‖ * ‖g i‖ (summable by Hölder)
   refine' .of_norm_bounded (fun i => ‖f i‖ * ‖g i‖) (lp.summable_mul _ f g) _
-  · rw [Real.isConjugateExponent_iff] <;> norm_num
+  · rw [Real.isConjExponent_iff]; norm_num
   intro i
   -- Then apply Cauchy-Schwarz pointwise
   exact norm_inner_le_norm (𝕜 := 𝕜) _ _
diff --git a/Mathlib/Analysis/MeanInequalities.lean b/Mathlib/Analysis/MeanInequalities.lean
index 69c520afbe8e6..dd68b141d2ad8 100644
--- a/Mathlib/Analysis/MeanInequalities.lean
+++ b/Mathlib/Analysis/MeanInequalities.lean
@@ -6,7 +6,7 @@ Authors: Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne
 import Mathlib.Analysis.Convex.Jensen
 import Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import Mathlib.Data.Real.ConjugateExponents
+import Mathlib.Data.Real.ConjExponents
 
 #align_import analysis.mean_inequalities from "leanprover-community/mathlib"@"8f9fea08977f7e450770933ee6abb20733b47c92"
 
@@ -261,14 +261,14 @@ namespace Real
 
 /-- Young's inequality, a version for nonnegative real numbers. -/
 theorem young_inequality_of_nonneg {a b p q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b)
-    (hpq : p.IsConjugateExponent q) : a * b ≤ a ^ p / p + b ^ q / q := by
+    (hpq : p.IsConjExponent q) : a * b ≤ a ^ p / p + b ^ q / q := by
   simpa [← rpow_mul, ha, hb, hpq.ne_zero, hpq.symm.ne_zero, _root_.div_eq_inv_mul] using
     geom_mean_le_arith_mean2_weighted hpq.inv_nonneg hpq.symm.inv_nonneg
       (rpow_nonneg ha p) (rpow_nonneg hb q) hpq.inv_add_inv_conj
 #align real.young_inequality_of_nonneg Real.young_inequality_of_nonneg
 
 /-- Young's inequality, a version for arbitrary real numbers. -/
-theorem young_inequality (a b : ℝ) {p q : ℝ} (hpq : p.IsConjugateExponent q) :
+theorem young_inequality (a b : ℝ) {p q : ℝ} (hpq : p.IsConjExponent q) :
     a * b ≤ |a| ^ p / p + |b| ^ q / q :=
   calc
     a * b ≤ |a * b| := le_abs_self (a * b)
@@ -283,17 +283,15 @@ namespace NNReal
 
 /-- Young's inequality, `ℝ≥0` version. We use `{p q : ℝ≥0}` in order to avoid constructing
 witnesses of `0 ≤ p` and `0 ≤ q` for the denominators.  -/
-theorem young_inequality (a b : ℝ≥0) {p q : ℝ≥0} (hp : 1 < p) (hpq : p⁻¹ + q⁻¹ = 1) :
+theorem young_inequality (a b : ℝ≥0) {p q : ℝ≥0} (hpq : p.IsConjExponent q) :
     a * b ≤ a ^ (p : ℝ) / p + b ^ (q : ℝ) / q :=
-  Real.young_inequality_of_nonneg a.coe_nonneg b.coe_nonneg ⟨hp, NNReal.coe_inj.2 hpq⟩
+  Real.young_inequality_of_nonneg a.coe_nonneg b.coe_nonneg hpq.coe
 #align nnreal.young_inequality NNReal.young_inequality
 
 /-- Young's inequality, `ℝ≥0` version with real conjugate exponents. -/
-theorem young_inequality_real (a b : ℝ≥0) {p q : ℝ} (hpq : p.IsConjugateExponent q) :
+theorem young_inequality_real (a b : ℝ≥0) {p q : ℝ} (hpq : p.IsConjExponent q) :
     a * b ≤ a ^ p / Real.toNNReal p + b ^ q / Real.toNNReal q := by
-  nth_rw 1 [← Real.coe_toNNReal p hpq.nonneg]
-  nth_rw 1 [← Real.coe_toNNReal q hpq.symm.nonneg]
-  exact young_inequality a b hpq.one_lt_nnreal hpq.inv_add_inv_conj_nnreal
+  simpa [Real.coe_toNNReal, hpq.nonneg, hpq.symm.nonneg] using young_inequality a b hpq.toNNReal
 #align nnreal.young_inequality_real NNReal.young_inequality_real
 
 end NNReal
@@ -301,7 +299,7 @@ end NNReal
 namespace ENNReal
 
 /-- Young's inequality, `ℝ≥0∞` version with real conjugate exponents. -/
-theorem young_inequality (a b : ℝ≥0∞) {p q : ℝ} (hpq : p.IsConjugateExponent q) :
+theorem young_inequality (a b : ℝ≥0∞) {p q : ℝ} (hpq : p.IsConjExponent q) :
     a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q := by
   by_cases h : a = ⊤ ∨ b = ⊤
   · refine' le_trans le_top (le_of_eq _)
@@ -328,10 +326,10 @@ section HolderMinkowski
 namespace NNReal
 
 private theorem inner_le_Lp_mul_Lp_of_norm_le_one (f g : ι → ℝ≥0) {p q : ℝ}
-    (hpq : p.IsConjugateExponent q) (hf : ∑ i in s, f i ^ p ≤ 1) (hg : ∑ i in s, g i ^ q ≤ 1) :
+    (hpq : p.IsConjExponent q) (hf : ∑ i in s, f i ^ p ≤ 1) (hg : ∑ i in s, g i ^ q ≤ 1) :
     ∑ i in s, f i * g i ≤ 1 := by
-  have hp_ne_zero : Real.toNNReal p ≠ 0 := (zero_lt_one.trans hpq.one_lt_nnreal).ne.symm
-  have hq_ne_zero : Real.toNNReal q ≠ 0 := (zero_lt_one.trans hpq.symm.one_lt_nnreal).ne.symm
+  have hp_ne_zero : Real.toNNReal p ≠ 0 := (zero_lt_one.trans hpq.toNNReal.one_lt).ne.symm
+  have hq_ne_zero : Real.toNNReal q ≠ 0 := (zero_lt_one.trans hpq.toNNReal.symm.one_lt).ne.symm
   calc
     ∑ i in s, f i * g i ≤ ∑ i in s, (f i ^ p / Real.toNNReal p + g i ^ q / Real.toNNReal q) :=
       Finset.sum_le_sum fun i _ => young_inequality_real (f i) (g i) hpq
@@ -341,10 +339,10 @@ private theorem inner_le_Lp_mul_Lp_of_norm_le_one (f g : ι → ℝ≥0) {p q :
       refine' add_le_add _ _
       · rwa [div_le_iff hp_ne_zero, div_mul_cancel _ hp_ne_zero]
       · rwa [div_le_iff hq_ne_zero, div_mul_cancel _ hq_ne_zero]
-    _ = 1 := by simp_rw [one_div, hpq.inv_add_inv_conj_nnreal]
+    _ = 1 := by simp_rw [one_div, hpq.toNNReal.inv_add_inv_conj]
 
 private theorem inner_le_Lp_mul_Lp_of_norm_eq_zero (f g : ι → ℝ≥0) {p q : ℝ}
-    (hpq : p.IsConjugateExponent q) (hf : ∑ i in s, f i ^ p = 0) :
+    (hpq : p.IsConjExponent q) (hf : ∑ i in s, f i ^ p = 0) :
     ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q) := by
   simp only [hf, hpq.ne_zero, one_div, sum_eq_zero_iff, zero_rpow, zero_mul,
     inv_eq_zero, Ne.def, not_false_iff, le_zero_iff, mul_eq_zero]
@@ -356,7 +354,7 @@ private theorem inner_le_Lp_mul_Lp_of_norm_eq_zero (f g : ι → ℝ≥0) {p q :
 /-- Hölder inequality: the scalar product of two functions is bounded by the product of their
 `L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
 with `ℝ≥0`-valued functions. -/
-theorem inner_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q : ℝ} (hpq : p.IsConjugateExponent q) :
+theorem inner_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q : ℝ} (hpq : p.IsConjExponent q) :
     ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q) := by
   by_cases hF_zero : ∑ i in s, f i ^ p = 0
   · exact inner_le_Lp_mul_Lp_of_norm_eq_zero s f g hpq hF_zero
@@ -389,7 +387,7 @@ theorem inner_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q : ℝ} (hpq : p.IsConjuga
 `L^p` and `L^q` norms when `p` and `q` are conjugate exponents. A version for `NNReal`-valued
 functions. For an alternative version, convenient if the infinite sums are already expressed as
 `p`-th powers, see `inner_le_Lp_mul_Lq_hasSum`. -/
-theorem inner_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.IsConjugateExponent q)
+theorem inner_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.IsConjExponent q)
     (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) :
     (Summable fun i => f i * g i) ∧
       ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by
@@ -409,13 +407,13 @@ theorem inner_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.IsCo
   exact ⟨H₂, tsum_le_of_sum_le H₂ H₁⟩
 #align nnreal.inner_le_Lp_mul_Lq_tsum NNReal.inner_le_Lp_mul_Lq_tsum
 
-theorem summable_mul_of_Lp_Lq {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.IsConjugateExponent q)
+theorem summable_mul_of_Lp_Lq {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.IsConjExponent q)
     (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) :
     Summable fun i => f i * g i :=
   (inner_le_Lp_mul_Lq_tsum hpq hf hg).1
 #align nnreal.summable_mul_of_Lp_Lq NNReal.summable_mul_of_Lp_Lq
 
-theorem inner_le_Lp_mul_Lq_tsum' {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.IsConjugateExponent q)
+theorem inner_le_Lp_mul_Lq_tsum' {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.IsConjExponent q)
     (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ q) :
     ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) :=
   (inner_le_Lp_mul_Lq_tsum hpq hf hg).2
@@ -426,7 +424,7 @@ theorem inner_le_Lp_mul_Lq_tsum' {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.IsC
 functions. For an alternative version, convenient if the infinite sums are not already expressed as
 `p`-th powers, see `inner_le_Lp_mul_Lq_tsum`.  -/
 theorem inner_le_Lp_mul_Lq_hasSum {f g : ι → ℝ≥0} {A B : ℝ≥0} {p q : ℝ}
-    (hpq : p.IsConjugateExponent q) (hf : HasSum (fun i => f i ^ p) (A ^ p))
+    (hpq : p.IsConjExponent q) (hf : HasSum (fun i => f i ^ p) (A ^ p))
     (hg : HasSum (fun i => g i ^ q) (B ^ q)) : ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C := by
   obtain ⟨H₁, H₂⟩ := inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable
   have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hpq.ne_zero]
@@ -445,7 +443,7 @@ theorem rpow_sum_le_const_mul_sum_rpow (f : ι → ℝ≥0) {p : ℝ} (hp : 1 
   cases' eq_or_lt_of_le hp with hp hp
   · simp [← hp]
   let q : ℝ := p / (p - 1)
-  have hpq : p.IsConjugateExponent q := by rw [Real.isConjugateExponent_iff hp]
+  have hpq : p.IsConjExponent q := .conjExponent hp
   have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
   have hq : 1 / q * p = p - 1 := by
     rw [← hpq.div_conj_eq_sub_one]
@@ -457,7 +455,7 @@ theorem rpow_sum_le_const_mul_sum_rpow (f : ι → ℝ≥0) {p : ℝ} (hp : 1 
 
 /-- The `L_p` seminorm of a vector `f` is the greatest value of the inner product
 `∑ i in s, f i * g i` over functions `g` of `L_q` seminorm less than or equal to one. -/
-theorem isGreatest_Lp (f : ι → ℝ≥0) {p q : ℝ} (hpq : p.IsConjugateExponent q) :
+theorem isGreatest_Lp (f : ι → ℝ≥0) {p q : ℝ} (hpq : p.IsConjExponent q) :
     IsGreatest ((fun g : ι → ℝ≥0 => ∑ i in s, f i * g i) '' { g | ∑ i in s, g i ^ q ≤ 1 })
       ((∑ i in s, f i ^ p) ^ (1 / p)) := by
   constructor
@@ -487,7 +485,7 @@ theorem Lp_add_le (f g : ι → ℝ≥0) {p : ℝ} (hp : 1 ≤ p) :
   -- The result is trivial when `p = 1`, so we can assume `1 < p`.
   rcases eq_or_lt_of_le hp with (rfl | hp);
   · simp [Finset.sum_add_distrib]
-  have hpq := Real.isConjugateExponent_conjugateExponent hp
+  have hpq := Real.IsConjExponent.conjExponent hp
   have := isGreatest_Lp s (f + g) hpq
   simp only [Pi.add_apply, add_mul, sum_add_distrib] at this
   rcases this.1 with ⟨φ, hφ, H⟩
@@ -561,7 +559,7 @@ variable (f g : ι → ℝ) {p q : ℝ}
 /-- Hölder inequality: the scalar product of two functions is bounded by the product of their
 `L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
 with real-valued functions. -/
-theorem inner_le_Lp_mul_Lq (hpq : IsConjugateExponent p q) :
+theorem inner_le_Lp_mul_Lq (hpq : IsConjExponent p q) :
     ∑ i in s, f i * g i ≤ (∑ i in s, |f i| ^ p) ^ (1 / p) * (∑ i in s, |g i| ^ q) ^ (1 / q) := by
   have :=
     NNReal.coe_le_coe.2
@@ -603,7 +601,7 @@ variable {f g}
 /-- Hölder inequality: the scalar product of two functions is bounded by the product of their
 `L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
 with real-valued nonnegative functions. -/
-theorem inner_le_Lp_mul_Lq_of_nonneg (hpq : IsConjugateExponent p q) (hf : ∀ i ∈ s, 0 ≤ f i)
+theorem inner_le_Lp_mul_Lq_of_nonneg (hpq : IsConjExponent p q) (hf : ∀ i ∈ s, 0 ≤ f i)
     (hg : ∀ i ∈ s, 0 ≤ g i) :
     ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q) := by
   convert inner_le_Lp_mul_Lq s f g hpq using 3 <;> apply sum_congr rfl <;> intro i hi <;>
@@ -614,7 +612,7 @@ theorem inner_le_Lp_mul_Lq_of_nonneg (hpq : IsConjugateExponent p q) (hf : ∀ i
 `L^p` and `L^q` norms when `p` and `q` are conjugate exponents. A version for `ℝ`-valued functions.
 For an alternative version, convenient if the infinite sums are already expressed as `p`-th powers,
 see `inner_le_Lp_mul_Lq_hasSum_of_nonneg`. -/
-theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.IsConjugateExponent q) (hf : ∀ i, 0 ≤ f i)
+theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.IsConjExponent q) (hf : ∀ i, 0 ≤ f i)
     (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) :
     (Summable fun i => f i * g i) ∧
       ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) := by
@@ -626,13 +624,13 @@ theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.IsConjugateExponent q) (hf :
   exact NNReal.inner_le_Lp_mul_Lq_tsum hpq hf_sum hg_sum
 #align real.inner_le_Lp_mul_Lq_tsum_of_nonneg Real.inner_le_Lp_mul_Lq_tsum_of_nonneg
 
-theorem summable_mul_of_Lp_Lq_of_nonneg (hpq : p.IsConjugateExponent q) (hf : ∀ i, 0 ≤ f i)
+theorem summable_mul_of_Lp_Lq_of_nonneg (hpq : p.IsConjExponent q) (hf : ∀ i, 0 ≤ f i)
     (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) :
     Summable fun i => f i * g i :=
   (inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).1
 #align real.summable_mul_of_Lp_Lq_of_nonneg Real.summable_mul_of_Lp_Lq_of_nonneg
 
-theorem inner_le_Lp_mul_Lq_tsum_of_nonneg' (hpq : p.IsConjugateExponent q) (hf : ∀ i, 0 ≤ f i)
+theorem inner_le_Lp_mul_Lq_tsum_of_nonneg' (hpq : p.IsConjExponent q) (hf : ∀ i, 0 ≤ f i)
     (hg : ∀ i, 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ q) :
     ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) :=
   (inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).2
@@ -642,7 +640,7 @@ theorem inner_le_Lp_mul_Lq_tsum_of_nonneg' (hpq : p.IsConjugateExponent q) (hf :
 `L^p` and `L^q` norms when `p` and `q` are conjugate exponents. A version for `NNReal`-valued
 functions. For an alternative version, convenient if the infinite sums are not already expressed as
 `p`-th powers, see `inner_le_Lp_mul_Lq_tsum_of_nonneg`.  -/
-theorem inner_le_Lp_mul_Lq_hasSum_of_nonneg (hpq : p.IsConjugateExponent q) {A B : ℝ} (hA : 0 ≤ A)
+theorem inner_le_Lp_mul_Lq_hasSum_of_nonneg (hpq : p.IsConjExponent q) {A B : ℝ} (hA : 0 ≤ A)
     (hB : 0 ≤ B) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i)
     (hf_sum : HasSum (fun i => f i ^ p) (A ^ p)) (hg_sum : HasSum (fun i => g i ^ q) (B ^ q)) :
     ∃ C : ℝ, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => f i * g i) C := by
@@ -739,7 +737,7 @@ variable (f g : ι → ℝ≥0∞) {p q : ℝ}
 /-- Hölder inequality: the scalar product of two functions is bounded by the product of their
 `L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
 with `ℝ≥0∞`-valued functions. -/
-theorem inner_le_Lp_mul_Lq (hpq : p.IsConjugateExponent q) :
+theorem inner_le_Lp_mul_Lq (hpq : p.IsConjExponent q) :
     ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q) := by
   by_cases H : (∑ i in s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i in s, g i ^ q) ^ (1 / q) = 0
   · replace H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0
@@ -773,7 +771,7 @@ theorem rpow_sum_le_const_mul_sum_rpow (hp : 1 ≤ p) :
   cases' eq_or_lt_of_le hp with hp hp
   · simp [← hp]
   let q : ℝ := p / (p - 1)
-  have hpq : p.IsConjugateExponent q := by rw [Real.isConjugateExponent_iff hp]
+  have hpq : p.IsConjExponent q := .conjExponent hp
   have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
   have hq : 1 / q * p = p - 1 := by
     rw [← hpq.div_conj_eq_sub_one]
diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean
index 296ab0bbd7604..301de111f8fdd 100644
--- a/Mathlib/Analysis/NormedSpace/lpSpace.lean
+++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean
@@ -526,10 +526,10 @@ instance normedAddCommGroup [hp : Fact (1 ≤ p)] : NormedAddCommGroup (lp E p)
           apply norm_add_le
       eq_zero_of_map_eq_zero' := fun f => norm_eq_zero_iff.1 }
 
--- TODO: define an `ENNReal` version of `IsConjugateExponent`, and then express this inequality
+-- TODO: define an `ENNReal` version of `IsConjExponent`, and then express this inequality
 -- in a better version which also covers the case `p = 1, q = ∞`.
 /-- Hölder inequality -/
-protected theorem tsum_mul_le_mul_norm {p q : ℝ≥0∞} (hpq : p.toReal.IsConjugateExponent q.toReal)
+protected theorem tsum_mul_le_mul_norm {p q : ℝ≥0∞} (hpq : p.toReal.IsConjExponent q.toReal)
     (f : lp E p) (g : lp E q) :
     (Summable fun i => ‖f i‖ * ‖g i‖) ∧ ∑' i, ‖f i‖ * ‖g i‖ ≤ ‖f‖ * ‖g‖ := by
   have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _
@@ -542,12 +542,12 @@ protected theorem tsum_mul_le_mul_norm {p q : ℝ≥0∞} (hpq : p.toReal.IsConj
   exact ⟨hC.summable, hC'⟩
 #align lp.tsum_mul_le_mul_norm lp.tsum_mul_le_mul_norm
 
-protected theorem summable_mul {p q : ℝ≥0∞} (hpq : p.toReal.IsConjugateExponent q.toReal)
+protected theorem summable_mul {p q : ℝ≥0∞} (hpq : p.toReal.IsConjExponent q.toReal)
     (f : lp E p) (g : lp E q) : Summable fun i => ‖f i‖ * ‖g i‖ :=
   (lp.tsum_mul_le_mul_norm hpq f g).1
 #align lp.summable_mul lp.summable_mul
 
-protected theorem tsum_mul_le_mul_norm' {p q : ℝ≥0∞} (hpq : p.toReal.IsConjugateExponent q.toReal)
+protected theorem tsum_mul_le_mul_norm' {p q : ℝ≥0∞} (hpq : p.toReal.IsConjExponent q.toReal)
     (f : lp E p) (g : lp E q) : ∑' i, ‖f i‖ * ‖g i‖ ≤ ‖f‖ * ‖g‖ :=
   (lp.tsum_mul_le_mul_norm hpq f g).2
 #align lp.tsum_mul_le_mul_norm' lp.tsum_mul_le_mul_norm'
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
index bafd56e0d710b..006f8f4213e76 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
@@ -110,7 +110,7 @@ theorem Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma {s t a b : ℝ} (hs : 0 <
   -- We will apply Hölder's inequality, for the conjugate exponents `p = 1 / a`
   -- and `q = 1 / b`, to the functions `f a s` and `f b t`, where `f` is as follows:
   let f : ℝ → ℝ → ℝ → ℝ := fun c u x => exp (-c * x) * x ^ (c * (u - 1))
-  have e : IsConjugateExponent (1 / a) (1 / b) := Real.isConjugateExponent_one_div ha hb hab
+  have e : IsConjExponent (1 / a) (1 / b) := Real.isConjExponent_one_div ha hb hab
   have hab' : b = 1 - a := by linarith
   have hst : 0 < a * s + b * t := add_pos (mul_pos ha hs) (mul_pos hb ht)
   -- some properties of f:
diff --git a/Mathlib/Data/Real/ConjExponents.lean b/Mathlib/Data/Real/ConjExponents.lean
new file mode 100644
index 0000000000000..c8206e344cfa1
--- /dev/null
+++ b/Mathlib/Data/Real/ConjExponents.lean
@@ -0,0 +1,234 @@
+/-
+Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel, Yury Kudryashov
+-/
+import Mathlib.Data.ENNReal.Real
+
+#align_import data.real.conjugate_exponents from "leanprover-community/mathlib"@"2196ab363eb097c008d4497125e0dde23fb36db2"
+
+/-!
+# Real conjugate exponents
+
+This file defines conjugate exponents in `ℝ` and `ℝ≥0`. Real numbers `p` and `q` are *conjugate* if
+they are both greater than `1` and satisfy `p⁻¹ + q⁻¹ = 1`. This property shows up often in
+analysis, especially when dealing with `L^p` spaces.
+
+## Main declarations
+
+* `Real.IsConjExponent`: Predicate for two real numbers to be conjugate.
+* `Real.conjExponent`: Conjugate exponent of a real number.
+* `NNReal.IsConjExponent`: Predicate for two nonnegative real numbers to be conjugate.
+* `NNReal.conjExponent`: Conjugate exponent of a nonnegative real number.
+
+## TODO
+
+* Eradicate the `1 / p` spelling in lemmas.
+* Do we want an `ℝ≥0∞` version?
+-/
+
+noncomputable section
+
+open scoped ENNReal
+
+namespace Real
+
+/-- Two real exponents `p, q` are conjugate if they are `> 1` and satisfy the equality
+`1/p + 1/q = 1`. This condition shows up in many theorems in analysis, notably related to `L^p`
+norms. -/
+@[mk_iff]
+structure IsConjExponent (p q : ℝ) : Prop where
+  one_lt : 1 < p
+  inv_add_inv_conj : p⁻¹ + q⁻¹ = 1
+#align real.is_conjugate_exponent Real.IsConjExponent
+
+/-- The conjugate exponent of `p` is `q = p/(p-1)`, so that `1/p + 1/q = 1`. -/
+def conjExponent (p : ℝ) : ℝ := p / (p - 1)
+#align real.conjugate_exponent Real.conjExponent
+
+variable {a b p q : ℝ} (h : p.IsConjExponent q)
+
+namespace IsConjExponent
+
+/- Register several non-vanishing results following from the fact that `p` has a conjugate exponent
+`q`: many computations using these exponents require clearing out denominators, which can be done
+with `field_simp` given a proof that these denominators are non-zero, so we record the most usual
+ones. -/
+theorem pos : 0 < p := lt_trans zero_lt_one h.one_lt
+#align real.is_conjugate_exponent.pos Real.IsConjExponent.pos
+
+theorem nonneg : 0 ≤ p := le_of_lt h.pos
+#align real.is_conjugate_exponent.nonneg Real.IsConjExponent.nonneg
+
+theorem ne_zero : p ≠ 0 := ne_of_gt h.pos
+#align real.is_conjugate_exponent.ne_zero Real.IsConjExponent.ne_zero
+
+theorem sub_one_pos : 0 < p - 1 := sub_pos.2 h.one_lt
+#align real.is_conjugate_exponent.sub_one_pos Real.IsConjExponent.sub_one_pos
+
+theorem sub_one_ne_zero : p - 1 ≠ 0 := ne_of_gt h.sub_one_pos
+#align real.is_conjugate_exponent.sub_one_ne_zero Real.IsConjExponent.sub_one_ne_zero
+
+protected lemma inv_pos : 0 < p⁻¹ := inv_pos.2 h.pos
+protected lemma inv_nonneg : 0 ≤ p⁻¹ := h.inv_pos.le
+protected lemma inv_ne_zero : p⁻¹ ≠ 0 := h.inv_pos.ne'
+
+theorem one_div_pos : 0 < 1 / p := _root_.one_div_pos.2 h.pos
+#align real.is_conjugate_exponent.one_div_pos Real.IsConjExponent.one_div_pos
+
+theorem one_div_nonneg : 0 ≤ 1 / p := le_of_lt h.one_div_pos
+#align real.is_conjugate_exponent.one_div_nonneg Real.IsConjExponent.one_div_nonneg
+
+theorem one_div_ne_zero : 1 / p ≠ 0 := ne_of_gt h.one_div_pos
+#align real.is_conjugate_exponent.one_div_ne_zero Real.IsConjExponent.one_div_ne_zero
+
+theorem conj_eq : q = p / (p - 1) := by
+  have := h.inv_add_inv_conj
+  rw [← eq_sub_iff_add_eq', inv_eq_iff_eq_inv] at this
+  field_simp [this, h.ne_zero]
+#align real.is_conjugate_exponent.conj_eq Real.IsConjExponent.conj_eq
+
+lemma conjExponent_eq : conjExponent p = q := h.conj_eq.symm
+#align real.is_conjugate_exponent.conjugate_eq Real.IsConjExponent.conjExponent_eq
+
+lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ := sub_eq_of_eq_add' h.inv_add_inv_conj.symm
+lemma inv_sub_one : p⁻¹ - 1 = -q⁻¹ := by rw [← h.inv_add_inv_conj, sub_add_cancel']
+
+theorem sub_one_mul_conj : (p - 1) * q = p :=
+  mul_comm q (p - 1) ▸ (eq_div_iff h.sub_one_ne_zero).1 h.conj_eq
+#align real.is_conjugate_exponent.sub_one_mul_conj Real.IsConjExponent.sub_one_mul_conj
+
+theorem mul_eq_add : p * q = p + q := by
+  simpa only [sub_mul, sub_eq_iff_eq_add, one_mul] using h.sub_one_mul_conj
+#align real.is_conjugate_exponent.mul_eq_add Real.IsConjExponent.mul_eq_add
+
+@[symm] protected lemma symm : q.IsConjExponent p where
+  one_lt := by simpa only [h.conj_eq] using (one_lt_div h.sub_one_pos).mpr (sub_one_lt p)
+  inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
+#align real.is_conjugate_exponent.symm Real.IsConjExponent.symm
+
+theorem div_conj_eq_sub_one : p / q = p - 1 := by
+  field_simp [h.symm.ne_zero]
+  rw [h.sub_one_mul_conj]
+#align real.is_conjugate_exponent.div_conj_eq_sub_one Real.IsConjExponent.div_conj_eq_sub_one
+
+theorem inv_add_inv_conj_ennreal : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1 := by
+  rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos,
+    ← ENNReal.ofReal_inv_of_pos h.symm.pos, ← ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg,
+    h.inv_add_inv_conj]
+#align real.is_conjugate_exponent.inv_add_inv_conj_ennreal Real.IsConjExponent.inv_add_inv_conj_ennreal
+
+protected lemma inv_inv (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : a⁻¹.IsConjExponent b⁻¹ :=
+  ⟨one_lt_inv ha $ by linarith, by simpa only [inv_inv]⟩
+
+lemma inv_one_sub_inv (ha₀ : 0 < a) (ha₁ : a < 1) : a⁻¹.IsConjExponent (1 - a)⁻¹ :=
+  .inv_inv ha₀ (sub_pos_of_lt ha₁) $ add_tsub_cancel_of_le ha₁.le
+
+lemma one_sub_inv_inv (ha₀ : 0 < a) (ha₁ : a < 1) : (1 - a)⁻¹.IsConjExponent a⁻¹ :=
+  (inv_one_sub_inv ha₀ ha₁).symm
+
+end IsConjExponent
+
+lemma isConjExponent_iff_eq_conjExponent (hp : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1) :=
+  ⟨IsConjExponent.conj_eq, fun h ↦ ⟨hp, by field_simp [h]⟩⟩
+#align real.is_conjugate_exponent_iff Real.isConjExponent_iff
+
+lemma IsConjExponent.conjExponent (h : 1 < p) : p.IsConjExponent (conjExponent p) :=
+  (isConjExponent_iff_eq_conjExponent h).2 rfl
+#align real.is_conjugate_exponent_conjugate_exponent Real.IsConjExponent.conjExponent
+
+lemma isConjExponent_one_div (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
+    (1 / a).IsConjExponent (1 / b) := by simpa using IsConjExponent.inv_inv ha hb hab
+#align real.is_conjugate_exponent_one_div Real.isConjExponent_one_div
+
+end Real
+
+namespace NNReal
+
+/-- Two nonnegative real exponents `p, q` are conjugate if they are `> 1` and satisfy the equality
+`1/p + 1/q = 1`. This condition shows up in many theorems in analysis, notably related to `L^p`
+norms. -/
+@[mk_iff, pp_dot]
+structure IsConjExponent (p q : ℝ≥0) : Prop where
+  one_lt : 1 < p
+  inv_add_inv_conj : p⁻¹ + q⁻¹ = 1
+#align real.is_conjugate_exponent.one_lt_nnreal NNReal.IsConjExponent.one_lt
+#align real.is_conjugate_exponent.inv_add_inv_conj_nnreal NNReal.IsConjExponent.inv_add_inv_conj
+
+/-- The conjugate exponent of `p` is `q = p/(p-1)`, so that `1/p + 1/q = 1`. -/
+noncomputable def conjExponent (p : ℝ≥0) : ℝ≥0 := p / (p - 1)
+
+variable {a b p q : ℝ≥0} (h : p.IsConjExponent q)
+
+@[simp, norm_cast] lemma isConjExponent_coe : (p : ℝ).IsConjExponent q ↔ p.IsConjExponent q := by
+  simp [Real.isConjExponent_iff, isConjExponent_iff]; norm_cast; simp
+
+alias ⟨_, IsConjExponent.coe⟩ := isConjExponent_coe
+
+namespace IsConjExponent
+
+/- Register several non-vanishing results following from the fact that `p` has a conjugate exponent
+`q`: many computations using these exponents require clearing out denominators, which can be done
+with `field_simp` given a proof that these denominators are non-zero, so we record the most usual
+ones. -/
+lemma one_le : 1 ≤ p := h.one_lt.le
+lemma pos : 0 < p := zero_lt_one.trans h.one_lt
+lemma ne_zero : p ≠ 0 := h.pos.ne'
+
+lemma sub_one_pos : 0 < p - 1 := tsub_pos_of_lt h.one_lt
+lemma sub_one_ne_zero : p - 1 ≠ 0 := h.sub_one_pos.ne'
+
+lemma inv_pos : 0 < p⁻¹ := _root_.inv_pos.2 h.pos
+lemma inv_ne_zero : p⁻¹ ≠ 0 := h.inv_pos.ne'
+
+lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ := tsub_eq_of_eq_add_rev h.inv_add_inv_conj.symm
+
+lemma conj_eq : q = p / (p - 1) := by
+  simpa only [← coe_one, ← NNReal.coe_sub h.one_le, ← NNReal.coe_div, coe_inj] using h.coe.conj_eq
+
+lemma conjExponent_eq : conjExponent p = q := h.conj_eq.symm
+
+lemma sub_one_mul_conj : (p - 1) * q = p :=
+  mul_comm q (p - 1) ▸ (eq_div_iff h.sub_one_ne_zero).1 h.conj_eq
+
+lemma mul_eq_add : p * q = p + q := by
+  simpa only [← NNReal.coe_mul, ← NNReal.coe_add, NNReal.coe_inj] using h.coe.mul_eq_add
+
+@[symm]
+protected lemma symm : q.IsConjExponent p where
+  one_lt := by
+      rw [h.conj_eq]
+      exact (one_lt_div h.sub_one_pos).mpr (tsub_lt_self h.pos zero_lt_one)
+  inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
+
+lemma div_conj_eq_sub_one : p / q = p - 1 := by field_simp [h.symm.ne_zero]; rw [h.sub_one_mul_conj]
+
+lemma inv_add_inv_conj_ennreal : (p⁻¹ + q⁻¹ : ℝ≥0∞) = 1 := by norm_cast; exact h.inv_add_inv_conj
+
+protected lemma inv_inv (ha : a ≠ 0) (hb : b ≠ 0) (hab : a + b = 1) :
+    a⁻¹.IsConjExponent b⁻¹ :=
+  ⟨one_lt_inv ha.bot_lt $ by rw [← hab]; exact lt_add_of_pos_right _ hb.bot_lt, by
+    simpa only [inv_inv] using hab⟩
+
+lemma inv_one_sub_inv (ha₀ : a ≠ 0) (ha₁ : a < 1) : a⁻¹.IsConjExponent (1 - a)⁻¹ :=
+  .inv_inv ha₀ (tsub_pos_of_lt ha₁).ne' $ add_tsub_cancel_of_le ha₁.le
+
+lemma one_sub_inv_inv (ha₀ : a ≠ 0) (ha₁ : a < 1) : (1 - a)⁻¹.IsConjExponent a⁻¹ :=
+  (inv_one_sub_inv ha₀ ha₁).symm
+
+end IsConjExponent
+
+lemma isConjExponent_iff_eq_conjExponent (h : 1 < p) : p.IsConjExponent q ↔ q = p / (p - 1) := by
+  rw [← isConjExponent_coe, Real.isConjExponent_iff_eq_conjExponent (mod_cast h), ← coe_inj,
+    NNReal.coe_div, NNReal.coe_sub h.le, coe_one]
+
+protected lemma IsConjExponent.conjExponent (h : 1 < p) : p.IsConjExponent (conjExponent p) :=
+  (isConjExponent_iff_eq_conjExponent h).2 rfl
+
+end NNReal
+
+protected lemma Real.IsConjExponent.toNNReal {p q : ℝ} (hpq : p.IsConjExponent q) :
+    p.toNNReal.IsConjExponent q.toNNReal where
+  one_lt := by simpa using hpq.one_lt
+  inv_add_inv_conj := by rw [← toNNReal_inv, ← toNNReal_inv, ← toNNReal_add hpq.inv_nonneg
+    hpq.symm.inv_nonneg, hpq.inv_add_inv_conj, toNNReal_one]
diff --git a/Mathlib/Data/Real/ConjugateExponents.lean b/Mathlib/Data/Real/ConjugateExponents.lean
deleted file mode 100644
index 13f69109b6a68..0000000000000
--- a/Mathlib/Data/Real/ConjugateExponents.lean
+++ /dev/null
@@ -1,142 +0,0 @@
-/-
-Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sébastien Gouëzel, Yury Kudryashov
--/
-import Mathlib.Data.ENNReal.Real
-
-#align_import data.real.conjugate_exponents from "leanprover-community/mathlib"@"2196ab363eb097c008d4497125e0dde23fb36db2"
-
-/-!
-# Real conjugate exponents
-
-`p.IsConjugateExponent q` registers the fact that the real numbers `p` and `q` are `> 1` and
-satisfy `1/p + 1/q = 1`. This property shows up often in analysis, especially when dealing with
-`L^p` spaces.
-
-We make several basic facts available through dot notation in this situation.
-
-We also introduce `p.conjugateExponent` for `p / (p-1)`. When `p > 1`, it is conjugate to `p`.
-
-## TODO
-
-Eradicate the `1 / p` spelling in lemmas.
--/
-
-
-noncomputable section
-
-namespace Real
-
-/-- Two real exponents `p, q` are conjugate if they are `> 1` and satisfy the equality
-`1/p + 1/q = 1`. This condition shows up in many theorems in analysis, notably related to `L^p`
-norms. -/
-structure IsConjugateExponent (p q : ℝ) : Prop where
-  one_lt : 1 < p
-  inv_add_inv_conj : p⁻¹ + q⁻¹ = 1
-#align real.is_conjugate_exponent Real.IsConjugateExponent
-
-/-- The conjugate exponent of `p` is `q = p/(p-1)`, so that `1/p + 1/q = 1`. -/
-def conjugateExponent (p : ℝ) : ℝ := p / (p - 1)
-#align real.conjugate_exponent Real.conjugateExponent
-
-namespace IsConjugateExponent
-
-variable {p q : ℝ} (h : p.IsConjugateExponent q)
-
-/- Register several non-vanishing results following from the fact that `p` has a conjugate exponent
-`q`: many computations using these exponents require clearing out denominators, which can be done
-with `field_simp` given a proof that these denominators are non-zero, so we record the most usual
-ones. -/
-theorem pos : 0 < p := lt_trans zero_lt_one h.one_lt
-#align real.is_conjugate_exponent.pos Real.IsConjugateExponent.pos
-
-theorem nonneg : 0 ≤ p := le_of_lt h.pos
-#align real.is_conjugate_exponent.nonneg Real.IsConjugateExponent.nonneg
-
-theorem ne_zero : p ≠ 0 := ne_of_gt h.pos
-#align real.is_conjugate_exponent.ne_zero Real.IsConjugateExponent.ne_zero
-
-theorem sub_one_pos : 0 < p - 1 := sub_pos.2 h.one_lt
-#align real.is_conjugate_exponent.sub_one_pos Real.IsConjugateExponent.sub_one_pos
-
-theorem sub_one_ne_zero : p - 1 ≠ 0 := ne_of_gt h.sub_one_pos
-#align real.is_conjugate_exponent.sub_one_ne_zero Real.IsConjugateExponent.sub_one_ne_zero
-
-protected lemma inv_pos : 0 < p⁻¹ := inv_pos.2 h.pos
-protected lemma inv_nonneg : 0 ≤ p⁻¹ := h.inv_pos.le
-protected lemma inv_ne_zero : p⁻¹ ≠ 0 := h.inv_pos.ne'
-
-theorem one_div_pos : 0 < 1 / p := _root_.one_div_pos.2 h.pos
-#align real.is_conjugate_exponent.one_div_pos Real.IsConjugateExponent.one_div_pos
-
-theorem one_div_nonneg : 0 ≤ 1 / p := le_of_lt h.one_div_pos
-#align real.is_conjugate_exponent.one_div_nonneg Real.IsConjugateExponent.one_div_nonneg
-
-theorem one_div_ne_zero : 1 / p ≠ 0 := ne_of_gt h.one_div_pos
-#align real.is_conjugate_exponent.one_div_ne_zero Real.IsConjugateExponent.one_div_ne_zero
-
-theorem conj_eq : q = p / (p - 1) := by
-  have := h.inv_add_inv_conj
-  rw [← eq_sub_iff_add_eq', inv_eq_iff_eq_inv] at this
-  field_simp [this, h.ne_zero]
-#align real.is_conjugate_exponent.conj_eq Real.IsConjugateExponent.conj_eq
-
-theorem conjugate_eq : conjugateExponent p = q := h.conj_eq.symm
-#align real.is_conjugate_exponent.conjugate_eq Real.IsConjugateExponent.conjugate_eq
-
-theorem sub_one_mul_conj : (p - 1) * q = p :=
-  mul_comm q (p - 1) ▸ (eq_div_iff h.sub_one_ne_zero).1 h.conj_eq
-#align real.is_conjugate_exponent.sub_one_mul_conj Real.IsConjugateExponent.sub_one_mul_conj
-
-theorem mul_eq_add : p * q = p + q := by
-  simpa only [sub_mul, sub_eq_iff_eq_add, one_mul] using h.sub_one_mul_conj
-#align real.is_conjugate_exponent.mul_eq_add Real.IsConjugateExponent.mul_eq_add
-
-@[symm]
-protected theorem symm : q.IsConjugateExponent p :=
-  { one_lt := by
-      rw [h.conj_eq]
-      exact (one_lt_div h.sub_one_pos).mpr (sub_one_lt p)
-    inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj }
-#align real.is_conjugate_exponent.symm Real.IsConjugateExponent.symm
-
-theorem div_conj_eq_sub_one : p / q = p - 1 := by
-  field_simp [h.symm.ne_zero]
-  rw [h.sub_one_mul_conj]
-#align real.is_conjugate_exponent.div_conj_eq_sub_one Real.IsConjugateExponent.div_conj_eq_sub_one
-
-theorem one_lt_nnreal : 1 < Real.toNNReal p := by
-  rw [← Real.toNNReal_one, Real.toNNReal_lt_toNNReal_iff h.pos]
-  exact h.one_lt
-#align real.is_conjugate_exponent.one_lt_nnreal Real.IsConjugateExponent.one_lt_nnreal
-
-theorem inv_add_inv_conj_nnreal : p.toNNReal⁻¹ + q.toNNReal⁻¹ = 1 := by
-  rw [← Real.toNNReal_one, ← Real.toNNReal_inv, ← Real.toNNReal_inv,
-      ← Real.toNNReal_add h.inv_nonneg h.symm.inv_nonneg, h.inv_add_inv_conj]
-#align real.is_conjugate_exponent.inv_add_inv_conj_nnreal Real.IsConjugateExponent.inv_add_inv_conj_nnreal
-
-theorem inv_add_inv_conj_ennreal : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1 := by
-  rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos,
-    ← ENNReal.ofReal_inv_of_pos h.symm.pos, ← ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg,
-    h.inv_add_inv_conj]
-#align real.is_conjugate_exponent.inv_add_inv_conj_ennreal Real.IsConjugateExponent.inv_add_inv_conj_ennreal
-
-end IsConjugateExponent
-
-theorem isConjugateExponent_iff {p q : ℝ} (h : 1 < p) : p.IsConjugateExponent q ↔ q = p / (p - 1) :=
-  ⟨fun H => H.conj_eq, fun H => ⟨h, by field_simp [H, ne_of_gt (lt_trans zero_lt_one h)] ⟩⟩
-#align real.is_conjugate_exponent_iff Real.isConjugateExponent_iff
-
-theorem isConjugateExponent_conjugateExponent {p : ℝ} (h : 1 < p) :
-    p.IsConjugateExponent (conjugateExponent p) := (isConjugateExponent_iff h).2 rfl
-#align real.is_conjugate_exponent_conjugate_exponent Real.isConjugateExponent_conjugateExponent
-
-lemma isConjugateExponent_inv {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
-    a⁻¹.IsConjugateExponent b⁻¹ := ⟨one_lt_inv ha $ by linarith, by simpa only [inv_inv]⟩
-
-theorem isConjugateExponent_one_div {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
-    (1 / a).IsConjugateExponent (1 / b) := by simpa using isConjugateExponent_inv ha hb hab
-#align real.is_conjugate_exponent_one_div Real.isConjugateExponent_one_div
-
-end Real
diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean
index 5c68e8c618b4a..33548df1c2b34 100644
--- a/Mathlib/MeasureTheory/Integral/Bochner.lean
+++ b/Mathlib/MeasureTheory/Integral/Bochner.lean
@@ -1715,7 +1715,7 @@ theorem mul_meas_ge_le_integral_of_nonneg {f : α → ℝ} (hf_nonneg : 0 ≤ᵐ
 norms of functions is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are
 conjugate exponents. -/
 theorem integral_mul_norm_le_Lp_mul_Lq {E} [NormedAddCommGroup E] {f g : α → E} {p q : ℝ}
-    (hpq : p.IsConjugateExponent q) (hf : Memℒp f (ENNReal.ofReal p) μ)
+    (hpq : p.IsConjExponent q) (hf : Memℒp f (ENNReal.ofReal p) μ)
     (hg : Memℒp g (ENNReal.ofReal q) μ) :
     ∫ a, ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ a, ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ a, ‖g a‖ ^ q ∂μ) ^ (1 / q) := by
   -- translate the Bochner integrals into Lebesgue integrals.
@@ -1763,7 +1763,7 @@ set_option linter.uppercaseLean3 false in
 /-- Hölder's inequality for functions `α → ℝ`. The integral of the product of two nonnegative
 functions is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
 exponents. -/
-theorem integral_mul_le_Lp_mul_Lq_of_nonneg {p q : ℝ} (hpq : p.IsConjugateExponent q) {f g : α → ℝ}
+theorem integral_mul_le_Lp_mul_Lq_of_nonneg {p q : ℝ} (hpq : p.IsConjExponent q) {f g : α → ℝ}
     (hf_nonneg : 0 ≤ᵐ[μ] f) (hg_nonneg : 0 ≤ᵐ[μ] g) (hf : Memℒp f (ENNReal.ofReal p) μ)
     (hg : Memℒp g (ENNReal.ofReal q) μ) :
     ∫ a, f a * g a ∂μ ≤ (∫ a, f a ^ p ∂μ) ^ (1 / p) * (∫ a, g a ^ q ∂μ) ^ (1 / q) := by
diff --git a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean
index 89959e0175024..bacce08c674d9 100644
--- a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean
+++ b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean
@@ -62,7 +62,7 @@ variable {α : Type*} [MeasurableSpace α] {μ : Measure α}
 
 namespace ENNReal
 
-theorem lintegral_mul_le_one_of_lintegral_rpow_eq_one {p q : ℝ} (hpq : p.IsConjugateExponent q)
+theorem lintegral_mul_le_one_of_lintegral_rpow_eq_one {p q : ℝ} (hpq : p.IsConjExponent q)
     {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf_norm : ∫⁻ a, f a ^ p ∂μ = 1)
     (hg_norm : ∫⁻ a, g a ^ q ∂μ = 1) : (∫⁻ a, (f * g) a ∂μ) ≤ 1 := by
   calc
@@ -106,7 +106,7 @@ theorem lintegral_rpow_funMulInvSnorm_eq_one {p : ℝ} (hp0_lt : 0 < p) {f : α
 #align ennreal.lintegral_rpow_fun_mul_inv_snorm_eq_one ENNReal.lintegral_rpow_funMulInvSnorm_eq_one
 
 /-- Hölder's inequality in case of finite non-zero integrals -/
-theorem lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top {p q : ℝ} (hpq : p.IsConjugateExponent q)
+theorem lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top {p q : ℝ} (hpq : p.IsConjExponent q)
     {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf_nontop : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤)
     (hg_nontop : (∫⁻ a, g a ^ q ∂μ) ≠ ⊤) (hf_nonzero : (∫⁻ a, f a ^ p ∂μ) ≠ 0)
     (hg_nonzero : (∫⁻ a, g a ^ q ∂μ) ≠ 0) :
@@ -160,7 +160,7 @@ theorem lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top {p q : ℝ} (hp0_lt : 0
 /-- Hölder's inequality for functions `α → ℝ≥0∞`. The integral of the product of two functions
 is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
 exponents. -/
-theorem lintegral_mul_le_Lp_mul_Lq (μ : Measure α) {p q : ℝ} (hpq : p.IsConjugateExponent q)
+theorem lintegral_mul_le_Lp_mul_Lq (μ : Measure α) {p q : ℝ} (hpq : p.IsConjExponent q)
     {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
     (∫⁻ a, (f * g) a ∂μ) ≤ (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ q ∂μ) ^ (1 / q) := by
   by_cases hf_zero : ∫⁻ a, f a ^ p ∂μ = 0
@@ -322,9 +322,8 @@ theorem lintegral_Lp_mul_le_Lq_mul_Lr {α} [MeasurableSpace α] {p q r : ℝ} (h
   have hq0_ne : q ≠ 0 := (ne_of_lt hq0_lt).symm
   have h_one_div_r : 1 / r = 1 / p - 1 / q := by rw [hpqr]; simp
   let p2 := q / p
-  let q2 := p2.conjugateExponent
-  have hp2q2 : p2.IsConjugateExponent q2 :=
-    Real.isConjugateExponent_conjugateExponent (by simp [_root_.lt_div_iff, hpq, hp0_lt])
+  let q2 := p2.conjExponent
+  have hp2q2 : p2.IsConjExponent q2 := .conjExponent (by simp [_root_.lt_div_iff, hpq, hp0_lt])
   calc
     (∫⁻ a : α, (f * g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ a : α, f a ^ p * g a ^ p ∂μ) ^ (1 / p) := by
       simp_rw [Pi.mul_apply, ENNReal.mul_rpow_of_nonneg _ _ hp0]
@@ -341,12 +340,12 @@ theorem lintegral_Lp_mul_le_Lq_mul_Lr {α} [MeasurableSpace α] {p q r : ℝ} (h
         rw [mul_comm, ← div_eq_iff hp0_ne]
       have hpq2 : p * q2 = r := by
         rw [← inv_inv r, ← one_div, ← one_div, h_one_div_r]
-        field_simp [Real.conjugateExponent, hp0_ne, hq0_ne]
+        field_simp [Real.conjExponent, hp0_ne, hq0_ne]
       simp_rw [div_mul_div_comm, mul_one, mul_comm p2, mul_comm q2, hpp2, hpq2]
 #align ennreal.lintegral_Lp_mul_le_Lq_mul_Lr ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr
 
 theorem lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow {p q : ℝ}
-    (hpq : p.IsConjugateExponent q) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    (hpq : p.IsConjExponent q) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
     (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) :
     (∫⁻ a, f a * g a ^ (p - 1) ∂μ) ≤
       (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ p ∂μ) ^ (1 / q) := by
@@ -366,7 +365,7 @@ theorem lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow {p q : ℝ}
 #align ennreal.lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow ENNReal.lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow
 
 theorem lintegral_rpow_add_le_add_snorm_mul_lintegral_rpow_add {p q : ℝ}
-    (hpq : p.IsConjugateExponent q) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
+    (hpq : p.IsConjExponent q) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
     (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) (hg : AEMeasurable g μ) (hg_top : (∫⁻ a, g a ^ p ∂μ) ≠ ⊤) :
     (∫⁻ a, (f + g) a ^ p ∂μ) ≤
       ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) *
@@ -401,7 +400,7 @@ theorem lintegral_rpow_add_le_add_snorm_mul_lintegral_rpow_add {p q : ℝ}
       · exact lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow hpq hg (hf.add hg) hg_top
 #align ennreal.lintegral_rpow_add_le_add_snorm_mul_lintegral_rpow_add ENNReal.lintegral_rpow_add_le_add_snorm_mul_lintegral_rpow_add
 
-private theorem lintegral_Lp_add_le_aux {p q : ℝ} (hpq : p.IsConjugateExponent q) {f g : α → ℝ≥0∞}
+private theorem lintegral_Lp_add_le_aux {p q : ℝ} (hpq : p.IsConjExponent q) {f g : α → ℝ≥0∞}
     (hf : AEMeasurable f μ) (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) (hg : AEMeasurable g μ)
     (hg_top : (∫⁻ a, g a ^ p ∂μ) ≠ ⊤) (h_add_zero : (∫⁻ a, (f + g) a ^ p ∂μ) ≠ 0)
     (h_add_top : (∫⁻ a, (f + g) a ^ p ∂μ) ≠ ⊤) :
@@ -452,7 +451,7 @@ theorem lintegral_Lp_add_le {p : ℝ} {f g : α → ℝ≥0∞} (hf : AEMeasurab
     refine' lt_of_le_of_ne hp1 _
     symm
     exact h1
-  have hpq := Real.isConjugateExponent_conjugateExponent hp1_lt
+  have hpq := Real.IsConjExponent.conjExponent hp1_lt
   by_cases h0 : (∫⁻ a, (f + g) a ^ p ∂μ) = 0
   · rw [h0, @ENNReal.zero_rpow_of_pos (1 / p) (by simp [lt_of_lt_of_le zero_lt_one hp1])]
     exact zero_le _
@@ -488,7 +487,7 @@ end ENNReal
 /-- Hölder's inequality for functions `α → ℝ≥0`. The integral of the product of two functions
 is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
 exponents. -/
-theorem NNReal.lintegral_mul_le_Lp_mul_Lq {p q : ℝ} (hpq : p.IsConjugateExponent q) {f g : α → ℝ≥0}
+theorem NNReal.lintegral_mul_le_Lp_mul_Lq {p q : ℝ} (hpq : p.IsConjExponent q) {f g : α → ℝ≥0}
     (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
     (∫⁻ a, (f * g) a ∂μ) ≤
       (∫⁻ a, (f a : ℝ≥0∞) ^ p ∂μ) ^ (1 / p) * (∫⁻ a, (g a : ℝ≥0∞) ^ q ∂μ) ^ (1 / q) := by
diff --git a/Mathlib/NumberTheory/Rayleigh.lean b/Mathlib/NumberTheory/Rayleigh.lean
index 3509b6d3d65dd..b7466191db969 100644
--- a/Mathlib/NumberTheory/Rayleigh.lean
+++ b/Mathlib/NumberTheory/Rayleigh.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Jason Yuen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jason Yuen
 -/
-import Mathlib.Data.Real.ConjugateExponents
+import Mathlib.Data.Real.ConjExponents
 import Mathlib.Data.Real.Irrational
 
 /-!
@@ -55,7 +55,7 @@ noncomputable def beattySeq' (r : ℝ) : ℤ → ℤ :=
 
 namespace Beatty
 
-variable {r s : ℝ} (hrs : r.IsConjugateExponent s) {j k : ℤ}
+variable {r s : ℝ} (hrs : r.IsConjExponent s) {j k : ℤ}
 
 /-- Let `r > 1` and `1/r + 1/s = 1`. Then `B_r` and `B'_s` are disjoint (i.e. no collision exists).
 -/
@@ -112,7 +112,7 @@ end Beatty
 
 /-- Generalization of Rayleigh's theorem on Beatty sequences. Let `r` be a real number greater
 than 1, and `1/r + 1/s = 1`. Then the complement of `B_r` is `B'_s`. -/
-theorem compl_beattySeq {r s : ℝ} (hrs : r.IsConjugateExponent s) :
+theorem compl_beattySeq {r s : ℝ} (hrs : r.IsConjExponent s) :
     {beattySeq r k | k}ᶜ = {beattySeq' s k | k} := by
   ext j
   by_cases h₁ : j ∈ {beattySeq r k | k} <;> by_cases h₂ : j ∈ {beattySeq' s k | k}
@@ -123,7 +123,7 @@ theorem compl_beattySeq {r s : ℝ} (hrs : r.IsConjugateExponent s) :
     have ⟨m, h₂₁, h₂₂⟩ := (Beatty.hit_or_miss' hrs.symm.pos).resolve_left h₂
     exact (Beatty.no_anticollision hrs ⟨j, k, m, h₁₁, h₁₂, h₂₁, h₂₂⟩).elim
 
-theorem compl_beattySeq' {r s : ℝ} (hrs : r.IsConjugateExponent s) :
+theorem compl_beattySeq' {r s : ℝ} (hrs : r.IsConjExponent s) :
     {beattySeq' r k | k}ᶜ = {beattySeq s k | k} := by
   rw [← compl_beattySeq hrs.symm, compl_compl]
 
@@ -131,7 +131,7 @@ open scoped symmDiff
 
 /-- Generalization of Rayleigh's theorem on Beatty sequences. Let `r` be a real number greater
 than 1, and `1/r + 1/s = 1`. Then `B⁺_r` and `B⁺'_s` partition the positive integers. -/
-theorem beattySeq_symmDiff_beattySeq'_pos {r s : ℝ} (hrs : r.IsConjugateExponent s) :
+theorem beattySeq_symmDiff_beattySeq'_pos {r s : ℝ} (hrs : r.IsConjExponent s) :
     {beattySeq r k | k > 0} ∆ {beattySeq' s k | k > 0} = {n | 0 < n} := by
   apply Set.eq_of_subset_of_subset
   · rintro j (⟨⟨k, hk, hjk⟩, -⟩ | ⟨⟨k, hk, hjk⟩, -⟩)
@@ -154,7 +154,7 @@ theorem beattySeq_symmDiff_beattySeq'_pos {r s : ℝ} (hrs : r.IsConjugateExpone
     Set.not_mem_compl_iff, Set.mem_compl_iff, and_self, and_self]
   exact or_not
 
-theorem beattySeq'_symmDiff_beattySeq_pos {r s : ℝ} (hrs : r.IsConjugateExponent s) :
+theorem beattySeq'_symmDiff_beattySeq_pos {r s : ℝ} (hrs : r.IsConjExponent s) :
     {beattySeq' r k | k > 0} ∆ {beattySeq s k | k > 0} = {n | 0 < n} := by
   rw [symmDiff_comm, beattySeq_symmDiff_beattySeq'_pos hrs.symm]
 
@@ -170,6 +170,6 @@ theorem Irrational.beattySeq'_pos_eq {r : ℝ} (hr : Irrational r) :
 /-- **Rayleigh's theorem** on Beatty sequences. Let `r` be an irrational number greater than 1, and
 `1/r + 1/s = 1`. Then `B⁺_r` and `B⁺_s` partition the positive integers. -/
 theorem Irrational.beattySeq_symmDiff_beattySeq_pos {r s : ℝ}
-    (hrs : r.IsConjugateExponent s) (hr : Irrational r) :
+    (hrs : r.IsConjExponent s) (hr : Irrational r) :
     {beattySeq r k | k > 0} ∆ {beattySeq s k | k > 0} = {n | 0 < n} := by
   rw [← hr.beattySeq'_pos_eq, beattySeq'_symmDiff_beattySeq_pos hrs]