Ordinary height envelope from orders

import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic
import Definitions.Def_D1Bound5_OrdinaryLog10_Definitions

section
namespace D1Bound5


theorem _root_.D1Bound5.ordinary_height_envelope_from_orders
    (B C D Z R h r u : ℝ)
    (hB : 1 ≤ B) (hC : 1 < C) (hD : 0 < D) (hZ : 1 ≤ Z) (hR : 0 < R)
    (hprod : C*D < 2*Z^2)
    (hHlog : ordinaryLog10 (42*B^3*C) < ordinaryLog10 C+h)
    (hRlog : 2*ordinaryLog10 C+r < ordinaryLog10 R)
    (hUlog : ordinaryLog10 (253*B^2) < u)
    (hxt : h-r < ordinaryLog10 C) (hx2 : 0 < 2*ordinaryLog10 C+r)
    (horders : ∀ k : ℕ, 1 ≤ k →
      1 < 3*C*(42*B^3*C)^k/(B*Z)+Z/(2*R^k)) :
    ordinaryLog10 D < 7*ordinaryLog10 C+(4*u+8*h-4*r)+
      (2*u*r+(4*u+8*h-4*r)*(h-r))/(ordinaryLog10 C-(h-r))+(2/5 : ℝ) := by sorry

end D1Bound5
end