Theorems · Theorem · several complex variables

FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1

∀ (n : ℕ) (p : ℕ → ℝ),
  (∀ (k : ℕ), 0 ≤ p k) →
    ∀ {r a : ℝ},
      0 ≤ r →
        0 ≤ a →
          ∑ k ∈ Finset.Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j, p (c.blocksFun j) ≤
            ∑ j ∈ Finset.Ico 2 (n + 1), r ^ j * (∑ k ∈ Finset.Ico 1 n, a ^ k * p k) ^ j

First technical lemma to control the growth of coefficients of the inverse. Bound the explicit expression for ∑_{k<n+1} aᵏ Qₖ in terms of a sum of powers of the same sum one step before, in a general abstract setup.

Defined in

Mathlib.Analysis.Analytic.Inverse

Cited by

1 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound