NNReal.IsConjExponent.conj_eq
theorem NNReal.IsConjExponent.conj_eq : ∀ {p q : NNReal}, p.IsConjExponent q → q = p / (p - 1)
The theorem `NNReal.IsConjExponent.conj_eq` states that for any two nonnegative real numbers `p` and `q`, if `p` is a conjugate exponent of `q`, then `q` is equal to `p` divided by `p - 1`.
More concisely: If `p` is a conjugate exponent of `q` in the nonnegative real numbers, then `q = p / (p - 1)`.
|
Real.IsConjExponent.nonneg
theorem Real.IsConjExponent.nonneg : ∀ {p q : ℝ}, p.IsConjExponent q → 0 ≤ p
This theorem named `Real.IsConjExponent.nonneg` states that if `p` and `q` are real numbers such that `p` is the conjugate exponent of `q`, then `p` is nonnegative, i.e., `p` is greater than or equal to zero.
More concisely: If `p` is the conjugate exponent of a real number `q`, then `p` is nonnegative.
|
Real.IsConjExponent.conj_eq
theorem Real.IsConjExponent.conj_eq : ∀ {p q : ℝ}, p.IsConjExponent q → q = p / (p - 1)
The theorem `Real.IsConjExponent.conj_eq` states that for any two real numbers `p` and `q`, if `p` and `q` are conjugate exponents (as defined by the relation `Real.IsConjExponent p q`), then `q` is equal to `p` divided by `p - 1`. This relationship is a key aspect of the definition of conjugate exponents in mathematical analysis.
More concisely: If `p` and `q` are conjugate exponents in the real numbers, then `q = p / (p - 1)`.
|
Real.IsConjExponent.ne_zero
theorem Real.IsConjExponent.ne_zero : ∀ {p q : ℝ}, p.IsConjExponent q → p ≠ 0
This theorem states that for any two real numbers `p` and `q`, if `q` is the conjugate exponent of `p` (as defined by the `Real.IsConjExponent` property), then `p` cannot be zero. This theorem helps ensure that the operations using the concept of conjugate exponent won't encounter issues with division by zero or other undefined mathematical behavior.
More concisely: If `p` is a real number and `q` is its conjugate exponent (as defined by `Real.IsConjExponent` property), then `p` is non-zero.
|
Real.IsConjExponent.pos
theorem Real.IsConjExponent.pos : ∀ {p q : ℝ}, p.IsConjExponent q → 0 < p
This theorem states that for any two real numbers `p` and `q`, if `p` and `q` are conjugate exponents (as defined by the `Real.IsConjExponent` predicate), then `p` must be greater than zero. Essentially, this is a property about the relationship between conjugate exponents in real numbers.
More concisely: If `p` and `q` are real numbers such that they are conjugate exponents (`Real.IsConjExponent p q` holds), then `p` is positive (`0 < p`).
|
Real.IsConjExponent.inv_nonneg
theorem Real.IsConjExponent.inv_nonneg : ∀ {p q : ℝ}, p.IsConjExponent q → 0 ≤ p⁻¹
This theorem states that for any real numbers `p` and `q`, if `p` and `q` are conjugate exponents, then the inverse of `p` is nonnegative. In mathematical terms, this means that if `p` and `q` satisfy the condition $1/p + 1/q = 1$, then $0 \leq 1/p$.
More concisely: If real numbers `p` and `q` are conjugate exponents, then the inverse of `p` is nonnegative (i.e., 1/p ≥ 0).
|
Real.IsConjExponent.symm
theorem Real.IsConjExponent.symm : ∀ {p q : ℝ}, p.IsConjExponent q → q.IsConjExponent p
This theorem states that for any two real numbers `p` and `q`, if `p` and `q` are conjugate exponents, then `q` and `p` are also conjugate exponents. That is, the "conjugate exponent" relation is symmetric. In other words, the relation "being conjugate exponents" is reciprocally valid between any pair of real numbers.
More concisely: If real numbers `p` and `q` are conjugate exponents, then `q` and `p` are also conjugate exponents. (The relation "being conjugate exponents" is symmetric.)
|
NNReal.IsConjExponent.coe
theorem NNReal.IsConjExponent.coe : ∀ {p q : NNReal}, p.IsConjExponent q → (↑p).IsConjExponent ↑q
This theorem states that for all nonnegative real numbers `p` and `q` (which are represented as `NNReal`), if `p` is a conjugate exponent of `q` (expressed as `p.IsConjExponent q`), then the real number equivalents of `p` and `q` (represented as `↑p` and `↑q` respectively) also share the same property, that is, the real number equivalent of `p` is a conjugate exponent of the real number equivalent of `q` (expressed as `Real.IsConjExponent ↑p ↑q`). In other words, the property of being conjugate exponents is preserved when nonnegative real numbers are converted to real numbers.
More concisely: If `p` and `q` are nonnegative real numbers with `p` a conjugate exponent of `q`, then `↑p` and `↑q` are real numbers with `↑p` a conjugate exponent of `↑q`.
|
NNReal.IsConjExponent.pos
theorem NNReal.IsConjExponent.pos : ∀ {p q : NNReal}, p.IsConjExponent q → 0 < p
This theorem states that for any two nonnegative real numbers `p` and `q`, if `p` is the conjugate exponent of `q`, then `p` is strictly greater than zero.
More concisely: For any nonnegative real number `q` with conjugate exponent `p`, `p` strictly exceeds zero.
|