ComputationsInterpolatedExponents.exp_lt_iff

lemma exp_lt_iff (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀p₁ : p₀ ≠ p₁)    (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹) :    p < p₀ ↔ p₁ < p₀ := by  rcases lt_or_gt_of_ne hp₀p₁ with p₀lt_p₁ | p₁lt_p₀  · exact ⟨fun h ↦ (not_le_of_gt h (le_of_lt (interp_exp_between hp₀ hp₁ p₀lt_p₁ ht hp).1)).elim,      fun h ↦ (not_le_of_gt h p₀lt_p₁.le).elim⟩  · exact ⟨fun _ ↦ p₁lt_p₀,      fun _ ↦ (interp_exp_between hp₁ hp₀ p₁lt_p₀ (mem_sub_Ioo one_ne_top ht) (switch_exponents ht hp)).2⟩