ErrorPowers.lean

theorem henselFactorization_exists_factor_of_coeff_mem_span_singleton
    {R : Type*} [CommRing R] {a : R} {P : R[X]}
    (hP : ∀ i : ℕ, P.coeff i ∈ Ideal.span ({a} : Set R)) :
    ∃ Q : R[X], P = Polynomial.C a * Q

theorem henselFactorization_coeff_mem_span_singleton_pow_of_factor
    {R : Type*} [CommRing R] {π : R} {n : ℕ} {P Q : R[X]}
    (hfactor : P = Polynomial.C (π ^ n) * Q) :
    ∀ i : ℕ, P.coeff i ∈ Ideal.span ({π ^ n} : Set R)

theorem henselFactorization_coeff_mem_span_pow_of_factor
    {R : Type*} [CommRing R] {π : R} {n : ℕ} {P Q : R[X]}
    (hfactor : P = Polynomial.C (π ^ n) * Q) :
    ∀ i : ℕ, P.coeff i ∈ Ideal.span ({π} : Set R) ^ n

theorem henselFactorization_span_singleton_le_ideal_of_mem
    {R : Type*} [CommRing R] (I : Ideal R) {π : R} (hπ : π ∈ I) :
    Ideal.span ({π} : Set R) ≤ I

theorem henselFactorization_coeff_mem_maximalIdeal_pow_of_factor_of_mem
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R} {n : ℕ} {P Q : R[X]}
    (hπ : π ∈ IsLocalRing.maximalIdeal R)
    (hfactor : P = Polynomial.C (π ^ n) * Q) :
    ∀ i : ℕ, P.coeff i ∈ IsLocalRing.maximalIdeal R ^ n

theorem henselFactorization_span_singleton_pow_mul_mem_succ
    {R : Type*} [CommRing R] {π x : R} (n : ℕ)
    (hx : x ∈ Ideal.span ({π} : Set R)) :
    π ^ n * x ∈ Ideal.span ({π ^ (n + 1)} : Set R)

theorem henselFactorization_pow_mul_mem_span_singleton_of_pos
    {R : Type*} [CommRing R] {π x : R} {n : ℕ} (hn : 1 ≤ n) :
    π ^ n * x ∈ Ideal.span ({π} : Set R)

theorem henselFactorization_span_singleton_pow_mul_pow_mem_succ_of_pos
    {R : Type*} [CommRing R] {π x : R} {n : ℕ} (hn : 1 ≤ n) :
    π ^ n * (π ^ n * x) ∈ Ideal.span ({π ^ (n + 1)} : Set R)

theorem henselFactorization_correction_congruence_symm_span_singleton
    {R : Type*} [CommRing R] {π : R} {A B : R[X]}
    (hcong : ∀ i : ℕ, (A - B).coeff i ∈ Ideal.span ({π} : Set R)) :
    ∀ i : ℕ, (B - A).coeff i ∈ Ideal.span ({π} : Set R)

theorem henselFactorization_power_update_error_coeff_mem_span_singleton
    {R : Type*} [CommRing R] {π : R} {n : ℕ} (hn : 1 ≤ n)
    {f g h fn p q : R[X]}
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hcorr :
      ∀ i : ℕ, (g * q + h * p - fn).coeff i ∈
        Ideal.span ({π} : Set R)) :
    ∀ i : ℕ,
      (f - (g + Polynomial.C (π ^ n) * p) *
          (h + Polynomial.C (π ^ n) * q)).coeff i ∈
        Ideal.span ({π ^ (n + 1)} : Set R)

theorem henselFactorization_power_update_error_factor_exists
    {R : Type*} [CommRing R] {π : R} {n : ℕ} (hn : 1 ≤ n)
    {f g h fn p q : R[X]}
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hcorr :
      ∀ i : ℕ, (g * q + h * p - fn).coeff i ∈
        Ideal.span ({π} : Set R)) :
    ∃ fnNext : R[X],
      f - (g + Polynomial.C (π ^ n) * p) *
          (h + Polynomial.C (π ^ n) * q) =
        Polynomial.C (π ^ (n + 1)) * fnNext

theorem henselFactorization_correction_congruence_span_singleton_of_maximalIdeal_le
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R} {A B : R[X]}
    (hπ : IsLocalRing.maximalIdeal R ≤ Ideal.span ({π} : Set R))
    (hcong : ∀ i : ℕ, (A - B).coeff i ∈ IsLocalRing.maximalIdeal R) :
    ∀ i : ℕ, (A - B).coeff i ∈ Ideal.span ({π} : Set R)

theorem henselFactorization_power_update_error_factor_exists_of_maximalIdeal_correction_le
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R} {n : ℕ} (hn : 1 ≤ n)
    (hπ : IsLocalRing.maximalIdeal R ≤ Ideal.span ({π} : Set R))
    {f g h fn p q : R[X]}
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hcorr :
      ∀ i : ℕ, (g * q + h * p - fn).coeff i ∈
        IsLocalRing.maximalIdeal R) :
    ∃ fnNext : R[X],
      f - (g + Polynomial.C (π ^ n) * p) *
          (h + Polynomial.C (π ^ n) * q) =
        Polynomial.C (π ^ (n + 1)) * fnNext