MovingLineComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Original-prior comparison for the moving-giant occurrence lines

theorem OAI.Ostmann.moving_line_probability_comparison line 13

Source documentation

No degree or height of an occurrence line is assumed: both are inherited from its actual path of reversals. The same applies to its nonzero row.

theorem moving_line_probability_comparison {A J : Type*} [Fintype A] [Fintype J]
    {n : ℕ} (value : A → ℤ) (hinj : Function.Injective value)
    (steps : J → List (PolynomialReversal (Fin n)))
    (v w : J → MvPolynomial (Fin n) ℤ) (i : J) (external : Bool)
    (k d : ℕ) (hlen : ∀ j, (steps j).length ≤ k)
    (hdegree : ∀ j, (∀ s ∈ steps j,
      s.v.totalDegree ≤ d ∧ s.w.totalDegree ≤ d ∧ s.u.totalDegree ≤ d) ∧
      (v j).totalDegree ≤ d ∧ (w j).totalDegree ≤ d)
    (K : ℝ) (hK : 1 ≤ K)
    (hheight : ∀ (x : Fin n → A) j,
      let φ := MvPolynomial.eval₂Hom (Int.castRingHom ℝ) (fun a => (value (x a) : ℝ))
…

Mentions: OAI.Ostmann.PolynomialReversal