Results about working with (interpolated) exponents

This files contains convenience results for working with interpolated exponents, as well as results about a particular choice of exponent that we will use for the proof of the real interpolation theorem.

theorem ENNReal.mem_sub_Ioo {q r : ENNReal} (hr : r ≠ ⊤) (hq : q ∈ Set.Ioo 0 r) : r - q ∈ Set.Ioo 0 r

theorem ENNReal.sub_toReal_of_le {t : ENNReal} (ht : t ≤ 1) : 1 - t.toReal = (1 - t).toReal

theorem ENNReal.sub_sub_toReal_of_le {t : ENNReal} (ht : t ≤ 1) : t.toReal = 1 - (1 - t).toReal

theorem ENNReal.one_sub_one_sub_eq {t : ENNReal} (ht : t ∈ Set.Ioo 0 1) : 1 - (1 - t) = t

theorem ENNReal.one_le_toReal {a : ENNReal} (ha₁ : 1 ≤ a) (ha₂ : a < ⊤) : 1 ≤ a.toReal

theorem ENNReal.coe_rpow_ne_top {a q : ℝ} (hq : 0 ≤ q) : ENNReal.ofReal a ^ q ≠ ⊤

theorem ENNReal.coe_rpow_ne_top' {a q : ℝ} (hq : 0 < q) : ENNReal.ofReal a ^ q ≠ ⊤

theorem ENNReal.coe_pow_pos {a q : ℝ} (ha : 0 < a) : 0 < ENNReal.ofReal a ^ q

theorem ENNReal.rpow_ne_top' {a : ENNReal} {q : ℝ} (ha : a ≠ 0) (ha' : a ≠ ⊤) : a ^ q ≠ ⊤

theorem ENNReal.exp_toReal_pos' {q : ENNReal} (hq : 1 ≤ q) (hq' : q < ⊤) : 0 < q.toReal

theorem ENNReal.ne_top_of_Ico {p q r : ENNReal} (hq : q ∈ Set.Ico p r) : q ≠ ⊤

theorem ENNReal.lt_top_of_Ico {p q r : ENNReal} (hq : q ∈ Set.Ico p r) : q < ⊤

theorem ENNReal.ne_top_of_Ioo {p q r : ENNReal} (hq : q ∈ Set.Ioo p r) : q ≠ ⊤

theorem ENNReal.lt_top_of_Ioo {p q r : ENNReal} (hq : q ∈ Set.Ioo p r) : q < ⊤

theorem ENNReal.toReal_mem_Ioo {t : ENNReal} (ht : t ∈ Set.Ioo 0 1) : t.toReal ∈ Set.Ioo 0 1

theorem ENNReal.ofReal_mem_Ioo_0_1 (t : ℝ) (h : t ∈ Set.Ioo 0 1) : ENNReal.ofReal t ∈ Set.Ioo 0 1

theorem ENNReal.ne_top_of_Ioc {p q r : ENNReal} (hq : q ∈ Set.Ioc p r) (hr : r < ⊤) : q ≠ ⊤

theorem ENNReal.pos_of_rb_Ioc {p q r : ENNReal} (hr : q ∈ Set.Ioc p r) : 0 < r

theorem ENNReal.pos_of_Ioo {p q r : ENNReal} (hq : q ∈ Set.Ioo p r) : 0 < q

theorem ENNReal.ne_zero_of_Ioo {p q r : ENNReal} (hq : q ∈ Set.Ioo p r) : q ≠ 0

theorem ENNReal.pos_of_Icc_1 {p q : ENNReal} (hp : p ∈ Set.Icc 1 q) : 0 < p

theorem ENNReal.pos_of_ge_1 {p : ENNReal} (hp : 1 ≤ p) : 0 < p

theorem ENNReal.pos_rb_of_Icc_1_inh {p q : ENNReal} (hp : p ∈ Set.Icc 1 q) : 0 < q

theorem ENNReal.toReal_pos_of_Ioo {q p r : ENNReal} (hp : p ∈ Set.Ioo q r) : 0 < p.toReal

theorem ENNReal.toReal_ne_zero_of_Ioo {q p r : ENNReal} (hp : p ∈ Set.Ioo q r) : p.toReal ≠ 0

theorem ENNReal.eq_of_rpow_eq (a b : ENNReal) (c : ℝ) (hc : c ≠ 0) (h : a ^ c = b ^ c) : a = b

theorem ENNReal.le_of_rpow_le {a b : ENNReal} {c : ℝ} (hc : 0 < c) (h : a ^ c ≤ b ^ c) : a ≤ b

theorem ENNReal.coe_inv_exponent {p₀ : ENNReal} (hp₀ : 0 < p₀) : ENNReal.ofReal p₀⁻¹.toReal = p₀⁻¹

Convenience results for working with (interpolated) exponents

theorem ComputationsInterpolatedExponents.ENNReal_preservation_positivity₀ {p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hpq : p ≠ ⊤ ∨ q ≠ ⊤) : 0 < (1 - t) * p⁻¹ + t * q⁻¹

theorem ComputationsInterpolatedExponents.ENNReal_preservation_positivity {p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hpq : p ≠ q) : 0 < (1 - t) * p⁻¹ + t * q⁻¹

theorem ComputationsInterpolatedExponents.ENNReal_preservation_positivity' {p₀ p₁ p t : ENNReal} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (ht : t ≠ ⊤) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : 0 < p

theorem ComputationsInterpolatedExponents.interp_exp_ne_top {p₀ p₁ p t : ENNReal} (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p ≠ ⊤

theorem ComputationsInterpolatedExponents.interp_exp_ne_top' {p₀ p₁ p t : ENNReal} (hp₀p₁ : p₀ ≠ ⊤ ∨ p₁ ≠ ⊤) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p ≠ ⊤

theorem ComputationsInterpolatedExponents.interp_exp_eq {p₀ p₁ p t : ENNReal} (hp₀p₁ : p₀ = p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p₀ = p

theorem ComputationsInterpolatedExponents.interp_exp_lt_top {p₀ p₁ p t : ENNReal} (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p < ⊤

theorem ComputationsInterpolatedExponents.interp_exp_lt_top' {p₀ p₁ p t : ENNReal} (hp₀p₁ : p₀ ≠ ⊤ ∨ p₁ ≠ ⊤) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p < ⊤

theorem ComputationsInterpolatedExponents.interp_exp_between {p₀ p₁ p t : ENNReal} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ < p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p ∈ Set.Ioo p₀ p₁

theorem ComputationsInterpolatedExponents.one_le_interp_exp_aux {p₀ p₁ p t : ENNReal} (hp₀ : 1 ≤ p₀) (hp₁ : 1 ≤ p₁) (hp₀p₁ : p₀ < p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : 1 ≤ p

theorem ComputationsInterpolatedExponents.switch_exponents {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p⁻¹ = (1 - (1 - t)) * p₁⁻¹ + (1 - t) * p₀⁻¹

theorem ComputationsInterpolatedExponents.one_le_interp {p₀ p₁ p t : ENNReal} (hp₀ : 1 ≤ p₀) (hp₁ : 1 ≤ p₁) (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : 1 ≤ p

theorem ComputationsInterpolatedExponents.one_le_interp_toReal {p₀ p₁ p t : ENNReal} (hp₀ : 1 ≤ p₀) (hp₁ : 1 ≤ p₁) (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : 1 ≤ p.toReal

theorem ComputationsInterpolatedExponents.exp_toReal_ne_zero_of_Ico {q p : ENNReal} (hq : q ∈ Set.Ico 1 p) : q.toReal ≠ 0

theorem ComputationsInterpolatedExponents.inv_of_interpolated_pos' {p₀ p₁ p t : ENNReal} (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : 0 < p⁻¹

theorem ComputationsInterpolatedExponents.interpolated_pos' {p₀ p₁ p t : ENNReal} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (ht : t ≠ ⊤) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : 0 < p

theorem ComputationsInterpolatedExponents.exp_toReal_pos {p₀ : ENNReal} (hp₀ : 0 < p₀) (hp₀' : p₀ ≠ ⊤) : 0 < p₀.toReal

theorem ComputationsInterpolatedExponents.interp_exp_in_Ioo_zero_top {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ ⊤ ∨ p₁ ≠ ⊤) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p ∈ Set.Ioo 0 ⊤

theorem ComputationsInterpolatedExponents.inv_toReal_pos_of_ne_top {p₀ : ENNReal} (hp₀ : 0 < p₀) (hp' : p₀ ≠ ⊤) : 0 < p₀⁻¹.toReal

theorem ComputationsInterpolatedExponents.inv_toReal_ne_zero_of_ne_top {p₀ : ENNReal} (hp₀ : 0 < p₀) (hp' : p₀ ≠ ⊤) : p₀⁻¹.toReal ≠ 0

theorem ComputationsInterpolatedExponents.interp_exp_toReal_pos {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : 0 < p.toReal

theorem ComputationsInterpolatedExponents.interp_exp_toReal_pos' {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hp₀p₁ : p₀ ≠ ⊤ ∨ p₁ ≠ ⊤) : 0 < p.toReal

theorem ComputationsInterpolatedExponents.interp_exp_inv_pos {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : 0 < p⁻¹.toReal

theorem ComputationsInterpolatedExponents.interp_exp_inv_ne_zero {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p⁻¹.toReal ≠ 0

theorem ComputationsInterpolatedExponents.preservation_interpolation {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p⁻¹.toReal = (1 - t).toReal * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal

theorem ComputationsInterpolatedExponents.preservation_positivity_inv_toReal {p₀ p₁ t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) : 0 < (1 - t.toReal) * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal

theorem ComputationsInterpolatedExponents.ne_inv_toReal_exponents {p₀ p₁ : ENNReal} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) : p₀⁻¹.toReal ≠ p₁⁻¹.toReal

theorem ComputationsInterpolatedExponents.ne_inv_toReal_exp_interp_exp {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p₀⁻¹.toReal ≠ p⁻¹.toReal

theorem ComputationsInterpolatedExponents.ne_sub_toReal_exp {p₀ p₁ : ENNReal} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) : p₁⁻¹.toReal - p₀⁻¹.toReal ≠ 0

theorem ComputationsInterpolatedExponents.ne_toReal_exp_interp_exp {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p₀.toReal ≠ p.toReal

theorem ComputationsInterpolatedExponents.ne_toReal_exp_interp_exp₁ {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p.toReal ≠ p₁.toReal

theorem ComputationsInterpolatedExponents.ofReal_inv_interp_sub_exp_pos₁ {q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) : ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ > 0

theorem ComputationsInterpolatedExponents.ofReal_inv_interp_sub_exp_pos₀ {q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) : ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹ > 0

theorem ComputationsInterpolatedExponents.exp_lt_iff {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p < p₀ ↔ p₁ < p₀

theorem ComputationsInterpolatedExponents.exp_gt_iff {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p₀ < p ↔ p₀ < p₁

theorem ComputationsInterpolatedExponents.exp_lt_exp_gt_iff {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p < p₀ ↔ p₁ < p

theorem ComputationsInterpolatedExponents.exp_gt_exp_lt_iff {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p₀ < p ↔ p < p₁

theorem ComputationsInterpolatedExponents.exp_lt_iff₁ {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p < p₁ ↔ p₀ < p₁

theorem ComputationsInterpolatedExponents.exp_gt_iff₁ {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) : p₁ < p ↔ p₁ < p₀

Results about the particular choice of exponent

The proof of the real interpolation theorem will estimate
`distribution (trunc f A(t)) t` and `distribution (truncCompl f A(t)) t` for a
function `A`. The function `A` can be given a closed-form expression that works for
_all_ cases in the real interpolation theorem, because of the computation rules available
for elements in `ℝ≥0∞` that avoid the need for a limiting procedure, e.g. `⊤⁻¹ = 0`.

The function `A` will be of the form `A(t) = (t / d) ^ σ` for particular choices of `d` and
`σ`. This section contatins results about the exponents `σ`.

def ComputationsChoiceExponent.ζ (p₀ q₀ p₁ q₁ : ENNReal) (t : ℝ) : ℝ

Equations

• ComputationsChoiceExponent.ζ p₀ q₀ p₁ q₁ t = ((1 - t) * p₀⁻¹.toReal + t * p₁⁻¹.toReal) * (q₁⁻¹.toReal - q₀⁻¹.toReal) / (((1 - t) * q₀⁻¹.toReal + t * q₁⁻¹.toReal) * (p₁⁻¹.toReal - p₀⁻¹.toReal))

theorem ComputationsChoiceExponent.ζ_equality₁ {p₀ q₀ p₁ q₁ t : ENNReal} (ht : t ∈ Set.Ioo 0 1) : ζ p₀ q₀ p₁ q₁ t.toReal = ((1 - t).toReal * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal) * ((1 - t).toReal * q₀⁻¹.toReal + t.toReal * q₁⁻¹.toReal - q₀⁻¹.toReal) / (((1 - t).toReal * q₀⁻¹.toReal + t.toReal * q₁⁻¹.toReal) * ((1 - t).toReal * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal - p₀⁻¹.toReal))

theorem ComputationsChoiceExponent.ζ_equality₂ {p₀ q₀ p₁ q₁ t : ENNReal} (ht : t ∈ Set.Ioo 0 1) : ζ p₀ q₀ p₁ q₁ t.toReal = ((1 - t).toReal * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal) * ((1 - t).toReal * q₀⁻¹.toReal + t.toReal * q₁⁻¹.toReal - q₁⁻¹.toReal) / (((1 - t).toReal * q₀⁻¹.toReal + t.toReal * q₁⁻¹.toReal) * ((1 - t).toReal * p₀⁻¹.toReal + t.toReal * p₁⁻¹.toReal - p₁⁻¹.toReal))

theorem ComputationsChoiceExponent.ζ_symm {p₀ q₀ p₁ q₁ t : ENNReal} (ht : t ∈ Set.Ioo 0 1) : ζ p₀ q₀ p₁ q₁ t.toReal = ζ p₁ q₁ p₀ q₀ (1 - t).toReal

theorem ComputationsChoiceExponent.ζ_equality₃ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) : ζ p₀ q₀ p₁ q₁ t.toReal = p₀.toReal * (q₀.toReal - q.toReal) / (q₀.toReal * (p₀.toReal - p.toReal))

theorem ComputationsChoiceExponent.ζ_equality₄ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ ≠ ⊤) : ζ p₀ q₀ p₁ q₁ t.toReal = p₁.toReal * (q₁.toReal - q.toReal) / (q₁.toReal * (p₁.toReal - p.toReal))

theorem ComputationsChoiceExponent.ζ_equality₅ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) : p₀.toReal + (ζ p₀ q₀ p₁ q₁ t.toReal)⁻¹ * (q.toReal - q₀.toReal) * (p₀.toReal / q₀.toReal) = p.toReal

theorem ComputationsChoiceExponent.ζ_equality₆ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ ≠ ⊤) : p₁.toReal + (ζ p₀ q₀ p₁ q₁ t.toReal)⁻¹ * (q.toReal - q₁.toReal) * (p₁.toReal / q₁.toReal) = p.toReal

theorem ComputationsChoiceExponent.ζ_equality₇ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ = ⊤) : ζ p₀ q₀ p₁ q₁ t.toReal = p₀.toReal / (p₀.toReal - p.toReal)

theorem ComputationsChoiceExponent.ζ_equality₈ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ = ⊤) : ζ p₀ q₀ p₁ q₁ t.toReal = p₁.toReal / (p₁.toReal - p.toReal)

theorem ComputationsChoiceExponent.ζ_eq_top_top {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₁' : p₁ = ⊤) (hq₁' : q₁ = ⊤) : ζ p₀ q₀ p₁ q₁ t.toReal = 1

theorem ComputationsChoiceExponent.ζ_pos_iff_aux {p₀ q₀ p q : ENNReal} (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) : 0 < p₀.toReal * (q₀.toReal - q.toReal) / (q₀.toReal * (p₀.toReal - p.toReal)) ↔ q.toReal < q₀.toReal ∧ p.toReal < p₀.toReal ∨ q₀.toReal < q.toReal ∧ p₀.toReal < p.toReal

theorem ComputationsChoiceExponent.preservation_inequality {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hp₀' : p₀ ≠ ⊤) : p.toReal < p₀.toReal ↔ p < p₀

theorem ComputationsChoiceExponent.preservation_inequality' {p₀ p₁ p t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hp₀' : p₀ ≠ ⊤) : p₀.toReal < p.toReal ↔ p₀ < p

theorem ComputationsChoiceExponent.preservation_inequality_of_lt₀ {q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₀q₁ : q₀ < q₁) : q₀.toReal < q.toReal

theorem ComputationsChoiceExponent.preservation_inequality_of_lt₁ {q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₀q₁ : q₀ < q₁) (hq₁' : q₁ ≠ ⊤) : q.toReal < q₁.toReal

theorem ComputationsChoiceExponent.ζ_pos_toReal_iff₀ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) : 0 < ζ p₀ q₀ p₁ q₁ t.toReal ↔ q.toReal < q₀.toReal ∧ p.toReal < p₀.toReal ∨ q₀.toReal < q.toReal ∧ p₀.toReal < p.toReal

theorem ComputationsChoiceExponent.ζ_pos_toReal_iff₁ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ ≠ ⊤) : 0 < ζ p₀ q₀ p₁ q₁ t.toReal ↔ q.toReal < q₁.toReal ∧ p.toReal < p₁.toReal ∨ q₁.toReal < q.toReal ∧ p₁.toReal < p.toReal

theorem ComputationsChoiceExponent.ζ_pos_iff_aux₀ {p₀ q₀ p₁ q₁ t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) : 0 < ζ p₀ q₀ p₁ q₁ t.toReal ↔ q₀⁻¹.toReal < q₁⁻¹.toReal ∧ p₀⁻¹.toReal < p₁⁻¹.toReal ∨ q₁⁻¹.toReal < q₀⁻¹.toReal ∧ p₁⁻¹.toReal < p₀⁻¹.toReal

theorem ComputationsChoiceExponent.inv_toReal_iff {p₀ p₁ : ENNReal} (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) : p₀⁻¹.toReal < p₁⁻¹.toReal ↔ p₁ < p₀

theorem ComputationsChoiceExponent.ζ_pos_iff {p₀ q₀ p₁ q₁ t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) : 0 < ζ p₀ q₀ p₁ q₁ t.toReal ↔ q₁ < q₀ ∧ p₁ < p₀ ∨ q₀ < q₁ ∧ p₀ < p₁

theorem ComputationsChoiceExponent.ζ_pos_iff' {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) : 0 < ζ p₀ q₀ p₁ q₁ t.toReal ↔ q < q₀ ∧ p < p₀ ∨ q₀ < q ∧ p₀ < p

theorem ComputationsChoiceExponent.ζ_pos_iff_of_lt₀ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) : 0 < ζ p₀ q₀ p₁ q₁ t.toReal ↔ q₀ < q

theorem ComputationsChoiceExponent.ζ_pos_iff_of_lt₁ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) : 0 < ζ p₀ q₀ p₁ q₁ t.toReal ↔ q < q₁

theorem ComputationsChoiceExponent.ζ_neg_iff_aux₀ {p₀ q₀ p₁ q₁ t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) : ζ p₀ q₀ p₁ q₁ t.toReal < 0 ↔ q₀⁻¹.toReal < q₁⁻¹.toReal ∧ p₁⁻¹.toReal < p₀⁻¹.toReal ∨ q₁⁻¹.toReal < q₀⁻¹.toReal ∧ p₀⁻¹.toReal < p₁⁻¹.toReal

theorem ComputationsChoiceExponent.ζ_neg_iff {p₀ q₀ p₁ q₁ t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) : ζ p₀ q₀ p₁ q₁ t.toReal < 0 ↔ q₁ < q₀ ∧ p₀ < p₁ ∨ q₀ < q₁ ∧ p₁ < p₀

theorem ComputationsChoiceExponent.ζ_neg_iff' {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) : ζ p₀ q₀ p₁ q₁ t.toReal < 0 ↔ q < q₀ ∧ p₀ < p ∨ q₀ < q ∧ p < p₀

theorem ComputationsChoiceExponent.ζ_neg_iff_of_lt₀ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) : ζ p₀ q₀ p₁ q₁ t.toReal < 0 ↔ q < q₀

theorem ComputationsChoiceExponent.ζ_neg_iff_of_lt₁ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) : ζ p₀ q₀ p₁ q₁ t.toReal < 0 ↔ q₁ < q

theorem ComputationsChoiceExponent.ζ_neg_iff_aux {p₀ q₀ p q : ENNReal} (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) : p₀.toReal * (q₀.toReal - q.toReal) / (q₀.toReal * (p₀.toReal - p.toReal)) < 0 ↔ q.toReal < q₀.toReal ∧ p₀.toReal < p.toReal ∨ q₀.toReal < q.toReal ∧ p.toReal < p₀.toReal

theorem ComputationsChoiceExponent.ζ_neg_toReal_iff₀ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) : ζ p₀ q₀ p₁ q₁ t.toReal < 0 ↔ q.toReal < q₀.toReal ∧ p₀.toReal < p.toReal ∨ q₀.toReal < q.toReal ∧ p.toReal < p₀.toReal

theorem ComputationsChoiceExponent.ζ_neg_toReal_iff₁ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ ≠ ⊤) : ζ p₀ q₀ p₁ q₁ t.toReal < 0 ↔ q.toReal < q₁.toReal ∧ p₁.toReal < p.toReal ∨ q₁.toReal < q.toReal ∧ p.toReal < p₁.toReal

theorem ComputationsChoiceExponent.ζ_neg_iff₀ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) : ζ p₀ q₀ p₁ q₁ t.toReal < 0 ↔ q < q₀ ∧ p₀ < p ∨ q₀ < q ∧ p < p₀

theorem ComputationsChoiceExponent.ζ_ne_zero {p₀ q₀ p₁ q₁ t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) : ζ p₀ q₀ p₁ q₁ t.toReal ≠ 0

theorem ComputationsChoiceExponent.ζ_le_zero_iff_of_lt₀ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) : ζ p₀ q₀ p₁ q₁ t.toReal ≤ 0 ↔ q < q₀

theorem ComputationsChoiceExponent.ζ_le_zero_iff_of_lt₁ {p₀ q₀ p₁ q₁ p q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) : ζ p₀ q₀ p₁ q₁ t.toReal ≤ 0 ↔ q₁ < q

theorem ComputationsChoiceExponent.eq_exponents₀ {q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) : q₀.toReal + q₁⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₀.toReal) = (1 - t).toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₂ {p₀ q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) : q₀.toReal / p₀.toReal + p₀⁻¹.toReal * q₁⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₀.toReal) = (1 - t).toReal * p₀⁻¹.toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₁ {q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) : q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₀.toReal) = -t.toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₃ {q₀ p₁ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) : p₁⁻¹.toReal * q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₀.toReal) = -t.toReal * p₁⁻¹.toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₄ {q₀ q₁ : ENNReal} : q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) = -(q₀⁻¹.toReal / (q₀⁻¹.toReal - q₁⁻¹.toReal))

theorem ComputationsChoiceExponent.eq_exponents₅ {q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) : q₁.toReal + -(q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₁.toReal)) = t.toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₆ {q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) : q₁⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₁.toReal) = (1 - t).toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₇ {q₀ p₁ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) : q₁.toReal / p₁.toReal + -(p₁⁻¹.toReal * q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₁.toReal)) = t.toReal * p₁⁻¹.toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₈ {p₀ q₀ q₁ q t : ENNReal} (ht : t ∈ Set.Ioo 0 1) (hq₀ : 0 < q₀) (hq₁ : 0 < q₁) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) : p₀⁻¹.toReal * q₁⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₁.toReal) = (1 - t).toReal * p₀⁻¹.toReal * q.toReal