Documentation

Mathlib.Data.Real.ConjExponents

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 #

TODO #

theorem Real.isConjExponent_iff (p : ) (q : ) :
p.IsConjExponent q 1 < p p⁻¹ + q⁻¹ = 1
structure Real.IsConjExponent (p : ) (q : ) :

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.

Instances For
    theorem Real.IsConjExponent.one_lt {p : } {q : } (self : p.IsConjExponent q) :
    1 < p
    theorem Real.IsConjExponent.inv_add_inv_conj {p : } {q : } (self : p.IsConjExponent q) :

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

    Equations
    • p.conjExponent = p / (p - 1)
    Instances For
      theorem Real.IsConjExponent.pos {p : } {q : } (h : p.IsConjExponent q) :
      0 < p
      theorem Real.IsConjExponent.nonneg {p : } {q : } (h : p.IsConjExponent q) :
      0 p
      theorem Real.IsConjExponent.ne_zero {p : } {q : } (h : p.IsConjExponent q) :
      p 0
      theorem Real.IsConjExponent.sub_one_pos {p : } {q : } (h : p.IsConjExponent q) :
      0 < p - 1
      theorem Real.IsConjExponent.sub_one_ne_zero {p : } {q : } (h : p.IsConjExponent q) :
      p - 1 0
      theorem Real.IsConjExponent.inv_pos {p : } {q : } (h : p.IsConjExponent q) :
      0 < p⁻¹
      theorem Real.IsConjExponent.inv_nonneg {p : } {q : } (h : p.IsConjExponent q) :
      theorem Real.IsConjExponent.inv_ne_zero {p : } {q : } (h : p.IsConjExponent q) :
      theorem Real.IsConjExponent.one_div_pos {p : } {q : } (h : p.IsConjExponent q) :
      0 < 1 / p
      theorem Real.IsConjExponent.one_div_nonneg {p : } {q : } (h : p.IsConjExponent q) :
      0 1 / p
      theorem Real.IsConjExponent.one_div_ne_zero {p : } {q : } (h : p.IsConjExponent q) :
      1 / p 0
      theorem Real.IsConjExponent.conj_eq {p : } {q : } (h : p.IsConjExponent q) :
      q = p / (p - 1)
      theorem Real.IsConjExponent.conjExponent_eq {p : } {q : } (h : p.IsConjExponent q) :
      p.conjExponent = q
      theorem Real.IsConjExponent.one_sub_inv {p : } {q : } (h : p.IsConjExponent q) :
      theorem Real.IsConjExponent.inv_sub_one {p : } {q : } (h : p.IsConjExponent q) :
      theorem Real.IsConjExponent.sub_one_mul_conj {p : } {q : } (h : p.IsConjExponent q) :
      (p - 1) * q = p
      theorem Real.IsConjExponent.mul_eq_add {p : } {q : } (h : p.IsConjExponent q) :
      p * q = p + q
      theorem Real.IsConjExponent.symm {p : } {q : } (h : p.IsConjExponent q) :
      q.IsConjExponent p
      theorem Real.IsConjExponent.div_conj_eq_sub_one {p : } {q : } (h : p.IsConjExponent q) :
      p / q = p - 1
      theorem Real.IsConjExponent.inv_inv {a : } {b : } (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
      a⁻¹.IsConjExponent b⁻¹
      theorem Real.IsConjExponent.inv_one_sub_inv {a : } (ha₀ : 0 < a) (ha₁ : a < 1) :
      a⁻¹.IsConjExponent (1 - a)⁻¹
      theorem Real.IsConjExponent.one_sub_inv_inv {a : } (ha₀ : 0 < a) (ha₁ : a < 1) :
      (1 - a)⁻¹.IsConjExponent a⁻¹
      theorem Real.isConjExponent_comm {p : } {q : } :
      p.IsConjExponent q q.IsConjExponent p
      theorem Real.isConjExponent_iff_eq_conjExponent {p : } {q : } (hp : 1 < p) :
      p.IsConjExponent q q = p / (p - 1)
      theorem Real.IsConjExponent.conjExponent {p : } (h : 1 < p) :
      p.IsConjExponent p.conjExponent
      theorem Real.isConjExponent_one_div {a : } {b : } (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
      (1 / a).IsConjExponent (1 / b)
      theorem NNReal.isConjExponent_iff (p : NNReal) (q : NNReal) :
      p.IsConjExponent q 1 < p p⁻¹ + q⁻¹ = 1
      structure NNReal.IsConjExponent (p : NNReal) (q : 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.

      Instances For
        theorem NNReal.IsConjExponent.one_lt {p : NNReal} {q : NNReal} (self : p.IsConjExponent q) :
        1 < p
        theorem NNReal.IsConjExponent.inv_add_inv_conj {p : NNReal} {q : NNReal} (self : p.IsConjExponent q) :
        noncomputable def NNReal.conjExponent (p : NNReal) :

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

        Equations
        • p.conjExponent = p / (p - 1)
        Instances For
          @[simp]
          theorem NNReal.isConjExponent_coe {p : NNReal} {q : NNReal} :
          (↑p).IsConjExponent q p.IsConjExponent q
          theorem NNReal.IsConjExponent.coe {p : NNReal} {q : NNReal} :
          p.IsConjExponent q(↑p).IsConjExponent q

          Alias of the reverse direction of NNReal.isConjExponent_coe.

          theorem NNReal.IsConjExponent.one_le {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          1 p
          theorem NNReal.IsConjExponent.pos {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          0 < p
          theorem NNReal.IsConjExponent.ne_zero {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          p 0
          theorem NNReal.IsConjExponent.sub_one_pos {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          0 < p - 1
          theorem NNReal.IsConjExponent.sub_one_ne_zero {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          p - 1 0
          theorem NNReal.IsConjExponent.inv_pos {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          0 < p⁻¹
          theorem NNReal.IsConjExponent.inv_ne_zero {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          theorem NNReal.IsConjExponent.one_sub_inv {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          theorem NNReal.IsConjExponent.conj_eq {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          q = p / (p - 1)
          theorem NNReal.IsConjExponent.conjExponent_eq {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          p.conjExponent = q
          theorem NNReal.IsConjExponent.sub_one_mul_conj {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          (p - 1) * q = p
          theorem NNReal.IsConjExponent.mul_eq_add {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          p * q = p + q
          theorem NNReal.IsConjExponent.symm {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          q.IsConjExponent p
          theorem NNReal.IsConjExponent.div_conj_eq_sub_one {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          p / q = p - 1
          theorem NNReal.IsConjExponent.inv_add_inv_conj_ennreal {p : NNReal} {q : NNReal} (h : p.IsConjExponent q) :
          p⁻¹ + q⁻¹ = 1
          theorem NNReal.IsConjExponent.inv_inv {a : NNReal} {b : NNReal} (ha : a 0) (hb : b 0) (hab : a + b = 1) :
          a⁻¹.IsConjExponent b⁻¹
          theorem NNReal.IsConjExponent.inv_one_sub_inv {a : NNReal} (ha₀ : a 0) (ha₁ : a < 1) :
          a⁻¹.IsConjExponent (1 - a)⁻¹
          theorem NNReal.IsConjExponent.one_sub_inv_inv {a : NNReal} (ha₀ : a 0) (ha₁ : a < 1) :
          (1 - a)⁻¹.IsConjExponent a⁻¹
          theorem NNReal.isConjExponent_comm {p : NNReal} {q : NNReal} :
          p.IsConjExponent q q.IsConjExponent p
          theorem NNReal.isConjExponent_iff_eq_conjExponent {p : NNReal} {q : NNReal} (h : 1 < p) :
          p.IsConjExponent q q = p / (p - 1)
          theorem NNReal.IsConjExponent.conjExponent {p : NNReal} (h : 1 < p) :
          p.IsConjExponent p.conjExponent
          theorem Real.IsConjExponent.toNNReal {p : } {q : } (hpq : p.IsConjExponent q) :
          p.toNNReal.IsConjExponent q.toNNReal
          theorem ENNReal.isConjExponent_iff (p : ENNReal) (q : ENNReal) :
          p.IsConjExponent q p⁻¹ + q⁻¹ = 1

          Two extended nonnegative real exponents p, q are conjugate and satisfy the equality 1/p + 1/q = 1. This condition shows up in many theorems in analysis, notably related to L^p norms. Note that we permit one of the exponents to be and the other 1.

          Instances For
            theorem ENNReal.IsConjExponent.inv_add_inv_conj {p : ENNReal} {q : ENNReal} (self : p.IsConjExponent q) :
            noncomputable def ENNReal.conjExponent (p : ENNReal) :

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

            Equations
            Instances For
              theorem ENNReal.coe_conjExponent {p : NNReal} (hp : 1 < p) :
              p.conjExponent = (↑p).conjExponent
              @[simp]
              theorem ENNReal.isConjExponent_coe {p : NNReal} {q : NNReal} :
              (↑p).IsConjExponent q p.IsConjExponent q
              theorem NNReal.IsConjExponent.coe_ennreal {p : NNReal} {q : NNReal} :
              p.IsConjExponent q(↑p).IsConjExponent q

              Alias of the reverse direction of ENNReal.isConjExponent_coe.

              theorem ENNReal.IsConjExponent.conjExponent {p : ENNReal} (hp : 1 p) :
              p.IsConjExponent p.conjExponent
              theorem ENNReal.IsConjExponent.symm {p : ENNReal} {q : ENNReal} (h : p.IsConjExponent q) :
              q.IsConjExponent p
              theorem ENNReal.IsConjExponent.one_le {p : ENNReal} {q : ENNReal} (h : p.IsConjExponent q) :
              1 p
              theorem ENNReal.IsConjExponent.pos {p : ENNReal} {q : ENNReal} (h : p.IsConjExponent q) :
              0 < p
              theorem ENNReal.IsConjExponent.ne_zero {p : ENNReal} {q : ENNReal} (h : p.IsConjExponent q) :
              p 0
              theorem ENNReal.IsConjExponent.one_sub_inv {p : ENNReal} {q : ENNReal} (h : p.IsConjExponent q) :
              theorem ENNReal.IsConjExponent.conjExponent_eq {p : ENNReal} {q : ENNReal} (h : p.IsConjExponent q) :
              p.conjExponent = q
              theorem ENNReal.IsConjExponent.conj_eq {p : ENNReal} {q : ENNReal} (h : p.IsConjExponent q) :
              q = 1 + (p - 1)⁻¹
              theorem ENNReal.IsConjExponent.mul_eq_add {p : ENNReal} {q : ENNReal} (h : p.IsConjExponent q) :
              p * q = p + q
              theorem ENNReal.IsConjExponent.div_conj_eq_sub_one {p : ENNReal} {q : ENNReal} (h : p.IsConjExponent q) :
              p / q = p - 1
              theorem ENNReal.IsConjExponent.inv_inv {a : ENNReal} {b : ENNReal} (hab : a + b = 1) :
              a⁻¹.IsConjExponent b⁻¹
              theorem ENNReal.IsConjExponent.inv_one_sub_inv {a : ENNReal} (ha : a 1) :
              a⁻¹.IsConjExponent (1 - a)⁻¹
              theorem ENNReal.IsConjExponent.one_sub_inv_inv {a : ENNReal} (ha : a 1) :
              (1 - a)⁻¹.IsConjExponent a⁻¹
              theorem ENNReal.IsConjExponent.top_one :
              .IsConjExponent 1
              theorem ENNReal.isConjExponent_comm {p : ENNReal} {q : ENNReal} :
              p.IsConjExponent q q.IsConjExponent p
              theorem ENNReal.isConjExponent_iff_eq_conjExponent {p : ENNReal} {q : ENNReal} (hp : 1 p) :
              p.IsConjExponent q q = 1 + (p - 1)⁻¹