Documentation

Mathlib.Data.Real.ConjExponents

Real conjugate exponents #

This file defines Hölder triple and Hölder conjugate exponents in and ℝ≥0. Real numbers p, q and r form a Hölder triple if 0 < p and 0 < q and p⁻¹ + q⁻¹ = r⁻¹ (which of course implies 0 < r). We say p and q are Hölder conjugate if p, q and 1 are a Hölder triple. In this case, 1 < p and 1 < q. This property shows up often in analysis, especially when dealing with L^p spaces.

These notions mimic the same notions for extended nonnegative reals where p q r : ℝ≥0∞ are allowed to take the values 0 and .

Main declarations #

TODO #

structure Real.HolderTriple (p q r : ) :

Real numbers p q r : ℝ are said to be a Hölder triple if p and q are positive and p⁻¹ + q⁻¹ = r⁻¹.

Instances For
    theorem Real.holderTriple_iff (p q r : ) :
    p.HolderTriple q r p⁻¹ + q⁻¹ = r⁻¹ 0 < p 0 < q
    @[reducible, inline]
    abbrev Real.HolderConjugate (p q : ) :

    Real numbers p q : ℝ are Hölder conjugate if they are positive and satisfy the equality p⁻¹ + q⁻¹ = 1. This is an abbreviation for Real.HolderTriple p q 1. This condition shows up in many theorems in analysis, notably related to L^p norms.

    It is equivalent that 1 < p and p⁻¹ + q⁻¹ = 1. See Real.holderConjugate_iff.

    Equations
    Instances For

      The conjugate exponent of p is q = p / (p-1), so that p⁻¹ + q⁻¹ = 1.

      Equations
      Instances For
        theorem Real.HolderTriple.of_pos {p q : } (hp : 0 < p) (hq : 0 < q) :
        theorem Real.HolderTriple.symm {p q r : } (h : p.HolderTriple q r) :
        theorem Real.HolderTriple.pos {p q r : } (h : p.HolderTriple q r) :
        0 < p
        theorem Real.HolderTriple.nonneg {p q r : } (h : p.HolderTriple q r) :
        0 p
        theorem Real.HolderTriple.ne_zero {p q r : } (h : p.HolderTriple q r) :
        p 0
        theorem Real.HolderTriple.inv_pos {p q r : } (h : p.HolderTriple q r) :
        0 < p⁻¹
        theorem Real.HolderTriple.inv_nonneg {p q r : } (h : p.HolderTriple q r) :
        theorem Real.HolderTriple.one_div_pos {p q r : } (h : p.HolderTriple q r) :
        0 < 1 / p
        theorem Real.HolderTriple.one_div_nonneg {p q r : } (h : p.HolderTriple q r) :
        0 1 / p
        theorem Real.HolderTriple.one_div_ne_zero {p q r : } (h : p.HolderTriple q r) :
        1 / p 0
        theorem Real.HolderTriple.pos' {p q r : } (h : p.HolderTriple q r) :
        0 < r

        For r, instead of p

        theorem Real.HolderTriple.nonneg' {p q r : } (h : p.HolderTriple q r) :
        0 r

        For r, instead of p

        theorem Real.HolderTriple.ne_zero' {p q r : } (h : p.HolderTriple q r) :
        r 0

        For r, instead of p

        theorem Real.HolderTriple.inv_pos' {p q r : } (h : p.HolderTriple q r) :
        0 < r⁻¹

        For r, instead of p

        theorem Real.HolderTriple.inv_nonneg' {p q r : } (h : p.HolderTriple q r) :

        For r, instead of p

        theorem Real.HolderTriple.inv_ne_zero' {p q r : } (h : p.HolderTriple q r) :

        For r, instead of p

        theorem Real.HolderTriple.one_div_pos' {p q r : } (h : p.HolderTriple q r) :
        0 < 1 / r

        For r, instead of p

        theorem Real.HolderTriple.one_div_nonneg' {p q r : } (h : p.HolderTriple q r) :
        0 1 / r

        For r, instead of p

        theorem Real.HolderTriple.one_div_ne_zero' {p q r : } (h : p.HolderTriple q r) :
        1 / r 0

        For r, instead of p

        theorem Real.HolderTriple.one_div_add_one_div {p q r : } (h : p.HolderTriple q r) :
        1 / p + 1 / q = 1 / r
        theorem Real.HolderTriple.one_div_eq {p q r : } (h : p.HolderTriple q r) :
        1 / r = 1 / p + 1 / q
        theorem Real.HolderTriple.lt {p q r : } (h : p.HolderTriple q r) :
        r < p
        theorem Real.HolderConjugate.conjugate_eq {p q : } (h : p.HolderConjugate q) :
        q = p / (p - 1)
        theorem Real.HolderConjugate.mul_eq_add {p q : } (h : p.HolderConjugate q) :
        p * q = p + q
        theorem Real.HolderConjugate.inv_inv {a b : } (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
        theorem Real.HolderConjugate.inv_one_sub_inv {a : } (ha₀ : 0 < a) (ha₁ : a < 1) :
        theorem Real.HolderConjugate.one_sub_inv_inv {a : } (ha₀ : 0 < a) (ha₁ : a < 1) :
        theorem Real.holderConjugate_iff_eq_conjExponent {p q : } (hp : 1 < p) :
        p.HolderConjugate q q = p / (p - 1)
        theorem Real.holderConjugate_one_div {a b : } (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
        (1 / a).HolderConjugate (1 / b)
        structure NNReal.HolderTriple (p q r : NNReal) :

        Nonnegative real numbers p q r : ℝ≥0 are said to be a Hölder triple if p and q are positive and p⁻¹ + q⁻¹ = r⁻¹.

        Instances For
          @[reducible, inline]

          Nonnegative real numbers p q : ℝ≥0 are Hölder conjugate if they are positive and satisfy the equality p⁻¹ + q⁻¹ = 1. This is an abbreviation for NNReal.HolderTriple p q 1. This condition shows up in many theorems in analysis, notably related to L^p norms.

          It is equivalent that 1 < p and p⁻¹ + q⁻¹ = 1. See NNReal.holderConjugate_iff.

          Equations
          Instances For

            The conjugate exponent of p is q = p/(p-1), so that p⁻¹ + q⁻¹ = 1.

            Equations
            Instances For
              @[simp]
              theorem NNReal.holderTriple_coe_iff {p q r : NNReal} :
              (↑p).HolderTriple q r p.HolderTriple q r
              theorem NNReal.HolderTriple.coe {p q r : NNReal} :
              p.HolderTriple q r(↑p).HolderTriple q r

              Alias of the reverse direction of NNReal.holderTriple_coe_iff.

              Alias of the reverse direction of NNReal.holderConjugate_coe_iff.

              theorem NNReal.HolderTriple.of_pos {p q : NNReal} (hp : 0 < p) (hq : 0 < q) :
              theorem NNReal.HolderTriple.symm {p q r : NNReal} (h : p.HolderTriple q r) :
              theorem NNReal.HolderTriple.pos {p q r : NNReal} (h : p.HolderTriple q r) :
              0 < p
              theorem NNReal.HolderTriple.nonneg {p q r : NNReal} (h : p.HolderTriple q r) :
              0 p
              theorem NNReal.HolderTriple.ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :
              p 0
              theorem NNReal.HolderTriple.inv_pos {p q r : NNReal} (h : p.HolderTriple q r) :
              0 < p⁻¹
              theorem NNReal.HolderTriple.one_div_pos {p q r : NNReal} (h : p.HolderTriple q r) :
              0 < 1 / p
              theorem NNReal.HolderTriple.pos' {p q r : NNReal} (h : p.HolderTriple q r) :
              0 < r

              For r, instead of p

              theorem NNReal.HolderTriple.nonneg' {p q r : NNReal} (h : p.HolderTriple q r) :
              0 r

              For r, instead of p

              theorem NNReal.HolderTriple.ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) :
              r 0

              For r, instead of p

              theorem NNReal.HolderTriple.inv_pos' {p q r : NNReal} (h : p.HolderTriple q r) :
              0 < r⁻¹

              For r, instead of p

              theorem NNReal.HolderTriple.inv_nonneg' {p q r : NNReal} (h : p.HolderTriple q r) :

              For r, instead of p

              For r, instead of p

              theorem NNReal.HolderTriple.one_div_pos' {p q r : NNReal} (h : p.HolderTriple q r) :
              0 < 1 / r

              For r, instead of p

              theorem NNReal.HolderTriple.one_div_nonneg' {p q r : NNReal} (h : p.HolderTriple q r) :
              0 1 / r

              For r, instead of p

              theorem NNReal.HolderTriple.one_div_ne_zero' {p q r : NNReal} (h : p.HolderTriple q r) :
              1 / r 0

              For r, instead of p

              theorem NNReal.HolderTriple.one_div_add_one_div {p q r : NNReal} (h : p.HolderTriple q r) :
              1 / p + 1 / q = 1 / r
              theorem NNReal.HolderTriple.one_div_eq {p q r : NNReal} (h : p.HolderTriple q r) :
              1 / r = 1 / p + 1 / q
              theorem NNReal.HolderTriple.lt {p q r : NNReal} (h : p.HolderTriple q r) :
              r < p
              theorem NNReal.HolderConjugate.inv_inv {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
              theorem NNReal.HolderConjugate.inv_one_sub_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :
              theorem NNReal.HolderConjugate.one_sub_inv_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :
              theorem NNReal.holderConjugate_one_div {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
              (1 / a).HolderConjugate (1 / b)
              noncomputable def ENNReal.conjExponent (p : ENNReal) :

              The conjugate exponent of p is q = 1 + (p - 1)⁻¹, so that p⁻¹ + q⁻¹ = 1.

              Equations
              Instances For
                theorem ENNReal.coe_conjExponent {p : NNReal} (hp : 1 < p) :
                @[simp]
                theorem ENNReal.holderTriple_coe_iff {p q r : NNReal} (hr : r 0) :
                (↑p).HolderTriple q r p.HolderTriple q r
                theorem NNReal.HolderTriple.coe_ennreal {p q r : NNReal} (hr : r 0) :
                p.HolderTriple q r(↑p).HolderTriple q r

                Alias of the reverse direction of ENNReal.holderTriple_coe_iff.

                Alias of the reverse direction of ENNReal.holderConjugate_coe_iff.

                theorem ENNReal.HolderTriple.toReal {p q : ENNReal} (r : ENNReal) (hp : 0 < p.toReal) (hq : 0 < q.toReal) [p.HolderTriple q r] :
                @[deprecated Real.HolderConjugate (since := "2025-03-14")]

                Alias of Real.HolderConjugate.


                Real numbers p q : ℝ are Hölder conjugate if they are positive and satisfy the equality p⁻¹ + q⁻¹ = 1. This is an abbreviation for Real.HolderTriple p q 1. This condition shows up in many theorems in analysis, notably related to L^p norms.

                It is equivalent that 1 < p and p⁻¹ + q⁻¹ = 1. See Real.holderConjugate_iff.

                Equations
                Instances For
                  @[deprecated Real.holderConjugate_iff (since := "2025-03-14")]

                  Alias of Real.holderConjugate_iff.

                  @[deprecated Real.HolderTriple.lt (since := "2025-03-14")]
                  theorem Real.IsConjExponent.one_lt {p q r : } (h : p.HolderTriple q r) :
                  r < p

                  Alias of Real.HolderTriple.lt.

                  @[deprecated Real.HolderConjugate.inv_add_inv_eq_one (since := "2025-03-14")]

                  Alias of Real.HolderConjugate.inv_add_inv_eq_one.

                  @[deprecated Real.HolderTriple.pos (since := "2025-03-14")]
                  theorem Real.IsConjExponent.pos {p q r : } (h : p.HolderTriple q r) :
                  0 < p

                  Alias of Real.HolderTriple.pos.

                  @[deprecated Real.HolderTriple.nonneg (since := "2025-03-14")]
                  theorem Real.IsConjExponent.nonneg {p q r : } (h : p.HolderTriple q r) :
                  0 p

                  Alias of Real.HolderTriple.nonneg.

                  @[deprecated Real.HolderTriple.ne_zero (since := "2025-03-14")]
                  theorem Real.IsConjExponent.ne_zero {p q r : } (h : p.HolderTriple q r) :
                  p 0

                  Alias of Real.HolderTriple.ne_zero.

                  @[deprecated Real.HolderConjugate.sub_one_pos (since := "2025-03-14")]
                  theorem Real.IsConjExponent.sub_one_pos {p q : } (h : p.HolderConjugate q) :
                  0 < p - 1

                  Alias of Real.HolderConjugate.sub_one_pos.

                  @[deprecated Real.HolderConjugate.sub_one_ne_zero (since := "2025-03-14")]

                  Alias of Real.HolderConjugate.sub_one_ne_zero.

                  @[deprecated Real.HolderTriple.inv_pos (since := "2025-03-14")]
                  theorem Real.IsConjExponent.inv_pos {p q r : } (h : p.HolderTriple q r) :
                  0 < p⁻¹

                  Alias of Real.HolderTriple.inv_pos.

                  @[deprecated Real.HolderTriple.inv_nonneg (since := "2025-03-14")]
                  theorem Real.IsConjExponent.inv_nonneg {p q r : } (h : p.HolderTriple q r) :

                  Alias of Real.HolderTriple.inv_nonneg.

                  @[deprecated Real.HolderTriple.inv_ne_zero (since := "2025-03-14")]
                  theorem Real.IsConjExponent.inv_ne_zero {p q r : } (h : p.HolderTriple q r) :

                  Alias of Real.HolderTriple.inv_ne_zero.

                  @[deprecated Real.HolderTriple.one_div_pos (since := "2025-03-14")]
                  theorem Real.IsConjExponent.one_div_pos {p q r : } (h : p.HolderTriple q r) :
                  0 < 1 / p

                  Alias of Real.HolderTriple.one_div_pos.

                  @[deprecated Real.HolderTriple.one_div_nonneg (since := "2025-03-14")]
                  theorem Real.IsConjExponent.one_div_nonneg {p q r : } (h : p.HolderTriple q r) :
                  0 1 / p

                  Alias of Real.HolderTriple.one_div_nonneg.

                  @[deprecated Real.HolderTriple.one_div_ne_zero (since := "2025-03-14")]
                  theorem Real.IsConjExponent.one_div_ne_zero {p q r : } (h : p.HolderTriple q r) :
                  1 / p 0

                  Alias of Real.HolderTriple.one_div_ne_zero.

                  @[deprecated Real.HolderConjugate.conjugate_eq (since := "2025-03-14")]
                  theorem Real.IsConjExponent.conj_eq {p q : } (h : p.HolderConjugate q) :
                  q = p / (p - 1)

                  Alias of Real.HolderConjugate.conjugate_eq.

                  @[deprecated Real.HolderConjugate.conjExponent_eq (since := "2025-03-14")]

                  Alias of Real.HolderConjugate.conjExponent_eq.

                  @[deprecated Real.HolderConjugate.one_sub_inv (since := "2025-03-14")]

                  Alias of Real.HolderConjugate.one_sub_inv.

                  @[deprecated Real.HolderConjugate.inv_sub_one (since := "2025-03-14")]

                  Alias of Real.HolderConjugate.inv_sub_one.

                  @[deprecated Real.HolderConjugate.sub_one_mul_conj (since := "2025-03-14")]
                  theorem Real.IsConjExponent.sub_one_mul_conj {p q : } (h : p.HolderConjugate q) :
                  (p - 1) * q = p

                  Alias of Real.HolderConjugate.sub_one_mul_conj.

                  @[deprecated Real.HolderConjugate.mul_eq_add (since := "2025-03-14")]
                  theorem Real.IsConjExponent.mul_eq_add {p q : } (h : p.HolderConjugate q) :
                  p * q = p + q

                  Alias of Real.HolderConjugate.mul_eq_add.

                  @[deprecated Real.HolderConjugate.symm (since := "2025-03-14")]

                  Alias of Real.HolderConjugate.symm.

                  @[deprecated Real.HolderConjugate.div_conj_eq_sub_one (since := "2025-03-14")]
                  theorem Real.IsConjExponent.div_conj_eq_sub_one {p q : } (h : p.HolderConjugate q) :
                  p / q = p - 1

                  Alias of Real.HolderConjugate.div_conj_eq_sub_one.

                  @[deprecated Real.HolderConjugate.inv_inv (since := "2025-03-14")]
                  theorem Real.IsConjExponent.inv_inv {a b : } (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

                  Alias of Real.HolderConjugate.inv_inv.

                  @[deprecated Real.HolderConjugate.inv_one_sub_inv (since := "2025-03-14")]
                  theorem Real.IsConjExponent.inv_one_sub_inv {a : } (ha₀ : 0 < a) (ha₁ : a < 1) :

                  Alias of Real.HolderConjugate.inv_one_sub_inv.

                  @[deprecated Real.HolderConjugate.one_sub_inv_inv (since := "2025-03-14")]
                  theorem Real.IsConjExponent.one_sub_inv_inv {a : } (ha₀ : 0 < a) (ha₁ : a < 1) :

                  Alias of Real.HolderConjugate.one_sub_inv_inv.

                  @[deprecated Real.HolderConjugate.inv_add_inv_ennreal (since := "2025-03-14")]

                  Alias of Real.HolderConjugate.inv_add_inv_ennreal.

                  @[deprecated Real.holderConjugate_comm (since := "2025-03-14")]

                  Alias of Real.holderConjugate_comm.

                  @[deprecated Real.holderConjugate_iff_eq_conjExponent (since := "2025-03-14")]
                  theorem Real.isConjExponent_iff_eq_conjExponent {p q : } (hp : 1 < p) :
                  p.HolderConjugate q q = p / (p - 1)

                  Alias of Real.holderConjugate_iff_eq_conjExponent.

                  @[deprecated Real.HolderConjugate.conjExponent (since := "2025-03-14")]

                  Alias of Real.HolderConjugate.conjExponent.

                  @[deprecated Real.holderConjugate_one_div (since := "2025-03-14")]
                  theorem Real.isConjExponent_one_div {a b : } (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
                  (1 / a).HolderConjugate (1 / b)

                  Alias of Real.holderConjugate_one_div.

                  @[deprecated NNReal.HolderConjugate (since := "2025-03-14")]

                  Alias of NNReal.HolderConjugate.


                  Nonnegative real numbers p q : ℝ≥0 are Hölder conjugate if they are positive and satisfy the equality p⁻¹ + q⁻¹ = 1. This is an abbreviation for NNReal.HolderTriple p q 1. This condition shows up in many theorems in analysis, notably related to L^p norms.

                  It is equivalent that 1 < p and p⁻¹ + q⁻¹ = 1. See NNReal.holderConjugate_iff.

                  Equations
                  Instances For
                    @[deprecated NNReal.holderConjugate_iff (since := "2025-03-14")]

                    Alias of NNReal.holderConjugate_iff.

                    @[deprecated NNReal.HolderTriple.lt (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.one_lt {p q r : NNReal} (h : p.HolderTriple q r) :
                    r < p

                    Alias of NNReal.HolderTriple.lt.

                    @[deprecated NNReal.HolderConjugate.inv_add_inv_eq_one (since := "2025-03-14")]

                    Alias of NNReal.HolderConjugate.inv_add_inv_eq_one.

                    @[deprecated NNReal.holderConjugate_coe_iff (since := "2025-03-14")]

                    Alias of NNReal.holderConjugate_coe_iff.

                    @[deprecated NNReal.HolderConjugate.coe (since := "2025-03-14")]

                    Alias of the reverse direction of NNReal.holderConjugate_coe_iff.


                    Alias of the reverse direction of NNReal.holderConjugate_coe_iff.

                    @[deprecated NNReal.HolderTriple.lt (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.one_le {p q r : NNReal} (h : p.HolderTriple q r) :
                    r < p

                    Alias of NNReal.HolderTriple.lt.

                    @[deprecated NNReal.HolderTriple.pos (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.pos {p q r : NNReal} (h : p.HolderTriple q r) :
                    0 < p

                    Alias of NNReal.HolderTriple.pos.

                    @[deprecated NNReal.HolderTriple.nonneg (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.nonneg {p q r : NNReal} (h : p.HolderTriple q r) :
                    0 p

                    Alias of NNReal.HolderTriple.nonneg.

                    @[deprecated NNReal.HolderTriple.ne_zero (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :
                    p 0

                    Alias of NNReal.HolderTriple.ne_zero.

                    @[deprecated NNReal.HolderConjugate.sub_one_pos (since := "2025-03-14")]

                    Alias of NNReal.HolderConjugate.sub_one_pos.

                    @[deprecated NNReal.HolderConjugate.sub_one_ne_zero (since := "2025-03-14")]

                    Alias of NNReal.HolderConjugate.sub_one_ne_zero.

                    @[deprecated NNReal.HolderTriple.inv_pos (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.inv_pos {p q r : NNReal} (h : p.HolderTriple q r) :
                    0 < p⁻¹

                    Alias of NNReal.HolderTriple.inv_pos.

                    @[deprecated NNReal.HolderTriple.inv_nonneg (since := "2025-03-14")]

                    Alias of NNReal.HolderTriple.inv_nonneg.

                    @[deprecated NNReal.HolderTriple.inv_ne_zero (since := "2025-03-14")]

                    Alias of NNReal.HolderTriple.inv_ne_zero.

                    @[deprecated NNReal.HolderTriple.one_div_pos (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.one_div_pos {p q r : NNReal} (h : p.HolderTriple q r) :
                    0 < 1 / p

                    Alias of NNReal.HolderTriple.one_div_pos.

                    @[deprecated NNReal.HolderTriple.one_div_nonneg (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.one_div_nonneg {p q r : NNReal} (h : p.HolderTriple q r) :
                    0 1 / p

                    Alias of NNReal.HolderTriple.one_div_nonneg.

                    @[deprecated NNReal.HolderTriple.one_div_ne_zero (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.one_div_ne_zero {p q r : NNReal} (h : p.HolderTriple q r) :
                    1 / p 0

                    Alias of NNReal.HolderTriple.one_div_ne_zero.

                    @[deprecated NNReal.HolderConjugate.conjugate_eq (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.conj_eq {p q : NNReal} (h : p.HolderConjugate q) :
                    q = p / (p - 1)

                    Alias of NNReal.HolderConjugate.conjugate_eq.

                    @[deprecated NNReal.HolderConjugate.conjExponent_eq (since := "2025-03-14")]

                    Alias of NNReal.HolderConjugate.conjExponent_eq.

                    @[deprecated NNReal.HolderConjugate.one_sub_inv (since := "2025-03-14")]

                    Alias of NNReal.HolderConjugate.one_sub_inv.

                    @[deprecated NNReal.HolderConjugate.sub_one_mul_conj (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.sub_one_mul_conj {p q : NNReal} (h : p.HolderConjugate q) :
                    (p - 1) * q = p

                    Alias of NNReal.HolderConjugate.sub_one_mul_conj.

                    @[deprecated NNReal.HolderConjugate.mul_eq_add (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.mul_eq_add {p q : NNReal} (h : p.HolderConjugate q) :
                    p * q = p + q

                    Alias of NNReal.HolderConjugate.mul_eq_add.

                    @[deprecated NNReal.HolderConjugate.symm (since := "2025-03-14")]

                    Alias of NNReal.HolderConjugate.symm.

                    @[deprecated NNReal.HolderConjugate.div_conj_eq_sub_one (since := "2025-03-14")]

                    Alias of NNReal.HolderConjugate.div_conj_eq_sub_one.

                    @[deprecated NNReal.HolderConjugate.inv_inv (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.inv_inv {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

                    Alias of NNReal.HolderConjugate.inv_inv.

                    @[deprecated NNReal.HolderConjugate.inv_one_sub_inv (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.inv_one_sub_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :

                    Alias of NNReal.HolderConjugate.inv_one_sub_inv.

                    @[deprecated NNReal.HolderConjugate.one_sub_inv_inv (since := "2025-03-14")]
                    theorem NNReal.IsConjExponent.one_sub_inv_inv {a : NNReal} (ha₀ : 0 < a) (ha₁ : a < 1) :

                    Alias of NNReal.HolderConjugate.one_sub_inv_inv.

                    @[deprecated NNReal.HolderConjugate.inv_add_inv_ennreal (since := "2025-03-14")]

                    Alias of NNReal.HolderConjugate.inv_add_inv_ennreal.

                    @[deprecated NNReal.holderConjugate_comm (since := "2025-03-14")]

                    Alias of NNReal.holderConjugate_comm.

                    @[deprecated NNReal.holderConjugate_iff_eq_conjExponent (since := "2025-03-14")]
                    theorem NNReal.isConjExponent_iff_eq_conjExponent {p q : NNReal} (hp : 1 < p) :
                    p.HolderConjugate q q = p / (p - 1)

                    Alias of NNReal.holderConjugate_iff_eq_conjExponent.

                    @[deprecated NNReal.HolderConjugate.conjExponent (since := "2025-03-14")]

                    Alias of NNReal.HolderConjugate.conjExponent.

                    @[deprecated NNReal.holderConjugate_one_div (since := "2025-03-14")]
                    theorem NNReal.isConjExponent_one_div {a b : NNReal} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
                    (1 / a).HolderConjugate (1 / b)

                    Alias of NNReal.holderConjugate_one_div.

                    @[deprecated Real.HolderTriple.toNNReal (since := "2025-03-14")]

                    Alias of Real.HolderTriple.toNNReal.

                    @[deprecated ENNReal.HolderConjugate (since := "2025-03-14")]

                    Alias of ENNReal.HolderConjugate.


                    An abbreviation for ENNReal.HolderTriple p q 1, this class states p⁻¹ + q⁻¹ = 1.

                    Equations
                    Instances For
                      @[deprecated ENNReal.holderConjugate_iff (since := "2025-03-14")]

                      Alias of ENNReal.holderConjugate_iff.

                      @[deprecated ENNReal.holderConjugate_coe_iff (since := "2025-03-14")]

                      Alias of ENNReal.holderConjugate_coe_iff.

                      @[deprecated NNReal.HolderConjugate.coe_ennreal (since := "2025-03-14")]

                      Alias of the reverse direction of ENNReal.holderConjugate_coe_iff.


                      Alias of the reverse direction of ENNReal.holderConjugate_coe_iff.

                      @[deprecated ENNReal.HolderConjugate.conjExponent (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.conjExponent.

                      @[deprecated ENNReal.HolderConjugate.symm (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.symm.

                      @[deprecated ENNReal.HolderTriple.le (since := "2025-03-14")]
                      theorem ENNReal.IsConjExponent.one_le (p q r : ENNReal) [p.HolderTriple q r] :
                      r p

                      Alias of ENNReal.HolderTriple.le.

                      @[deprecated ENNReal.HolderConjugate.pos (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.pos.

                      @[deprecated ENNReal.HolderConjugate.ne_zero (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.ne_zero.

                      @[deprecated ENNReal.HolderConjugate.one_sub_inv (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.one_sub_inv.

                      @[deprecated ENNReal.HolderConjugate.conjExponent_eq (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.conjExponent_eq.

                      @[deprecated ENNReal.HolderConjugate.conj_eq (since := "2025-03-14")]
                      theorem ENNReal.IsConjExponent.conj_eq {p q : ENNReal} [h : p.HolderConjugate q] :
                      q = 1 + (p - 1)⁻¹

                      Alias of ENNReal.HolderConjugate.conj_eq.

                      @[deprecated ENNReal.HolderConjugate.mul_eq_add (since := "2025-03-14")]
                      theorem ENNReal.IsConjExponent.mul_eq_add {p q : ENNReal} [h : p.HolderConjugate q] :
                      p * q = p + q

                      Alias of ENNReal.HolderConjugate.mul_eq_add.

                      @[deprecated ENNReal.HolderConjugate.div_conj_eq_sub_one (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.div_conj_eq_sub_one.

                      @[deprecated ENNReal.HolderConjugate.inv_inv (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.inv_inv.

                      @[deprecated ENNReal.HolderConjugate.inv_one_sub_inv (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.inv_one_sub_inv.

                      @[deprecated ENNReal.HolderConjugate.one_sub_inv_inv (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.one_sub_inv_inv.

                      @[deprecated ENNReal.HolderConjugate.top_one (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.top_one.

                      @[deprecated ENNReal.HolderConjugate.one_top (since := "2025-03-14")]

                      Alias of ENNReal.HolderConjugate.one_top.