Finite Q pair height

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Analysis.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_FiniteQMatrix_Definitions

section
namespace D1Bound5


theorem _root_.D1Bound5.finiteQ_pair_height
    (u v c : ℂ) (T C : ℝ) (hT : 0 ≤ T) (hC : 0 ≤ C)
    (hu : ‖u‖ ≤ T) (hv : ‖v‖ ≤ T) (hc : ‖c‖ ≤ C) (hTC : 1 ≤ T*C) :
    ‖finiteQLeft u v c‖ + ‖finiteQRight u v c‖ ≤ 36*T^3*C := by sorry



end D1Bound5
end