English
seminormFromConst is defined as the seminormFromConst' with the given hypotheses; i.e., seminormFromConst hf1 hc hpm = seminormFromConst' hf1 hc hpm.
Русский
seminormFromConst задается через seminormFromConst' с заданными гипотезами; то есть seminormFromConst hf1 hc hpm = seminormFromConst' hf1 hc hpm.
LaTeX
$$seminormFromConst hf1 hc hpm = seminormFromConst' hf1 hc hpm$$
Lean4
/-- The function `seminormFromConst` is a `RingSeminorm` on `R`. -/
def seminormFromConst : RingSeminorm R
where
toFun := seminormFromConst' hf1 hc hpm
map_zero' :=
tendsto_nhds_unique (seminormFromConst_isLimit hf1 hc hpm 0)
(by simpa [seminormFromConst_seq_zero c (map_zero _)] using tendsto_const_nhds)
add_le' x
y :=
by
apply
le_of_tendsto_of_tendsto' (seminormFromConst_isLimit hf1 hc hpm (x + y))
((seminormFromConst_isLimit hf1 hc hpm x).add (seminormFromConst_isLimit hf1 hc hpm y))
intro n
have h_add : f ((x + y) * c ^ n) ≤ f (x * c ^ n) + f (y * c ^ n) := by simp only [add_mul, map_add_le_add f _ _]
simp only [seminormFromConst_seq, ← add_div]
gcongr
neg'
x :=
by
apply
tendsto_nhds_unique_of_eventuallyEq (seminormFromConst_isLimit hf1 hc hpm (-x))
(seminormFromConst_isLimit hf1 hc hpm x)
simp only [EventuallyEq, eventually_atTop]
use 0
simp only [seminormFromConst_seq, neg_mul, map_neg_eq_map, zero_le, implies_true]
mul_le' x
y :=
by
have hlim :
Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop (𝓝 (seminormFromConst' hf1 hc hpm (x * y))) :=
by
apply
(seminormFromConst_isLimit hf1 hc hpm (x * y)).comp
(tendsto_atTop_atTop_of_monotone (fun _ _ hnm ↦ by simp only [mul_le_mul_iff_right₀, Nat.succ_pos', hnm]) _)
· rintro n; use n; omega
refine
le_of_tendsto_of_tendsto' hlim
((seminormFromConst_isLimit hf1 hc hpm x).mul (seminormFromConst_isLimit hf1 hc hpm y)) (fun n ↦ ?_)
simp only [seminormFromConst_seq]
rw [div_mul_div_comm, ← pow_add, two_mul,
div_le_div_iff_of_pos_right (pow_pos (lt_of_le_of_ne (apply_nonneg f _) hc.symm) _), pow_add, ← mul_assoc,
mul_comm (x * y), ← mul_assoc, mul_assoc, mul_comm (c ^ n)]
exact map_mul_le_mul f (x * c ^ n) (y * c ^ n)
