One Small Cutoff Row — start overlap 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.start_overlap_real (r : OneSmallCutoffRow)
    (hv : r.Valid) (S T : ℝ) (hS : 0 < S)
    (hSsq : S^2 = (r.s0 : ℝ))
    (hlarge : (r.triple.cutoff : ℝ) ≤ T^2) :
    1 < (1-1/4000 : ℝ)*(r.retainedCoefficient : ℝ)^4*T^10/(12100*S^10) := by sorry



end D1Bound5
end