Finite Homogeneous Two norm le ratio

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Tactic.Convert
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_FiniteHomogeneousRatio_Definitions
import Definitions.Def_D1Bound5_FiniteHomogeneousTwo_Definitions

section
noncomputable section

namespace D1Bound5






theorem _root_.D1Bound5.finiteHomogeneousTwo_norm_le_ratio (n : ℕ) (v : Fin (n+1) → ℤ)
    (x y : ℂ) (r : ℝ) (hr : 0 ≤ r) (hxy : ‖x‖ ≤ r*‖y‖) :
    ‖finiteHomogeneousTwo n v x y‖ ≤ finiteHomogeneousRatioWeight n v r*‖y‖^n := by sorry







end D1Bound5
end