English
If hμ1 and μ is nonarchimedean, then smoothingFun μ is nonarchimedean.
Русский
Если hμ1 и μ неархимедова, то smoothingFun μ — неархимедова.
LaTeX
$$IsNonarchimedean (smoothingFun μ)$$
Lean4
/-- If `μ 1 ≤ 1` and `μ` is nonarchimedean, then `smoothingFun μ` is nonarchimedean. -/
theorem isNonarchimedean_smoothingFun (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean μ) : IsNonarchimedean (smoothingFun μ) :=
by
-- Fix `x, y : R`.
intro x y
have hn :
∀ n : ℕ, ∃ m < n + 1, μ ((x + y) ^ (n : ℕ)) ^ (1 / (n : ℝ)) ≤ (μ (x ^ m) * μ (y ^ (n - m : ℕ))) ^ (1 / (n : ℝ)) :=
fun n => RingSeminorm.exists_index_pow_le μ hna x y n
let mu : ℕ → ℕ := fun n => mu μ hn n
set nu : ℕ → ℕ := fun n => n - mu n with hnu
have hmu_le : ∀ n : ℕ, mu n ≤ n := fun n => mu_le μ hn n
have hmu_bdd : ∀ n : ℕ, (mu n : ℝ) / n ∈ Set.Icc (0 : ℝ) 1 := fun n => mu_bdd μ hn n
have hs : Bornology.IsBounded (Set.Icc (0 : ℝ) 1) :=
Metric.isBounded_Icc 0
1
/- Since `0 ≤ (mu n) / n ≤ 1` for all `n`, we can find a subsequence `(ψ n) ⊆ ℕ` such that the
limit of `mu (ψ n) / ψ n` as `n` tends to infinity exists. We denote this limit by `a`. -/
obtain ⟨a, a_in, ψ, hψ_mono, hψ_lim⟩ := tendsto_subseq_of_bounded hs hmu_bdd
rw [closure_Icc] at a_in
set b := 1 - a with hb
have hb_lim : Tendsto ((fun n : ℕ => (nu n : ℝ) / ↑n) ∘ ψ) atTop (𝓝 b) :=
by
apply Tendsto.congr' _ (Tendsto.const_sub 1 hψ_lim)
simp only [EventuallyEq, Function.comp_apply, eventually_atTop, ge_iff_le]
use 1
intro m hm
have h0 : (ψ m : ℝ) ≠ 0 :=
cast_ne_zero.mpr
(_root_.ne_of_gt (lt_of_le_of_lt (_root_.zero_le _) (hψ_mono (Nat.pos_of_ne_zero (one_le_iff_ne_zero.mp hm)))))
rw [← div_self h0, ← sub_div, cast_sub (hmu_le _)]
have b_in : b ∈ Set.Icc (0 : ℝ) 1 := Set.Icc.mem_iff_one_sub_mem.mp a_in
have hnu_le : ∀ n : ℕ, nu n ≤ n := fun n => by simp only [hnu, tsub_le_self]
have hx : limsup (fun n : ℕ => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤ smoothingFun μ x ^ a :=
limsup_mu_le μ hμ1 hmu_le a_in hψ_mono hψ_lim
have hy : limsup (fun n : ℕ => μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤ smoothingFun μ y ^ b :=
limsup_mu_le μ hμ1 hnu_le b_in hψ_mono hb_lim
have hxy :
limsup (fun n => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ)) * μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤
smoothingFun μ x ^ a * smoothingFun μ y ^ b :=
by
have hxy' :
limsup (fun n : ℕ => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ)) * μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤
limsup (fun n : ℕ => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop *
limsup (fun n : ℕ => μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop :=
limsup_mul_le (Frequently.of_forall (fun n => rpow_nonneg (apply_nonneg _ _) _))
(μ_bddAbove μ hμ1 hmu_le x ψ).isBoundedUnder_of_range
(Eventually.of_forall (fun n => rpow_nonneg (apply_nonneg _ _) _))
(μ_bddAbove μ hμ1 hnu_le y ψ).isBoundedUnder_of_range
have h_bdd : IsBoundedUnder LE.le atTop fun n : ℕ => μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)) :=
RingSeminorm.isBoundedUnder μ hμ1 hnu_le ψ
apply
le_trans hxy'
(mul_le_mul hx hy
(le_limsup_of_frequently_le (Frequently.of_forall (fun n ↦ rpow_nonneg (apply_nonneg μ _) _)) h_bdd)
(rpow_nonneg (smoothingFun_nonneg μ hμ1 x) _))
apply le_of_forall_sub_le
intro ε hε
rw [sub_le_iff_le_add]
have h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε :=
by
rw [max_def]
split_ifs with h
· rw [add_le_add_iff_right]
apply
le_trans
(mul_le_mul_of_nonneg_right (rpow_le_rpow (smoothingFun_nonneg μ hμ1 _) h a_in.1)
(rpow_nonneg (smoothingFun_nonneg μ hμ1 _) _))
rw [hb, ← rpow_add_of_nonneg (smoothingFun_nonneg μ hμ1 _) a_in.1 (sub_nonneg.mpr a_in.2), add_sub,
add_sub_cancel_left, rpow_one]
· rw [add_le_add_iff_right]
apply
le_trans
(mul_le_mul_of_nonneg_left (rpow_le_rpow (smoothingFun_nonneg μ hμ1 _) (le_of_lt (not_le.mp h)) b_in.1)
(rpow_nonneg (smoothingFun_nonneg μ hμ1 _) _))
rw [hb, ← rpow_add_of_nonneg (smoothingFun_nonneg μ hμ1 _) a_in.1 (sub_nonneg.mpr a_in.2), add_sub,
add_sub_cancel_left, rpow_one]
apply le_trans _ h_mul
have hex :
∃ n : PNat,
μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ)) * μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)) <
smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε :=
Filter.exists_lt_of_limsup_le
(bddAbove_range_mul (μ_bddAbove μ hμ1 hmu_le _ _) (fun n => rpow_nonneg (apply_nonneg _ _) _)
(μ_bddAbove μ hμ1 hnu_le _ _) fun n => rpow_nonneg (apply_nonneg _ _) _).isBoundedUnder_of_range
hxy hε
obtain ⟨N, hN⟩ := hex
apply
le_trans
(ciInf_le (smoothingSeminormSeq_bddBelow μ _)
⟨ψ N, lt_of_le_of_lt (_root_.zero_le (ψ 0)) (hψ_mono.lt_iff_lt.mpr N.pos)⟩)
apply le_trans _ hN.le
simpa [PNat.mk_coe, hnu, ← mul_rpow (apply_nonneg μ _) (apply_nonneg μ _)] using mu_property μ hn (ψ N)
