ComputationsInterpolatedExponents.preservation_positivity_inv_toReal

lemma preservation_positivity_inv_toReal (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁)    (hp₀p₁ : p₀ ≠ p₁) :    0 < (1 - t.toReal) * (p₀⁻¹).toReal + t.toReal * (p₁⁻¹).toReal := by  -- TODO: do we need aux' ever? if so, extract as general lemma!  -- have aux' : 0 < (1 - t).toReal :=  --   toReal_pos (tsub_pos_iff_lt.mpr ht.2).ne' (sub_ne_top top_ne_one.symm)  have aux : 0 < 1 - t.toReal := by simpa using (toReal_mem_Ioo ht).2  rcases (eq_or_ne p₀ ⊤) with p₀eq_top | p₀ne_top  · rw [p₀eq_top]    simp only [inv_top, toReal_zero, mul_zero, zero_add]    apply mul_pos (toReal_mem_Ioo ht).1    rw [toReal_inv]    refine inv_pos_of_pos (exp_toReal_pos hp₁ ?_)    rw [p₀eq_top] at hp₀p₁    exact hp₀p₁.symm  · exact add_pos_of_pos_of_nonneg      (mul_pos aux <| toReal_inv _ ▸ inv_pos_of_pos (exp_toReal_pos hp₀ p₀ne_top))      (mul_nonneg (toReal_mem_Ioo ht).1.le toReal_nonneg)