Frontier scalar reduction

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

section
namespace D1Bound5








theorem _root_.D1Bound5.frontier_scalar_reduction (A B C T alpha beta K L Q : ℝ)
    (ha : 0 < alpha) (hb : 0 < beta)
    (hA : alpha ≤ A) (hB : beta ≤ B) (hC : beta ≤ C) (hT : 0 ≤ T)
    (hK : 0 ≤ K) (hL : 0 ≤ L) (hQ : 0 ≤ Q)
    (hupper : A*B*C*T ≤
      2*K*(A^2+B^2+C^2+T^2)+L*(A*B+A*C+A*T+B*C+B*T+C*T)+Q) :
    let tau := T/(A*B*C)
    tau ≤ 2*K*tau^2+L*(2/(alpha*beta)+1/beta^2)*tau+
      (2*K*(2/(alpha^2*beta^2)+1/beta^4)+
       L*(1/(alpha^2*beta^2)+2/(alpha*beta^3))+Q/(alpha^2*beta^4)) := by sorry



end D1Bound5
end