smoothingSeminorm

In this file, we prove [BGR, Proposition 1.3.2/1][bosch-guntzer-remmert] : if μ is a nonarchimedean seminorm on a commutative ring R, then iInf (fun (n : PNat), (μ(x ^ (n : ℕ))) ^ (1 / (n : ℝ)))is a power-multiplicative nonarchimedean seminorm onR`.

Main Definitions

• smoothingSeminormSeq : the ℝ-valued sequence sending n to ((f( (x ^ n)) ^ (1 / n : ℝ).
• smoothingFun : the iInf of the sequence n ↦ f(x ^ (n : ℕ))) ^ (1 / (n : ℝ).
• smoothingSeminorm : if μ 1 ≤ 1 and μ is nonarchimedean, then smoothingFun is a ring seminorm.

Main Results

• tendsto_smoothingFun_of_map_one_le_one : if μ 1 ≤ 1, then smoothingFun μ x is the limit of smoothingSeminormSeq μ x as n tends to infinity.
• isNonarchimedean_smoothingFun : if μ 1 ≤ 1 and μ is nonarchimedean, then smoothingFun is nonarchimedean.
• isPowMul_smoothingFun : if μ 1 ≤ 1 and μ is nonarchimedean, then smoothingFun μ is power-multiplicative.

References

• [S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert]

Tags

smoothingSeminorm, seminorm, nonarchimedean

@[reducible, inline]

abbrev smoothingSeminormSeq {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) : ℕ → ℝ

The ℝ-valued sequence sending n to (μ (x ^ n))^(1/n : ℝ).

theorem zero_mem_lowerBounds_smoothingSeminormSeq_range {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) : 0 ∈ lowerBounds (Set.range fun (n : ℕ+) => μ (x ^ ↑n) ^ (1 / ↑↑n))

0 is a lower bound of smoothingSeminormSeq.

theorem smoothingSeminormSeq_bddBelow {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) : BddBelow (Set.range fun (n : ℕ+) => μ (x ^ ↑n) ^ (1 / ↑↑n))

smoothingSeminormSeq is bounded below (by zero).

@[reducible, inline]

abbrev smoothingFun {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) : ℝ

The iInf of the sequence n ↦ μ(x ^ (n : ℕ)))^(1 / (n : ℝ).

theorem tendsto_smoothingFun_of_eq_zero {R : Type u_1} [CommRing R] (μ : RingSeminorm R) {x : R} (hx : μ x = 0) : Filter.Tendsto (smoothingSeminormSeq μ x) Filter.atTop (nhds (smoothingFun μ x))

If μ x = 0, then smoothingFun μ x is the limit of smoothingSeminormSeq μ x.

theorem tendsto_smoothingFun_of_ne_zero {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) {x : R} (hx : μ x ≠ 0) : Filter.Tendsto (smoothingSeminormSeq μ x) Filter.atTop (nhds (smoothingFun μ x))

If μ 1 ≤ 1 and μ x ≠ 0, then smoothingFun μ x is the limit of smoothingSeminormSeq μ x.

theorem tendsto_smoothingFun_of_map_one_le_one {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (x : R) : Filter.Tendsto (smoothingSeminormSeq μ x) Filter.atTop (nhds (smoothingFun μ x))

If μ 1 ≤ 1, then smoothingFun μ x is the limit of smoothingSeminormSeq μ x as n tends to infinity.

theorem smoothingFun_nonneg {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (x : R) : 0 ≤ smoothingFun μ x

If μ 1 ≤ 1, then smoothingFun μ x is nonnegative.

theorem smoothingFun_one_le {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) : smoothingFun μ 1 ≤ 1

If μ 1 ≤ 1, then smoothingFun μ 1 ≤ 1.

theorem smoothingFun_le {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) (n : ℕ+) : smoothingFun μ x ≤ μ (x ^ ↑n) ^ (1 / ↑↑n)

For any x and any positive n, smoothingFun μ x ≤ μ (x ^ (n : ℕ))^(1 / n : ℝ).

theorem smoothingFun_le_self {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (x : R) : smoothingFun μ x ≤ μ x

For all x : R, smoothingFun μ x ≤ μ x.

theorem tendsto_smoothingFun_comp {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (x : R) {ψ : ℕ → ℕ} (hψ_mono : StrictMono ψ) : Filter.Tendsto (fun (n : ℕ) => μ (x ^ ψ n) ^ (1 / ↑(ψ n))) Filter.atTop (nhds (smoothingFun μ x))

theorem isNonarchimedean_smoothingFun {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean ⇑μ) : IsNonarchimedean (smoothingFun μ)

If μ 1 ≤ 1 and μ is nonarchimedean, then smoothingFun μ is nonarchimedean.

def smoothingSeminorm {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean ⇑μ) : RingSeminorm R

If μ 1 ≤ 1 and μ is nonarchimedean, then smoothingFun is a ring seminorm.

theorem smoothingSeminorm_map_one_le_one {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean ⇑μ) : (smoothingSeminorm μ hμ1 hna) 1 ≤ 1

If μ 1 ≤ 1 and μ is nonarchimedean, then smoothingSeminorm μ 1 ≤ 1.

theorem isPowMul_smoothingFun {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) : IsPowMul (smoothingFun μ)

If μ 1 ≤ 1 and μ is nonarchimedean, then smoothingFun μ is power-multiplicative.

theorem smoothingFun_of_powMul {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) {x : R} (hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n) : smoothingFun μ x = μ x

If μ 1 ≤ 1 and ∀ (1 ≤ n), μ (x ^ n) = μ x ^ n, then smoothingFun μ x = μ x.

theorem smoothingFun_apply_of_map_mul_eq_mul {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) {x : R} (hx : ∀ (y : R), μ (x * y) = μ x * μ y) : smoothingFun μ x = μ x

If μ 1 ≤ 1 and ∀ y : R, μ (x * y) = μ x * μ y, then smoothingFun μ x = μ x.

theorem smoothingSeminorm_apply_of_map_mul_eq_mul {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean ⇑μ) {x : R} (hx : ∀ (y : R), μ (x * y) = μ x * μ y) : (smoothingSeminorm μ hμ1 hna) x = μ x

If μ 1 ≤ 1, μ is nonarchimedean, and ∀ y : R, μ (x * y) = μ x * μ y, then smoothingSeminorm μ x = μ x.

theorem smoothingFun_of_map_mul_eq_mul {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) {x : R} (hx : ∀ (y : R), μ (x * y) = μ x * μ y) (y : R) : smoothingFun μ (x * y) = smoothingFun μ x * smoothingFun μ y

If μ 1 ≤ 1, and x is multiplicative for μ, then it is multiplicative for smoothingFun.

theorem smoothingSeminorm_of_mul {R : Type u_1} [CommRing R] (μ : RingSeminorm R) (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean ⇑μ) {x : R} (hx : ∀ (y : R), μ (x * y) = μ x * μ y) (y : R) : (smoothingSeminorm μ hμ1 hna) (x * y) = (smoothingSeminorm μ hμ1 hna) x * (smoothingSeminorm μ hμ1 hna) y

If μ 1 ≤ 1, μ is nonarchimedean, and x is multiplicative for μ, then x is multiplicative for smoothingSeminorm.