Frontier Table Row — parameters

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
import Definitions.Def_D1Bound5_FrontierScalarReduction_Definitions
import Definitions.Def_D1Bound5_FrontierTableNumeric_Definitions

section
namespace D1Bound5




theorem _root_.D1Bound5.FrontierTableRow.parameters {alpha beta target : ℝ}
    (h : FrontierTableRow alpha beta target) :
    0 < alpha ∧ 3 ≤ beta ∧ alpha ≤ beta ∧ 5 < alpha*beta ∧
      0 ≤ frontierK alpha beta ∧ 0 ≤ frontierL alpha beta ∧
      0 ≤ frontierQ alpha beta := by sorry



end D1Bound5
end