Radius vectors, exponents and monomials

The part of the convergent-series library that does not depend on the coefficient field, shared by the real modules Hironaka/Analytic/ConvSeries/* and the general ones over K = ℝ or ℂ in Hironaka/Analytic/ConvSeries/*:

• the monomial monomialEval x ν = x^ν of a point x : Fin m → R over any commutative monoid R;
• radius vectors ρ : Fin m → ℝ≥0, their monomials monomialEval ρ ν = ρ^ν, and the type Radius m of radius vectors with positive entries (the polyradii of the majorant norms, [GR71, Kap. I]);
• the enumeration expList ν of an exponent ν of degree Finsupp.degree ν = |ν|, the finite set degreeSet m n of exponents of degree n, the count vector countVec k of a tuple of coordinate indices, and the regrouping of sums over exponents by degree or along antidiagonals (hasSum_sum_degreeSet, hasSum_sum_antidiagonal, stated for any regular topological monoid).

Not in the sources: elementary bookkeeping for the majorant norms and for the evaluation of series.

Monomials over a commutative monoid

@[elab_without_expected_type]

def Analytic.monomialEval {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin m → R) (ν : Fin m →₀ ℕ) : R

The monomial x^ν = ∏ k, x k ^ ν k of a point x, over any commutative monoid (the points of the analytic library are x : Fin m → K with K = ℝ or ℂ, and the radius vectors ρ : Fin m → ℝ≥0). The monoid is read off x, not the expected type, so that (monomialEval ρ ν : ℝ≥0∞) coerces a radius monomial.

Equations

• Analytic.monomialEval x ν = ν.prod fun (k : Fin m) (n : ℕ) => x k ^ n

@[simp]

theorem Analytic.monomialEval_zero {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin m → R) : monomialEval x 0 = 1

theorem Analytic.monomialEval_add {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin m → R) (μ ν : Fin m →₀ ℕ) : monomialEval x (μ + ν) = monomialEval x μ * monomialEval x ν

theorem Analytic.monomialEval_eq_prod {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin m → R) (ν : Fin m →₀ ℕ) : monomialEval x ν = ∏ k : Fin m, x k ^ ν k

x^ν = ∏_k x_k^{ν_k} over all coordinates.

theorem Analytic.monomialEval_single_pow {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin m → R) (k : Fin m) (n : ℕ) : monomialEval x (Finsupp.single k n) = x k ^ n

x^{n e_k} = x_k^n.

theorem Analytic.monomialEval_cons {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin (m + 1) → R) (k : ℕ) (y : Fin m →₀ ℕ) : monomialEval x (Finsupp.cons k y) = x 0 ^ k * monomialEval (Fin.tail x) y

Radius vectors

theorem Analytic.monomialEval_pos {m : ℕ} {ρ : Fin m → NNReal} (hρ : ∀ (k : Fin m), 0 < ρ k) (ν : Fin m →₀ ℕ) : 0 < monomialEval ρ ν

theorem Analytic.monomialEval_le_monomialEval {m : ℕ} {ρ ρ' : Fin m → NNReal} (h : ∀ (k : Fin m), ρ k ≤ ρ' k) (ν : Fin m →₀ ℕ) : monomialEval ρ ν ≤ monomialEval ρ' ν

theorem Analytic.coe_monomialEval {m : ℕ} (ρ : Fin m → NNReal) (ν : Fin m →₀ ℕ) : ↑(monomialEval ρ ν) = ν.prod fun (k : Fin m) (n : ℕ) => ↑(ρ k) ^ n

theorem Analytic.monomialEval_one {m : ℕ} (ν : Fin m →₀ ℕ) : monomialEval (fun (x : Fin m) => 1) ν = 1

@[reducible, inline]

abbrev Analytic.Radius (m : ℕ) : Type

A radius vector with positive entries, ρ ∈ (0, ∞)^m.

Equations

• Analytic.Radius m = { ρ : Fin m → NNReal // ∀ (k : Fin m), 0 < ρ k }

@[instance_reducible]

instance Analytic.Radius.instCoeFunForallFinNNReal {m : ℕ} : CoeFun (Radius m) fun (x : Radius m) => Fin m → NNReal

Equations

• Analytic.Radius.instCoeFunForallFinNNReal = { coe := Subtype.val }

theorem Analytic.Radius.pos {m : ℕ} (ρ : Radius m) (k : Fin m) : 0 < ↑ρ k

def Analytic.Radius.min {m : ℕ} (ρ ρ' : Radius m) : Radius m

The pointwise minimum of two radius vectors.

Equations

• ρ.min ρ' = ⟨fun (k : Fin m) => min (↑ρ k) (↑ρ' k), ⋯⟩

theorem Analytic.Radius.min_le_left {m : ℕ} (ρ ρ' : Radius m) (k : Fin m) : ↑(ρ.min ρ') k ≤ ↑ρ k

theorem Analytic.Radius.min_le_right {m : ℕ} (ρ ρ' : Radius m) (k : Fin m) : ↑(ρ.min ρ') k ≤ ↑ρ' k

def Analytic.Radius.one (m : ℕ) : Radius m

The constant radius vector 1.

Equations

• Analytic.Radius.one m = ⟨fun (x : Fin m) => 1, ⋯⟩

def Analytic.Radius.tail {m : ℕ} (ρ : Radius (m + 1)) : Radius m

The base radius of a radius in m + 1 variables (the distinguished coordinate is 0).

Equations

• ρ.tail = ⟨fun (k : Fin m) => ↑ρ k.succ, ⋯⟩

theorem Analytic.Radius.exists_le {m : ℕ} (ρ : Radius m) : ∃ (r : NNReal), 0 < r ∧ ∀ (k : Fin m), r ≤ ↑ρ k

Every radius vector admits a positive common lower bound r ≤ ρ_k (the product of the min 1 ρ_k).

theorem Analytic.monomialEval_pos' {m : ℕ} (ρ : Radius m) (ν : Fin m →₀ ℕ) : 0 < monomialEval (↑ρ) ν

Exponents

noncomputable def Analytic.expList {m : ℕ} (ν : Fin m →₀ ℕ) : List (Fin m)

An enumeration of the exponent ν as a list with ν k entries equal to k; its length is the degree |ν| = ∑ k, ν k (Finsupp.degree).

Equations

• Analytic.expList ν = (Finsupp.toMultiset ν).toList

theorem Analytic.length_expList {m : ℕ} (ν : Fin m →₀ ℕ) : (expList ν).length = Finsupp.degree ν

noncomputable def Analytic.degreeSet (m n : ℕ) : Finset (Fin m →₀ ℕ)

The exponents of degree n.

Equations

• Analytic.degreeSet m n = Finset.univ.finsuppAntidiag n

theorem Analytic.mem_degreeSet {m n : ℕ} {ν : Fin m →₀ ℕ} : ν ∈ degreeSet m n ↔ Finsupp.degree ν = n

theorem Analytic.pow_le_monomialEval {m : ℕ} {ρ : Fin m → NNReal} {r : NNReal} (hr : ∀ (k : Fin m), r ≤ ρ k) {n : ℕ} {ν : Fin m →₀ ℕ} (hν : Finsupp.degree ν = n) : r ^ n ≤ monomialEval ρ ν

Exponents of degree n have ρ^ν ≥ r^n when r ≤ ρ_k for all k.

theorem Analytic.pairwiseDisjoint_degreeSet {m : ℕ} (s : Finset ℕ) : (↑s).PairwiseDisjoint (degreeSet m)

The degree sets are pairwise disjoint.

noncomputable def Analytic.countVec {m n : ℕ} (k : Fin n → Fin m) : Fin m →₀ ℕ

The count vector ν(k) = ∑_i single (k i) 1 of a tuple of coordinate indices.

Equations

• Analytic.countVec k = ∑ i : Fin n, Finsupp.single (k i) 1

theorem Analytic.degree_countVec {m n : ℕ} (k : Fin n → Fin m) : Finsupp.degree (countVec k) = n

theorem Analytic.sum_card_fiber_countVec {m : ℕ} (n : ℕ) : ∑ ν ∈ degreeSet m n, ↑{k : Fin n → Fin m | countVec k = ν}.card = ↑m ^ n

The fibre counts over the exponents of degree n add up to m^n.

Sums regrouped by degree and along antidiagonals

theorem Analytic.summable_sum_degreeSet {m : ℕ} {w : (Fin m →₀ ℕ) → ℝ} (hw0 : ∀ (ν : Fin m →₀ ℕ), 0 ≤ w ν) (hw : Summable w) : Summable fun (n : ℕ) => ∑ ν ∈ degreeSet m n, w ν

The degree-wise sums of a summable nonnegative family are summable, with the same total.

theorem Analytic.summable_of_summable_sum_degreeSet {m : ℕ} {w : (Fin m →₀ ℕ) → ℝ} (hw0 : ∀ (ν : Fin m →₀ ℕ), 0 ≤ w ν) (hs : Summable fun (n : ℕ) => ∑ ν ∈ degreeSet m n, w ν) : Summable w

A nonnegative family on the exponents whose degree-wise sums are summable is summable.

theorem Analytic.hasSum_sum_degreeSet {m : ℕ} {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] [T3Space E] [ContinuousAdd E] {g : (Fin m →₀ ℕ) → E} {a : E} (hg : HasSum g a) : HasSum (fun (n : ℕ) => ∑ ν ∈ degreeSet m n, g ν) a

Regrouping a convergent sum over exponents by degree.

theorem Analytic.hasSum_sum_antidiagonal {m : ℕ} {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] [T3Space E] [ContinuousAdd E] {h : (Fin m →₀ ℕ) × (Fin m →₀ ℕ) → E} {a : E} (hh : HasSum h a) : HasSum (fun (ν : Fin m →₀ ℕ) => ∑ p ∈ Finset.antidiagonal ν, h p) a

A summable family on pairs of exponents, regrouped by the sum of the pair.

Monomials at the enumeration and the count vector of an exponent

theorem Analytic.prod_map_expList {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin m → R) (ν : Fin m →₀ ℕ) : (List.map x (expList ν)).prod = monomialEval x ν

theorem Analytic.monomialEval_sum {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin m → R) {ι : Type u_2} (s : Finset ι) (g : ι → Fin m →₀ ℕ) : monomialEval x (∑ i ∈ s, g i) = ∏ i ∈ s, monomialEval x (g i)

@[simp]

theorem Analytic.monomialEval_single {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin m → R) (j : Fin m) : monomialEval x (Finsupp.single j 1) = x j

theorem Analytic.monomialEval_countVec {m : ℕ} {R : Type u_1} [CommMonoid R] (x : Fin m → R) {n : ℕ} (k : Fin n → Fin m) : monomialEval x (countVec k) = ∏ i : Fin n, x (k i)