One Small Cutoff Row — overlaps at real

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Int.Interval
import Mathlib.Data.Int.Sqrt
import Mathlib.Data.List.Range
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_OneSmallCutoffArithmetic_Definitions_001
import Definitions.Def_D1Bound5_OneSmallRows_Definitions

section
namespace D1Bound5


theorem _root_.D1Bound5.OneSmallCutoffRow.overlaps_at_real (r : OneSmallCutoffRow)
    (hv : r.Valid) (x : ℝ) (hx : (r.triple.cutoff : ℝ) ≤ x)
    (e : ℚ × ℕ) (he : e ∈ r.overlaps) :
    1 < (e.1 : ℝ)*x^e.2 := by sorry





end D1Bound5
end