sgl_poly_bounds

import Definitions.Def_sipser_gacs_lautemann
import Mathlib.Tactic.Ring

/-!
# Closure of polynomial boundedness

The machine's running time is a sum of products of the input's length, the
leaf count, the ruler's width, and constants.  Rather than exhibit one
coefficient and degree for the total, this module closes
`PolynomiallyBounded` under the operations the total is built from.
-/

namespace SipserGacsLautemann

theorem polynomiallyBounded_of_le {f g : Nat → Nat}
    (h : ∀ n, f n ≤ g n) (hg : PolynomiallyBounded g) :
    PolynomiallyBounded f := by
  obtain ⟨cg, dg, hbound⟩ := hg
  exact ⟨cg, dg, fun n => le_trans (h n) (hbound n)⟩

theorem polynomiallyBounded_const (c : Nat) :
    PolynomiallyBounded (fun _ => c) :=
  ⟨c, 0, fun n => by simp⟩

theorem polynomiallyBounded_id : PolynomiallyBounded (fun n => n) :=
  ⟨1, 1, fun n => by simp⟩

/-- A fixed power, with a fixed coefficient. -/
theorem polynomiallyBounded_pow (c k : Nat) :
    PolynomiallyBounded (fun n => c * (n + 1) ^ k) :=
  ⟨c, k, fun _ => le_refl _⟩

theorem polynomiallyBounded_add {f g : Nat → Nat}
    (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) :
    PolynomiallyBounded (fun n => f n + g n) := by
  obtain ⟨cf, df, hfb⟩ := hf
  obtain ⟨cg, dg, hgb⟩ := hg
  refine ⟨cf + cg, max df dg, fun n => ?_⟩
  show f n + g n ≤ (cf + cg) * (n + 1) ^ (max df dg)
  have h1 : cf * (n + 1) ^ df ≤ cf * (n + 1) ^ (max df dg) :=
    Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by omega) (le_max_left _ _))
  have h2 : cg * (n + 1) ^ dg ≤ cg * (n + 1) ^ (max df dg) :=
    Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by omega) (le_max_right _ _))
  have h3 : (cf + cg) * (n + 1) ^ (max df dg) =
      cf * (n + 1) ^ (max df dg) + cg * (n + 1) ^ (max df dg) := by ring
  have hf' := hfb n
  have hg' := hgb n
  omega

theorem polynomiallyBounded_mul {f g : Nat → Nat}
    (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) :
    PolynomiallyBounded (fun n => f n * g n) := by
  obtain ⟨cf, df, hfb⟩ := hf
  obtain ⟨cg, dg, hgb⟩ := hg
  refine ⟨cf * cg, df + dg, fun n => ?_⟩
  show f n * g n ≤ cf * cg * (n + 1) ^ (df + dg)
  calc f n * g n ≤ (cf * (n + 1) ^ df) * (cg * (n + 1) ^ dg) :=
        Nat.mul_le_mul (hfb n) (hgb n)
    _ = cf * cg * (n + 1) ^ (df + dg) := by rw [pow_add]; ring

theorem polynomiallyBounded_mul_const {f : Nat → Nat} (c : Nat)
    (hf : PolynomiallyBounded f) :
    PolynomiallyBounded (fun n => c * f n) :=
  polynomiallyBounded_mul (polynomiallyBounded_const c) hf

theorem polynomiallyBounded_add_const {f : Nat → Nat} (c : Nat)
    (hf : PolynomiallyBounded f) :
    PolynomiallyBounded (fun n => f n + c) :=
  polynomiallyBounded_add hf (polynomiallyBounded_const c)

/-- A polynomial of a polynomially bounded argument, at fixed degree. -/
theorem polynomiallyBounded_comp_pow {f : Nat → Nat} (c k : Nat)
    (hf : PolynomiallyBounded f) :
    PolynomiallyBounded (fun n => c * (f n + 1) ^ k) := by
  induction k with
  | zero =>
      refine polynomiallyBounded_of_le (g := fun _ => c) (fun n => ?_)
        (polynomiallyBounded_const c)
      rw [pow_zero, Nat.mul_one]
  | succ k ih =>
      refine polynomiallyBounded_of_le
        (g := fun n => (c * (f n + 1) ^ k) * (f n + 1)) (fun n => ?_)
        (polynomiallyBounded_mul ih
          (polynomiallyBounded_add hf (polynomiallyBounded_const 1)))
      show c * (f n + 1) ^ (k + 1) ≤ c * (f n + 1) ^ k * (f n + 1)
      rw [pow_succ]
      exact le_of_eq (by ring)

end SipserGacsLautemann