exists_eq_sum_and_forall_sum_mem_of_isPos

English

A simplified variant of the sum-representation lemma with simpler bounds.

Русский

Упрощённый вариант леммы о представлении суммы.

LaTeX

$$same as 133511$$

Lean4

/-- This lemma is included mostly for comparison with the informal literature. Usually
`RootPairing.Base.IsPos.induction_on_add` will be more useful. -/
theorem exists_eq_sum_and_forall_sum_mem_of_isPos {i : ι} (hi : b.IsPos i) :
    ∃ n,
      ∃ f : Fin n → ι,
        range f ⊆ b.support ∧ P.root i = ∑ m, P.root (f m) ∧ ∀ m, ∑ m' ≤ m, P.root (f m') ∈ range P.root :=
  by
  apply hi.induction_on_add (fun j hj ↦ ⟨1, ![j], by simpa⟩)
  intro j k l h₁ ⟨n, f, h₂, h₃, h₄⟩ h₅
  refine ⟨n + 1, Fin.snoc f k, ?_, ?_, fun m ↦ ?_⟩
  · simpa using insert_subset h₅ h₂
  · simp [Fin.sum_univ_castSucc, h₁, h₃]
  · by_cases hm : m < n
    · have : m = (⟨m, hm⟩ : Fin n).castSucc := rfl
      rw [this, Fin.sum_Iic_castSucc]
      simp only [Fin.snoc_castSucc, h₄]
    · replace hm : m = n := by omega
      replace hm : Finset.Iic m = Finset.univ := by ext; simp [hm, Fin.le_def, Fin.is_le]
      simp [hm, Fin.sum_univ_castSucc, ← h₃, ← h₁]

Похожие утверждения