Field-free lemmas of the germ theory

Lemmas about exponents and radius vectors that do not depend on the coefficient field: the weight of a monomial under a shift of one exponent; the degree of an exponent after removing one coordinate; the identification ℕ ≃ (Fin 1 →₀ ℕ) of one-variable exponents and the regrouping of sums over exponents by degree; the coordinate swap swapEmb k of the index set and its action on exponents; and the splitting ν = partI I ν + partT I ν of an exponent into its part on a set I of coordinates and its complement, with the elementary properties used to slice a series along a coordinate subspace. The germ theory (Hironaka/Analytic/Germ) imports this module.

Shifting an exponent

theorem Analytic.monomialEval_add_single {n : ℕ} (ρ : Fin n → NNReal) (ν : Fin n →₀ ℕ) (k : Fin n) : monomialEval ρ (ν + Finsupp.single k 1) = monomialEval ρ ν * ρ k

The degree after removing one coordinate

theorem Analytic.degree_tsub_single {n : ℕ} {θ : Fin n →₀ ℕ} {k : Fin n} (hk : θ k ≠ 0) : Finsupp.degree (θ - Finsupp.single k 1) + 1 = Finsupp.degree θ

Exponents in one variable and sums regrouped by degree

noncomputable def Analytic.natEquivFin1 : ℕ ≃ (Fin 1 →₀ ℕ)

ℕ ≃ (Fin 1 →₀ ℕ), d ↦ d e_0.

Equations

• One or more equations did not get rendered due to their size.

theorem Analytic.natEquivFin1_apply (d : ℕ) : natEquivFin1 d = Finsupp.single 0 d

theorem Analytic.ennreal_tsum_eq_tsum_sum_degreeSet {n : ℕ} (g : (Fin n →₀ ℕ) → ENNReal) : ∑' (ν : Fin n →₀ ℕ), g ν = ∑' (d : ℕ), ∑ ν ∈ degreeSet n d, g ν

Regrouping an ℝ≥0∞-valued sum over exponents by degree.

theorem Analytic.degree_fin1 (d : Fin 1 →₀ ℕ) : Finsupp.degree d = d 0

The coordinate swap on exponents

def Analytic.swapEmb {n : ℕ} (k : Fin (n + 1)) : Fin (n + 1) ↪ Fin (n + 1)

The coordinate swap 0 ↔ k as an embedding of the index set.

Equations

• Analytic.swapEmb k = Equiv.toEmbedding (Equiv.swap 0 k)

theorem Analytic.swapEmb_apply {n : ℕ} (k i : Fin (n + 1)) : (swapEmb k) i = (Equiv.swap 0 k) i

theorem Analytic.embDomain_swapEmb_swapEmb {n : ℕ} (k : Fin (n + 1)) (ν : Fin (n + 1) →₀ ℕ) : Finsupp.embDomain (swapEmb k) (Finsupp.embDomain (swapEmb k) ν) = ν

theorem Analytic.embDomain_swapEmb_apply_zero {n : ℕ} (k : Fin (n + 1)) (ν : Fin (n + 1) →₀ ℕ) : (Finsupp.embDomain (swapEmb k) ν) 0 = ν k

theorem Analytic.embDomain_swapEmb_apply_k {n : ℕ} (k : Fin (n + 1)) (ν : Fin (n + 1) →₀ ℕ) : (Finsupp.embDomain (swapEmb k) ν) k = ν 0

Splitting an exponent along a set of coordinates

def Analytic.partI {n : ℕ} (I : Finset (Fin n)) (ν : Fin n →₀ ℕ) : Fin n →₀ ℕ

The part of an exponent supported on I.

Equations

• Analytic.partI I ν = Finsupp.filter (fun (x : Fin n) => x ∈ I) ν

def Analytic.partT {n : ℕ} (I : Finset (Fin n)) (ν : Fin n →₀ ℕ) : Fin n →₀ ℕ

The part of an exponent supported off I.

Equations

• Analytic.partT I ν = Finsupp.filter (fun (x : Fin n) => x ∉ I) ν

theorem Analytic.partI_apply {n : ℕ} (I : Finset (Fin n)) (ν : Fin n →₀ ℕ) (k : Fin n) : (partI I ν) k = if k ∈ I then ν k else 0

theorem Analytic.partT_apply {n : ℕ} (I : Finset (Fin n)) (ν : Fin n →₀ ℕ) (k : Fin n) : (partT I ν) k = if k ∉ I then ν k else 0

theorem Analytic.partI_add_partT {n : ℕ} (I : Finset (Fin n)) (ν : Fin n →₀ ℕ) : partI I ν + partT I ν = ν

theorem Analytic.partI_add {n : ℕ} (I : Finset (Fin n)) (μ ν : Fin n →₀ ℕ) : partI I (μ + ν) = partI I μ + partI I ν

theorem Analytic.partT_add {n : ℕ} (I : Finset (Fin n)) (μ ν : Fin n →₀ ℕ) : partT I (μ + ν) = partT I μ + partT I ν

theorem Analytic.partT_partI {n : ℕ} (I : Finset (Fin n)) (ν : Fin n →₀ ℕ) : partT I (partI I ν) = 0

theorem Analytic.partI_partT {n : ℕ} (I : Finset (Fin n)) (ν : Fin n →₀ ℕ) : partI I (partT I ν) = 0

theorem Analytic.partI_eq_self_of_partT_eq_zero {n : ℕ} (I : Finset (Fin n)) {β : Fin n →₀ ℕ} (h : partT I β = 0) : partI I β = β

theorem Analytic.partT_eq_self_of_partI_eq_zero {n : ℕ} (I : Finset (Fin n)) {γ : Fin n →₀ ℕ} (h : partI I γ = 0) : partT I γ = γ

theorem Analytic.degree_partI {n : ℕ} (I : Finset (Fin n)) (ν : Fin n →₀ ℕ) : Finsupp.degree (partI I ν) = ∑ k ∈ I, ν k

noncomputable def Analytic.splitEquiv {n : ℕ} (I : Finset (Fin n)) : { β : Fin n →₀ ℕ // partT I β = 0 } × { γ : Fin n →₀ ℕ // partI I γ = 0 } ≃ (Fin n →₀ ℕ)

Exponents split into their I-part and their complement.

Equations

• One or more equations did not get rendered due to their size.

theorem Analytic.monomialEval_eq_inv_mul {n : ℕ} (ρ : Radius n) (β γ : Fin n →₀ ℕ) : monomialEval (↑ρ) γ = (monomialEval (↑ρ) β)⁻¹ * monomialEval (↑ρ) (β + γ)

theorem Analytic.ennreal_tsum_split {n : ℕ} (I : Finset (Fin n)) (g : (Fin n →₀ ℕ) → ENNReal) : ∑' (ν : Fin n →₀ ℕ), g ν = ∑' (β : { β : Fin n →₀ ℕ // partT I β = 0 }) (γ : { γ : Fin n →₀ ℕ // partI I γ = 0 }), g (↑β + ↑γ)

Regrouping an ℝ≥0∞-valued sum over exponents by I-part and complement.