FormalProduct.lean

theorem formalLogOnePlusProductArgument_choiceCounts_q_range
    {q : ℕ} {e : Fin 2 →₀ ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hl : l ∈ Finset.finsuppAntidiag (Finset.range q) e)
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    e (0 : Fin 2) ≤ q ∧ e (1 : Fin 2) ≤ q ∧
      q ≤ e (0 : Fin 2) + e (1 : Fin 2)

theorem formalLogOnePlusProductArgumentBasicFactorChoices_nonempty_q_range
    {q : ℕ} {e : Fin 2 →₀ ℕ}
    (h :
      (formalLogOnePlusProductArgumentBasicFactorChoices q e).Nonempty) :
    e (0 : Fin 2) ≤ q ∧ e (1 : Fin 2) ≤ q ∧
      q ≤ e (0 : Fin 2) + e (1 : Fin 2)

theorem formalLogOnePlusProductArgumentBasicFactorChoices_eq_empty_of_q_lt_left_coord
    {q : ℕ} {e : Fin 2 →₀ ℕ}
    (hleft : q < e (0 : Fin 2)) :
    formalLogOnePlusProductArgumentBasicFactorChoices q e = ∅

theorem formalLogOnePlusProductArgumentBasicFactorChoices_eq_empty_of_q_lt_right_coord
    {q : ℕ} {e : Fin 2 →₀ ℕ}
    (hright : q < e (1 : Fin 2)) :
    formalLogOnePlusProductArgumentBasicFactorChoices q e = ∅

theorem formalLogOnePlusProductArgumentBasicFactorChoices_eq_empty_of_coord_sum_lt_q
    {q : ℕ} {e : Fin 2 →₀ ℕ}
    (hsum : e (0 : Fin 2) + e (1 : Fin 2) < q) :
    formalLogOnePlusProductArgumentBasicFactorChoices q e = ∅

theorem formalLogOnePlusProductArgument_pow_term_prod_eq_one_of_factors_basic
    (A : Type*) [CommRing A] {q : ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hbasic : ∀ i ∈ Finset.range q,
      l i = Finsupp.single (0 : Fin 2) 1 ∨
        l i = Finsupp.single (1 : Fin 2) 1 ∨
          l i =
            Finsupp.single (0 : Fin 2) 1 +
              Finsupp.single (1 : Fin 2) 1) :
    (∏ i ∈ Finset.range q,
      MvPowerSeries.coeff (l i) (formalLogOnePlusProductArgument A)) = 1

theorem formalLogOnePlusProductArgument_pow_term_prod_eq_one_of_basicFactor
    (A : Type*) [CommRing A] {q : ℕ} {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hbasic : ∀ i ∈ Finset.range q,
      formalLogOnePlusProductArgumentBasicFactor (l i)) :
    (∏ i ∈ Finset.range q,
      MvPowerSeries.coeff (l i) (formalLogOnePlusProductArgument A)) = 1

theorem formalLogOnePlusProductArgument_pow_term_prod_eq_one_of_ne_zero
    (A : Type*) [CommRing A] {q : ℕ}
    {l : ℕ →₀ (Fin 2 →₀ ℕ)}
    (hprod :
      (∏ i ∈ Finset.range q,
        MvPowerSeries.coeff (l i) (formalLogOnePlusProductArgument A)) ≠ 0) :
    (∏ i ∈ Finset.range q,
      MvPowerSeries.coeff (l i) (formalLogOnePlusProductArgument A)) = 1

theorem formalLogOnePlusProductArgument_pow_coeff_eq_sum_basicFactor
    (A : Type*) [CommRing A] (q : ℕ) (e : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff e ((formalLogOnePlusProductArgument A) ^ q) =
      ∑ l ∈ Finset.finsuppAntidiag (Finset.range q) e,
        if ∀ i ∈ Finset.range q,
            formalLogOnePlusProductArgumentBasicFactor (l i)
        then (1 : A) else 0 := by
  classical
  rw [MvPowerSeries.coeff_pow]
  apply Finset.sum_congr rfl
  intro l hl
  by_cases hbasic :
      ∀ i ∈ Finset.range q,
        formalLogOnePlusProductArgumentBasicFactor (l i)
  · rw [formalLogOnePlusProductArgument_pow_term_prod_eq_one_of_basicFactor
      A hbasic]
    rw [ite_eq_left hbasic]
  · have hprodZero :
        (∏ i ∈ Finset.range q,
          MvPowerSeries.coeff (l i) (formalLogOnePlusProductArgument A)) = 0 := by
      by_contra hprodNe
      apply hbasic
      intro i hi
      exact
        formalLogOnePlusProductArgument_coeff_ne_zero_eq_basic A (l i) (by
          intro hzero
          exact hprodNe (Finset.prod_eq_zero hi hzero))
    rw [hprodZero]
    rw [ite_eq_right hbasic]

theorem formalLogOnePlusProductArgument_basicFactor_sum_eq_card_choices
    (A : Type*) [CommRing A] (q : ℕ) (e : Fin 2 →₀ ℕ) :
    (∑ l ∈ Finset.finsuppAntidiag (Finset.range q) e,
      if ∀ i ∈ Finset.range q,
          formalLogOnePlusProductArgumentBasicFactor (l i)
      then (1 : A) else 0) =
      ((formalLogOnePlusProductArgumentBasicFactorChoices q e).card : A) := by
  classical
  simp [formalLogOnePlusProductArgumentBasicFactorChoices]

theorem formalLogOnePlusProductArgument_pow_coeff_eq_card_choices
    (A : Type*) [CommRing A] (q : ℕ) (e : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff e ((formalLogOnePlusProductArgument A) ^ q) =
      ((formalLogOnePlusProductArgumentBasicFactorChoices q e).card : A)

theorem formalLogOnePlusProductArgument_pow_coeff_eq_zero_of_coord_sum_lt
    (A : Type*) [CommRing A] (q : ℕ) (e : Fin 2 →₀ ℕ)
    (hsum : e (0 : Fin 2) + e (1 : Fin 2) < q) :
    MvPowerSeries.coeff e ((formalLogOnePlusProductArgument A) ^ q) = 0

theorem formalLogOnePlusProductArgument_pow_coeff_eq_zero_of_left_coord_lt
    (A : Type*) [CommRing A] (q : ℕ) (e : Fin 2 →₀ ℕ)
    (hleft : q < e (0 : Fin 2)) :
    MvPowerSeries.coeff e ((formalLogOnePlusProductArgument A) ^ q) = 0

theorem formalLogOnePlusProductArgument_pow_coeff_eq_zero_of_right_coord_lt
    (A : Type*) [CommRing A] (q : ℕ) (e : Fin 2 →₀ ℕ)
    (hright : q < e (1 : Fin 2)) :
    MvPowerSeries.coeff e ((formalLogOnePlusProductArgument A) ^ q) = 0

theorem formalLogOnePlusProductArgument_pow_coeff_eq_zero_of_degree_lt
    (A : Type*) [CommRing A] (q : ℕ) (e : Fin 2 →₀ ℕ)
    (hdegree : Finsupp.degree e < q) :
    MvPowerSeries.coeff e ((formalLogOnePlusProductArgument A) ^ q) = 0

theorem formalLogOnePlusProductArgument_logSubst_coeff_term_eq_zero_of_degree_lt
    (A : Type*) [CommRing A] [Algebra ℚ A] (q : ℕ) (e : Fin 2 →₀ ℕ)
    (hdegree : Finsupp.degree e < q) :
    PowerSeries.coeff q (PowerSeries.log A) •
        MvPowerSeries.coeff e ((formalLogOnePlusProductArgument A) ^ q) =
      0

theorem formalLogOnePlusProductArgument_logSubst_coeff_term_eq_zero_of_left_coord_lt
    (A : Type*) [CommRing A] [Algebra ℚ A] (q : ℕ) (e : Fin 2 →₀ ℕ)
    (hleft : q < e (0 : Fin 2)) :
    PowerSeries.coeff q (PowerSeries.log A) •
        MvPowerSeries.coeff e ((formalLogOnePlusProductArgument A) ^ q) =
      0

theorem formalLogOnePlusProductArgument_logSubst_coeff_term_eq_zero_of_right_coord_lt
    (A : Type*) [CommRing A] [Algebra ℚ A] (q : ℕ) (e : Fin 2 →₀ ℕ)
    (hright : q < e (1 : Fin 2)) :
    PowerSeries.coeff q (PowerSeries.log A) •
        MvPowerSeries.coeff e ((formalLogOnePlusProductArgument A) ^ q) =
      0

theorem formalLogOnePlusProductArgument_logSubst_coeff_eq_sum_range_degree_succ
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff e
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) =
      ∑ q ∈ Finset.range (Finsupp.degree e + 1),
        PowerSeries.coeff q (PowerSeries.log A) •
          MvPowerSeries.coeff e
            ((formalLogOnePlusProductArgument A) ^ q)

theorem formalLogOnePlusProductArgument_logSubst_coeff_eq_sum_range_degree_succ_filter_coord_le
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff e
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) =
      ∑ q ∈
        (Finset.range (Finsupp.degree e + 1)).filter
          (fun q : ℕ => e (0 : Fin 2) ≤ q ∧ e (1 : Fin 2) ≤ q),
        PowerSeries.coeff q (PowerSeries.log A) •
          MvPowerSeries.coeff e
            ((formalLogOnePlusProductArgument A) ^ q) := by
  rw [formalLogOnePlusProductArgument_logSubst_coeff_eq_sum_range_degree_succ]
  exact
    (Finset.sum_subset (Finset.filter_subset _ _) (fun q hq hnot => by
      by_cases hleft : e (0 : Fin 2) ≤ q
      · by_cases hright : e (1 : Fin 2) ≤ q
        · exfalso
          exact hnot (by simpa [hleft, hright] using hq)
        · exact
            formalLogOnePlusProductArgument_logSubst_coeff_term_eq_zero_of_right_coord_lt
              A q e (Nat.lt_of_not_ge hright)
      · exact
          formalLogOnePlusProductArgument_logSubst_coeff_term_eq_zero_of_left_coord_lt
            A q e (Nat.lt_of_not_ge hleft))).symm

theorem formalLogOnePlusProductArgument_sub_leftVariable_dvd_rightVariable
    (A : Type*) [CommRing A] :
    (MvPowerSeries.X (1 : Fin 2) : MvPowerSeries (Fin 2) A) ∣
      formalLogOnePlusProductArgument A -
        MvPowerSeries.X (0 : Fin 2)

theorem formalLogOnePlusProductArgument_sub_rightVariable_dvd_leftVariable
    (A : Type*) [CommRing A] :
    (MvPowerSeries.X (0 : Fin 2) : MvPowerSeries (Fin 2) A) ∣
      formalLogOnePlusProductArgument A -
        MvPowerSeries.X (1 : Fin 2)

theorem formalLogOnePlusProductArgument_pow_sub_leftVariable_pow_dvd_rightVariable
    (A : Type*) [CommRing A] (d : ℕ) :
    (MvPowerSeries.X (1 : Fin 2) : MvPowerSeries (Fin 2) A) ∣
      (formalLogOnePlusProductArgument A) ^ d -
        (MvPowerSeries.X (0 : Fin 2) : MvPowerSeries (Fin 2) A) ^ d

theorem formalLogOnePlusProductArgument_pow_sub_rightVariable_pow_dvd_leftVariable
    (A : Type*) [CommRing A] (d : ℕ) :
    (MvPowerSeries.X (0 : Fin 2) : MvPowerSeries (Fin 2) A) ∣
      (formalLogOnePlusProductArgument A) ^ d -
        (MvPowerSeries.X (1 : Fin 2) : MvPowerSeries (Fin 2) A) ^ d

theorem formalLogOnePlusProductArgument_pow_coeff_single_left
    (A : Type*) [CommRing A] (d n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) n)
        ((formalLogOnePlusProductArgument A) ^ d) =
      MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) n)
        ((MvPowerSeries.X (0 : Fin 2) : MvPowerSeries (Fin 2) A) ^ d)

theorem formalLogOnePlusProductArgument_pow_coeff_single_right
    (A : Type*) [CommRing A] (d n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (1 : Fin 2) n)
        ((formalLogOnePlusProductArgument A) ^ d) =
      MvPowerSeries.coeff (Finsupp.single (1 : Fin 2) n)
        ((MvPowerSeries.X (1 : Fin 2) : MvPowerSeries (Fin 2) A) ^ d)

theorem formalLogOnePlusLeftVariable_pow_coeff
    (A : Type*) [CommRing A] (e : Fin 2 →₀ ℕ) (d : ℕ) :
    MvPowerSeries.coeff e
        ((MvPowerSeries.X (0 : Fin 2) : MvPowerSeries (Fin 2) A) ^ d) =
      if e = Finsupp.single (0 : Fin 2) d then 1 else 0 := by
  simpa using
    MvPowerSeries.coeff_X_pow (R := A) e (0 : Fin 2) d

theorem formalLogOnePlusRightVariable_pow_coeff
    (A : Type*) [CommRing A] (e : Fin 2 →₀ ℕ) (d : ℕ) :
    MvPowerSeries.coeff e
        ((MvPowerSeries.X (1 : Fin 2) : MvPowerSeries (Fin 2) A) ^ d) =
      if e = Finsupp.single (1 : Fin 2) d then 1 else 0 := by
  simpa using
    MvPowerSeries.coeff_X_pow (R := A) e (1 : Fin 2) d

theorem formalLogOnePlusProductArgument_logSubst_coeff_single_left
    (A : Type*) [CommRing A] [Algebra ℚ A] (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) n)
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) =
      PowerSeries.coeff n (PowerSeries.log A)

theorem formalLogOnePlusProductArgument_logSubst_coeff_single_right
    (A : Type*) [CommRing A] [Algebra ℚ A] (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (1 : Fin 2) n)
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) =
      PowerSeries.coeff n (PowerSeries.log A)

def formalLogOnePlusLeftVariableLogSubst
    (A : Type*) [CommRing A] [Algebra ℚ A] : MvPowerSeries (Fin 2) A

def formalLogOnePlusRightVariableLogSubst
    (A : Type*) [CommRing A] [Algebra ℚ A] : MvPowerSeries (Fin 2) A

def formalLogOnePlusProductRightSide
    (A : Type*) [CommRing A] [Algebra ℚ A] : MvPowerSeries (Fin 2) A

theorem formalLogOnePlusLeftVariableLogSubst_coeff_single
    (A : Type*) [CommRing A] [Algebra ℚ A] (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) n)
        (formalLogOnePlusLeftVariableLogSubst A) =
      PowerSeries.coeff n (PowerSeries.log A)

theorem formalLogOnePlusRightVariableLogSubst_coeff_single
    (A : Type*) [CommRing A] [Algebra ℚ A] (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (1 : Fin 2) n)
        (formalLogOnePlusRightVariableLogSubst A) =
      PowerSeries.coeff n (PowerSeries.log A)

theorem formalLogOnePlusLeftVariableLogSubst_coeff_of_ne_axis
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (he : ∀ d : ℕ, e ≠ Finsupp.single (0 : Fin 2) d) :
    MvPowerSeries.coeff e (formalLogOnePlusLeftVariableLogSubst A) = 0

theorem formalLogOnePlusRightVariableLogSubst_coeff_of_ne_axis
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (he : ∀ d : ℕ, e ≠ Finsupp.single (1 : Fin 2) d) :
    MvPowerSeries.coeff e (formalLogOnePlusRightVariableLogSubst A) = 0

theorem formalLogOnePlusProductRightSide_coeff
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff e (formalLogOnePlusProductRightSide A) =
      MvPowerSeries.coeff e (formalLogOnePlusLeftVariableLogSubst A) +
        MvPowerSeries.coeff e (formalLogOnePlusRightVariableLogSubst A)

theorem formalLogOnePlusProductArgument_logSubst_constantCoeff
    (A : Type*) [CommRing A] [Algebra ℚ A] :
    MvPowerSeries.constantCoeff
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) = 0

theorem formalLogOnePlusProductRightSide_coeff_single_left
    (A : Type*) [CommRing A] [Algebra ℚ A] (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) n)
        (formalLogOnePlusProductRightSide A) =
      PowerSeries.coeff n (PowerSeries.log A)

theorem formalLogOnePlusProductRightSide_coeff_single_right
    (A : Type*) [CommRing A] [Algebra ℚ A] (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (1 : Fin 2) n)
        (formalLogOnePlusProductRightSide A) =
      PowerSeries.coeff n (PowerSeries.log A)

theorem formalLogOnePlusProductRightSide_coeff_of_ne_axes
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (heLeft : ∀ d : ℕ, e ≠ Finsupp.single (0 : Fin 2) d)
    (heRight : ∀ d : ℕ, e ≠ Finsupp.single (1 : Fin 2) d) :
    MvPowerSeries.coeff e (formalLogOnePlusProductRightSide A) = 0

theorem formalLogOnePlusProductFormula_coeff_single_left
    (A : Type*) [CommRing A] [Algebra ℚ A] (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) n)
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) =
      MvPowerSeries.coeff (Finsupp.single (0 : Fin 2) n)
        (formalLogOnePlusProductRightSide A)

theorem formalLogOnePlusProductFormula_coeff_single_right
    (A : Type*) [CommRing A] [Algebra ℚ A] (n : ℕ) :
    MvPowerSeries.coeff (Finsupp.single (1 : Fin 2) n)
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) =
      MvPowerSeries.coeff (Finsupp.single (1 : Fin 2) n)
        (formalLogOnePlusProductRightSide A)

theorem finsupp_fin_two_eq_single_left_of_right_eq_zero
    (e : Fin 2 →₀ ℕ) (he : e (1 : Fin 2) = 0) :
    e = Finsupp.single (0 : Fin 2) (e (0 : Fin 2))

theorem finsupp_fin_two_eq_single_right_of_left_eq_zero
    (e : Fin 2 →₀ ℕ) (he : e (0 : Fin 2) = 0) :
    e = Finsupp.single (1 : Fin 2) (e (1 : Fin 2))

theorem finsupp_fin_two_left_pos_of_not_right_axis
    (e : Fin 2 →₀ ℕ)
    (he : ∀ d : ℕ, e ≠ Finsupp.single (1 : Fin 2) d) :
    0 < e (0 : Fin 2)

theorem finsupp_fin_two_right_pos_of_not_left_axis
    (e : Fin 2 →₀ ℕ)
    (he : ∀ d : ℕ, e ≠ Finsupp.single (0 : Fin 2) d) :
    0 < e (1 : Fin 2)

theorem finsupp_fin_two_degree_eq (e : Fin 2 →₀ ℕ) :
    Finsupp.degree e = e (0 : Fin 2) + e (1 : Fin 2)

theorem finsupp_fin_two_ne_single_left_of_right_pos
    (e : Fin 2 →₀ ℕ) (hpos : 0 < e (1 : Fin 2)) (d : ℕ) :
    e ≠ Finsupp.single (0 : Fin 2) d

theorem finsupp_fin_two_ne_single_right_of_left_pos
    (e : Fin 2 →₀ ℕ) (hpos : 0 < e (0 : Fin 2)) (d : ℕ) :
    e ≠ Finsupp.single (1 : Fin 2) d

theorem formalLogOnePlusProductRightSide_coeff_of_pos_coords
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (hleft : 0 < e (0 : Fin 2)) (hright : 0 < e (1 : Fin 2)) :
    MvPowerSeries.coeff e (formalLogOnePlusProductRightSide A) = 0

theorem formalLogOnePlusProductFormula_coeff_of_right_coord_zero
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (he : e (1 : Fin 2) = 0) :
    MvPowerSeries.coeff e
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) =
      MvPowerSeries.coeff e (formalLogOnePlusProductRightSide A)

theorem formalLogOnePlusProductFormula_coeff_of_left_coord_zero
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (he : e (0 : Fin 2) = 0) :
    MvPowerSeries.coeff e
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) =
      MvPowerSeries.coeff e (formalLogOnePlusProductRightSide A)

def formalLogOnePlusProductFormulaDefect
    (A : Type*) [CommRing A] [Algebra ℚ A] : MvPowerSeries (Fin 2) A

theorem formalLogOnePlusProductFormulaDefect_coeff_of_right_coord_zero
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (he : e (1 : Fin 2) = 0) :
    MvPowerSeries.coeff e
        (formalLogOnePlusProductFormulaDefect A) = 0

theorem formalLogOnePlusProductFormulaDefect_coeff_of_left_coord_zero
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (he : e (0 : Fin 2) = 0) :
    MvPowerSeries.coeff e
        (formalLogOnePlusProductFormulaDefect A) = 0

theorem
  formalLogOnePlusProductFormulaDefect_coeff_of_pos_coords_eq_sum_range_degree_succ_filter_coord_le
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (hleft : 0 < e (0 : Fin 2)) (hright : 0 < e (1 : Fin 2)) :
    MvPowerSeries.coeff e
        (formalLogOnePlusProductFormulaDefect A) =
      ∑ q ∈
        (Finset.range (Finsupp.degree e + 1)).filter
          (fun q : ℕ => e (0 : Fin 2) ≤ q ∧ e (1 : Fin 2) ≤ q),
        PowerSeries.coeff q (PowerSeries.log A) •
          MvPowerSeries.coeff e
            ((formalLogOnePlusProductArgument A) ^ q) := by
  simp [formalLogOnePlusProductFormulaDefect,
    formalLogOnePlusProductRightSide_coeff_of_pos_coords A e hleft hright,
    formalLogOnePlusProductArgument_logSubst_coeff_eq_sum_range_degree_succ_filter_coord_le]

theorem formalProductDefect_coeff_pos_eq_filtered_sum
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (hleft : 0 < e (0 : Fin 2)) (hright : 0 < e (1 : Fin 2)) :
    MvPowerSeries.coeff e
        (formalLogOnePlusProductFormulaDefect A) =
      ∑ q ∈
        (Finset.range (e (0 : Fin 2) + e (1 : Fin 2) + 1)).filter
          (fun q : ℕ => e (0 : Fin 2) ≤ q ∧ e (1 : Fin 2) ≤ q),
        PowerSeries.coeff q (PowerSeries.log A) •
          MvPowerSeries.coeff e
            ((formalLogOnePlusProductArgument A) ^ q) := by
  rw [
  formalLogOnePlusProductFormulaDefect_coeff_of_pos_coords_eq_sum_range_degree_succ_filter_coord_le
    A e hleft hright]
  rw [finsupp_fin_two_degree_eq]

theorem formalLogOnePlusProductFormulaDefect_coeff_of_pos_coords_eq_sum_basicFactor
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (hleft : 0 < e (0 : Fin 2)) (hright : 0 < e (1 : Fin 2)) :
    MvPowerSeries.coeff e
        (formalLogOnePlusProductFormulaDefect A) =
      ∑ q ∈
        (Finset.range (e (0 : Fin 2) + e (1 : Fin 2) + 1)).filter
          (fun q : ℕ => e (0 : Fin 2) ≤ q ∧ e (1 : Fin 2) ≤ q),
        PowerSeries.coeff q (PowerSeries.log A) •
          (∑ l ∈ Finset.finsuppAntidiag (Finset.range q) e,
            if ∀ i ∈ Finset.range q,
                formalLogOnePlusProductArgumentBasicFactor (l i)
            then (1 : A) else 0) := by
  rw [formalProductDefect_coeff_pos_eq_filtered_sum
    A e hleft hright]
  apply Finset.sum_congr rfl
  intro q _hq
  rw [formalLogOnePlusProductArgument_pow_coeff_eq_sum_basicFactor]

theorem formalLogOnePlusProductFormulaDefect_coeff_of_pos_coords_eq_sum_card_choices
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (hleft : 0 < e (0 : Fin 2)) (hright : 0 < e (1 : Fin 2)) :
    MvPowerSeries.coeff e
        (formalLogOnePlusProductFormulaDefect A) =
      ∑ q ∈
        (Finset.range (e (0 : Fin 2) + e (1 : Fin 2) + 1)).filter
          (fun q : ℕ => e (0 : Fin 2) ≤ q ∧ e (1 : Fin 2) ≤ q),
        PowerSeries.coeff q (PowerSeries.log A) •
          ((formalLogOnePlusProductArgumentBasicFactorChoices q e).card : A) := by
  rw [formalLogOnePlusProductFormulaDefect_coeff_of_pos_coords_eq_sum_basicFactor
    A e hleft hright]
  apply Finset.sum_congr rfl
  intro q _hq
  rw [formalLogOnePlusProductArgument_basicFactor_sum_eq_card_choices]

theorem sum_range_add_filter_coord_le_reindex
    {R : Type*} [AddCommMonoid R] (a b : ℕ) (F : ℕ → R) :
    (∑ q ∈ (Finset.range (a + b + 1)).filter (fun q => a ≤ q ∧ b ≤ q),
      F q) =
      ∑ m ∈ (Finset.range (a + 1)).filter (fun m => m ≤ b),
        F (a + b - m) := by
  refine Finset.sum_bij'
    (fun q _ => a + b - q)
    (fun m _ => a + b - m)
    ?_ ?_ ?_ ?_ ?_
  · intro q hq
    rw [Finset.mem_filter] at hq ⊢
    constructor
    · rw [Finset.mem_range]
      omega
    · omega
  · intro m hm
    rw [Finset.mem_filter] at hm ⊢
    have hmle_a : m ≤ a := Nat.lt_succ_iff.mp (Finset.mem_range.mp hm.1)
    have hmle_b : m ≤ b := hm.2
    have hleftRewrite : a + b - m = a + (b - m) := by
      exact Nat.add_sub_assoc hmle_b a
    have hrightRewrite : a + b - m = b + (a - m) := by
      rw [Nat.add_comm a b]
      exact Nat.add_sub_assoc hmle_a b
    constructor
    · rw [Finset.mem_range]
      omega
    · constructor
      · rw [hleftRewrite]
        omega
      · rw [hrightRewrite]
        omega
  · intro q hq
    rw [Finset.mem_filter] at hq
    have hqle : q ≤ a + b := Nat.lt_succ_iff.mp (Finset.mem_range.mp hq.1)
    exact Nat.sub_sub_self hqle
  · intro m hm
    rw [Finset.mem_filter] at hm
    have hmle_a : m ≤ a := Nat.lt_succ_iff.mp (Finset.mem_range.mp hm.1)
    have hmle : m ≤ a + b := by omega
    exact Nat.sub_sub_self hmle
  · intro q hq
    rw [Finset.mem_filter] at hq
    have hqle : q ≤ a + b := Nat.lt_succ_iff.mp (Finset.mem_range.mp hq.1)
    simp [Nat.sub_sub_self hqle]

theorem formalLogOnePlusProduct_alternating_sum_choose_eq_zero
    (a b : ℕ) (ha : 0 < a) (hb : 0 < b) :
    (∑ m ∈ Finset.range (a + 1),
      ((-1 : ℚ) ^ m) * (Nat.choose a m : ℚ) *
        (Nat.choose (a + b - 1 - m) (a - 1) : ℚ)) = 0

theorem formalLogOnePlusProduct_alternating_sum_choose_filter_eq_zero
    (a b : ℕ) (ha : 0 < a) (hb : 0 < b) :
    (∑ m ∈ (Finset.range (a + 1)).filter (fun m => m ≤ b),
      ((-1 : ℚ) ^ m) * (Nat.choose a m : ℚ) *
        (Nat.choose (a + b - 1 - m) (a - 1) : ℚ)) = 0 := by
  rw [← formalLogOnePlusProduct_alternating_sum_choose_eq_zero a b ha hb]
  exact
    (Finset.sum_subset (Finset.filter_subset _ _) (fun m hm hnot => by
      have hle_a : m ≤ a := Nat.lt_succ_iff.mp (Finset.mem_range.mp hm)
      have hlt_b : b < m := Nat.lt_of_not_ge (by
        intro hmb
        exact hnot (Finset.mem_filter.mpr ⟨hm, hmb⟩))
      have hchooseZero :
          Nat.choose (a + b - 1 - m) (a - 1) = 0 := by
        apply Nat.choose_eq_zero_of_lt
        omega
      change
        ((-1 : ℚ) ^ m) * (Nat.choose a m : ℚ) *
          (Nat.choose (a + b - 1 - m) (a - 1) : ℚ) = 0
      rw [hchooseZero]
      simp))

theorem formalLogOnePlusProduct_rational_mixed_reindexed_term
    (a b m : ℕ) (ha : 0 < a) (hmle_a : m ≤ a) (hmle_b : m ≤ b) :
    let q := a + b - m
    (a : ℚ) *
        (((-1 : ℚ) ^ (q - 1) / (q : ℚ)) *
          ((Nat.choose q m * Nat.choose (q - m) (q - b) : ℕ) : ℚ)) =
      ((-1 : ℚ) ^ (a + b - 1)) *
        (((-1 : ℚ) ^ m) * (Nat.choose a m : ℚ) *
          (Nat.choose (a + b - 1 - m) (a - 1) : ℚ)) := by
  intro q
  subst q
  have hqpos : 0 < a + b - m := by omega
  have hq_ne : ((a + b - m : ℕ) : ℚ) ≠ 0 := by
    exact_mod_cast (Nat.ne_of_gt hqpos)
  have hq_sub_b : a + b - m - b = a - m := by omega
  have hq_pred : a + b - m - 1 = a + b - 1 - m := by omega
  have hprodNat :
      Nat.choose (a + b - m) m *
          Nat.choose (a + b - m - m) (a + b - m - b) =
        Nat.choose (a + b - m) a * Nat.choose a m := by
    rw [hq_sub_b]
    exact
      (Nat.choose_mul (n := a + b - m) (k := a) (s := m) hmle_a).symm
  have hsuccNat :
      (a + b - m) * Nat.choose (a + b - m - 1) (a - 1) =
        Nat.choose (a + b - m) a * a := by
    calc
      (a + b - m) * Nat.choose (a + b - m - 1) (a - 1)
          =
        ((a + b - m - 1) + 1) *
          Nat.choose (a + b - m - 1) (a - 1) := by
            rw [Nat.sub_add_cancel (Nat.succ_le_of_lt hqpos)]
      _ =
        Nat.choose ((a + b - m - 1) + 1) ((a - 1) + 1) *
          ((a - 1) + 1) := by
            exact Nat.add_one_mul_choose_eq (a + b - m - 1) (a - 1)
      _ = Nat.choose (a + b - m) a * a := by
            rw [Nat.sub_add_cancel (Nat.succ_le_of_lt hqpos),
              Nat.sub_add_cancel (Nat.succ_le_of_lt ha)]
  have hsuccQ :
      ((a + b - m : ℕ) : ℚ) *
          (Nat.choose (a + b - m - 1) (a - 1) : ℚ) =
        (Nat.choose (a + b - m) a : ℚ) * (a : ℚ) := by
    exact_mod_cast hsuccNat
  have hsuccQ' :
      ((a + b - m : ℕ) : ℚ) *
          (Nat.choose (a + b - 1 - m) (a - 1) : ℚ) =
        (Nat.choose (a + b - m) a : ℚ) * (a : ℚ) := by
    simpa [hq_pred] using hsuccQ
  have hsign :
      (-1 : ℚ) ^ (a + b - m - 1) =
        (-1 : ℚ) ^ (a + b - 1) * (-1 : ℚ) ^ m := by
    calc
      (-1 : ℚ) ^ (a + b - m - 1)
          = (-1 : ℚ) ^ ((a + b - 1) + m) := by
            have hadd : (a + b - 1) + m = a + b - m - 1 + 2 * m := by
              omega
            rw [hadd, pow_add, pow_mul]
            simp [pow_two]
      _ = (-1 : ℚ) ^ (a + b - 1) * (-1 : ℚ) ^ m := by
            rw [pow_add]
  rw [hprodNat, hsign]
  field_simp [hq_ne]
  rw [Nat.cast_mul]
  calc
    (a : ℚ) *
        ((Nat.choose (a + b - m) a : ℚ) * (Nat.choose a m : ℚ))
        =
      ((Nat.choose (a + b - m) a : ℚ) * (a : ℚ)) *
        (Nat.choose a m : ℚ) := by
          ring
    _ =
      (((a + b - m : ℕ) : ℚ) *
          (Nat.choose (a + b - 1 - m) (a - 1) : ℚ)) *
        (Nat.choose a m : ℚ) := by
          rw [← hsuccQ']
    _ =
      ((a + b - m : ℕ) : ℚ) * (Nat.choose a m : ℚ) *
        (Nat.choose (a + b - 1 - m) (a - 1) : ℚ) := by
          ring

theorem formalLogOnePlusProduct_rational_mixed_sum_eq_zero
    (a b : ℕ) (ha : 0 < a) (hb : 0 < b) :
    (∑ q ∈
      (Finset.range (a + b + 1)).filter (fun q : ℕ => a ≤ q ∧ b ≤ q),
      (((-1 : ℚ) ^ (q - 1) / (q : ℚ)) *
        ((Nat.choose q (a + b - q) *
          Nat.choose (q - (a + b - q)) (q - b) : ℕ) : ℚ))) = 0 := by
  let F : ℕ → ℚ := fun q =>
    (((-1 : ℚ) ^ (q - 1) / (q : ℚ)) *
      ((Nat.choose q (a + b - q) *
        Nat.choose (q - (a + b - q)) (q - b) : ℕ) : ℚ))
  change
    (∑ q ∈
      (Finset.range (a + b + 1)).filter (fun q : ℕ => a ≤ q ∧ b ≤ q),
      F q) = 0
  rw [sum_range_add_filter_coord_le_reindex a b F]
  have haQ : (a : ℚ) ≠ 0 := by
    exact_mod_cast (Nat.ne_of_gt ha)
  apply (mul_eq_zero.mp ?_).resolve_left haQ
  calc
    (a : ℚ) *
        (∑ m ∈ (Finset.range (a + 1)).filter (fun m => m ≤ b),
          F (a + b - m))
        =
      ∑ m ∈ (Finset.range (a + 1)).filter (fun m => m ≤ b),
        (a : ℚ) * F (a + b - m) := by
          rw [Finset.mul_sum]
    _ =
      ∑ m ∈ (Finset.range (a + 1)).filter (fun m => m ≤ b),
        ((-1 : ℚ) ^ (a + b - 1)) *
          (((-1 : ℚ) ^ m) * (Nat.choose a m : ℚ) *
            (Nat.choose (a + b - 1 - m) (a - 1) : ℚ)) := by
          apply Finset.sum_congr rfl
          intro m hm
          rw [Finset.mem_filter] at hm
          have hmle_a : m ≤ a := Nat.lt_succ_iff.mp (Finset.mem_range.mp hm.1)
          have hmle_b : m ≤ b := hm.2
          have hmle_sum : m ≤ a + b := by omega
          have hsub : a + b - (a + b - m) = m := Nat.sub_sub_self hmle_sum
          change
            (a : ℚ) *
                (((-1 : ℚ) ^ (a + b - m - 1) /
                    ((a + b - m : ℕ) : ℚ)) *
                  ((Nat.choose (a + b - m) (a + b - (a + b - m)) *
                    Nat.choose
                      (a + b - m - (a + b - (a + b - m)))
                      (a + b - m - b) : ℕ) : ℚ)) =
              ((-1 : ℚ) ^ (a + b - 1)) *
                (((-1 : ℚ) ^ m) * (Nat.choose a m : ℚ) *
                  (Nat.choose (a + b - 1 - m) (a - 1) : ℚ))
          rw [hsub]
          exact formalLogOnePlusProduct_rational_mixed_reindexed_term
            a b m ha hmle_a hmle_b
    _ =
      ((-1 : ℚ) ^ (a + b - 1)) *
        (∑ m ∈ (Finset.range (a + 1)).filter (fun m => m ≤ b),
          ((-1 : ℚ) ^ m) * (Nat.choose a m : ℚ) *
            (Nat.choose (a + b - 1 - m) (a - 1) : ℚ)) := by
          rw [Finset.mul_sum]
    _ = 0 := by
          rw [formalLogOnePlusProduct_alternating_sum_choose_filter_eq_zero
            a b ha hb]
          simp

theorem formalLogOnePlusProductFormulaDefect_coeff_of_pos_coords_eq_zero
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ)
    (hleft : 0 < e (0 : Fin 2)) (hright : 0 < e (1 : Fin 2)) :
    MvPowerSeries.coeff e
        (formalLogOnePlusProductFormulaDefect A) = 0

theorem formalLogOnePlusProductFormulaDefect_coeff_eq_zero
    (A : Type*) [CommRing A] [Algebra ℚ A] (e : Fin 2 →₀ ℕ) :
    MvPowerSeries.coeff e
        (formalLogOnePlusProductFormulaDefect A) = 0

theorem formalLogOnePlusProductFormula
    (A : Type*) [CommRing A] [Algebra ℚ A] :
    PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A) =
      formalLogOnePlusProductRightSide A

theorem mvPowerSeries_hasEval_of_finite_topologicallyNilpotent
    {σ : Type*} {S : Type*} [CommRing S] [TopologicalSpace S] [Finite σ]
    {a : σ → S} (hpow : ∀ s, IsTopologicallyNilpotent (a s)) :
    MvPowerSeries.HasEval a

theorem mvPowerSeries_hasEval_fin_two
    {S : Type*} [CommRing S] [TopologicalSpace S] {x y : S}
    (hx : IsTopologicallyNilpotent x) (hy : IsTopologicallyNilpotent y) :
    MvPowerSeries.HasEval (fun i : Fin 2 => if i = 0 then x else y) := by
  apply mvPowerSeries_hasEval_of_finite_topologicallyNilpotent
  intro i
  fin_cases i <;> simp [hx, hy]

theorem formalLogOnePlusProductFormula_aeval
    (A : Type*) [CommRing A] [Algebra ℚ A]
    [UniformSpace A] [IsUniformAddGroup A]
    [CompleteSpace A] [T2Space A] [IsTopologicalRing A]
    [IsLinearTopology A A]
    {a : Fin 2 → A} (ha : MvPowerSeries.HasEval a) :
    MvPowerSeries.aeval ha
        (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) =
      MvPowerSeries.aeval ha (formalLogOnePlusProductRightSide A)

def mvPowerSeriesMonomialValue
    {σ : Type*} {A : Type*} [CommMonoid A]
    (a : σ → A) (d : σ →₀ ℕ) : A

theorem formalLogOnePlusProductArgument_pow_monomialValue_sum_eq
    (A : Type*) [CommRing A] (x y : A) (q : ℕ) :
    (∑ d ∈ (formalLogOnePlusProductArgumentPolynomial A ^ q).support,
      MvPowerSeries.coeff d ((formalLogOnePlusProductArgument A) ^ q) *
        mvPowerSeriesMonomialValue
          (fun i : Fin 2 => if i = 0 then x else y) d) =
      (x + y + x * y) ^ q := by
  classical
  let P : MvPolynomial (Fin 2) A :=
    formalLogOnePlusProductArgumentPolynomial A
  let a : Fin 2 → A := fun i => if i = 0 then x else y
  have hpow :
      ((P ^ q : MvPolynomial (Fin 2) A) : MvPowerSeries (Fin 2) A) =
        (formalLogOnePlusProductArgument A) ^ q := by
    simp [P, formalLogOnePlusProductArgument_eq_coe_polynomial]
  calc
    (∑ d ∈ (formalLogOnePlusProductArgumentPolynomial A ^ q).support,
      MvPowerSeries.coeff d ((formalLogOnePlusProductArgument A) ^ q) *
        mvPowerSeriesMonomialValue
          (fun i : Fin 2 => if i = 0 then x else y) d)
        =
      ∑ d ∈ (P ^ q).support,
        (P ^ q).coeff d * d.prod (fun i e => a i ^ e) := by
          subst P
          subst a
          apply Finset.sum_congr rfl
          intro d hd
          rw [← hpow, MvPolynomial.coeff_coe]
          simp [mvPowerSeriesMonomialValue]
    _ = MvPolynomial.eval a (P ^ q) := by
          rw [MvPolynomial.eval_eq]
          simp [Finsupp.prod]
    _ = (MvPolynomial.eval a P) ^ q := by
          simp
    _ = (x + y + x * y) ^ q := by
          simp [P, a]

theorem hasSum_formalLogOnePlusProductArgument_pow_monomialValue_pair
    (A : Type*) [CommRing A] [TopologicalSpace A] (x y : A) (q : ℕ) :
    HasSum
      (fun d : Fin 2 →₀ ℕ =>
        MvPowerSeries.coeff d ((formalLogOnePlusProductArgument A) ^ q) *
          mvPowerSeriesMonomialValue
            (fun i : Fin 2 => if i = 0 then x else y) d)
      ((x + y + x * y) ^ q) := by
  classical
  let P : MvPolynomial (Fin 2) A :=
    formalLogOnePlusProductArgumentPolynomial A
  let term : (Fin 2 →₀ ℕ) → A := fun d =>
    MvPowerSeries.coeff d ((formalLogOnePlusProductArgument A) ^ q) *
      mvPowerSeriesMonomialValue
        (fun i : Fin 2 => if i = 0 then x else y) d
  have hpow :
      ((P ^ q : MvPolynomial (Fin 2) A) : MvPowerSeries (Fin 2) A) =
        (formalLogOnePlusProductArgument A) ^ q := by
    simp [P, formalLogOnePlusProductArgument_eq_coe_polynomial]
  have hzero :
      ∀ d ∉ (formalLogOnePlusProductArgumentPolynomial A ^ q).support,
        term d = 0 := by
    intro d hd
    have hcoeff_poly :
        (formalLogOnePlusProductArgumentPolynomial A ^ q).coeff d = 0 :=
      by
        by_contra hne
        exact hd (MvPolynomial.mem_support_iff.mpr hne)
    have hcoeff_poly_P : (P ^ q).coeff d = 0 := by
      simpa [P] using hcoeff_poly
    have hcoeff :
        MvPowerSeries.coeff d
            ((formalLogOnePlusProductArgument A) ^ q) = 0 := by
      rw [← hpow]
      rw [MvPolynomial.coeff_coe]
      exact hcoeff_poly_P
    simp [term, hcoeff]
  have hfinite : HasSum term
      (∑ d ∈ (formalLogOnePlusProductArgumentPolynomial A ^ q).support,
        term d) :=
    hasSum_sum_of_ne_finset_zero hzero
  have hsum :
      (∑ d ∈ (formalLogOnePlusProductArgumentPolynomial A ^ q).support,
        term d) =
        (x + y + x * y) ^ q := by
    simpa [term] using
      formalLogOnePlusProductArgument_pow_monomialValue_sum_eq A x y q
  simpa [hsum, term] using hfinite

theorem hasSum_formalLogOnePlusProductArgument_pow_monomialValue_pair_mul_left
    (A : Type*) [CommRing A] [TopologicalSpace A] [IsTopologicalSemiring A]
    (c x y : A) (q : ℕ) :
    HasSum
      (fun d : Fin 2 →₀ ℕ =>
        c * MvPowerSeries.coeff d ((formalLogOnePlusProductArgument A) ^ q) *
          mvPowerSeriesMonomialValue
            (fun i : Fin 2 => if i = 0 then x else y) d)
      (c * (x + y + x * y) ^ q) := by
  refine
    ((hasSum_formalLogOnePlusProductArgument_pow_monomialValue_pair
      A x y q).mul_left c).congr_fun ?_
  intro d
  ring

theorem formalLogOnePlusProductFormula_hasSum_monomialValue_eq
    (A : Type*) [CommRing A] [Algebra ℚ A] [TopologicalSpace A] [T2Space A]
    {a : Fin 2 → A} {L R : A}
    (hleft :
      HasSum
        (fun d : Fin 2 →₀ ℕ =>
          MvPowerSeries.coeff d
              (PowerSeries.subst (formalLogOnePlusProductArgument A) (PowerSeries.log A)) *
            mvPowerSeriesMonomialValue a d) L)
    (hright :
      HasSum
        (fun d : Fin 2 →₀ ℕ =>
          MvPowerSeries.coeff d (formalLogOnePlusProductRightSide A) *
            mvPowerSeriesMonomialValue a d) R) :
    L = R := by
  rw [formalLogOnePlusProductFormula A] at hleft
  exact hleft.unique hright