English
The real-valued limit of the sequence seminormFromConst_seq c f x exists and equals seminormFromConst' hf1 hc hpm x.
Русский
Существуют пределы для последовательности и он равен seminormFromConst' hf1 hc hpm x.
LaTeX
$$Tendsto( seminormFromConst_seq c f x) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))$$
Lean4
/-- `seminormFromConst_seq c f x` is antitone. -/
theorem seminormFromConst_seq_antitone (x : R) : Antitone (seminormFromConst_seq c f x) :=
by
intro m n hmn
simp only [seminormFromConst_seq]
nth_rw 1 [← Nat.add_sub_of_le hmn]
rw [pow_add, ← mul_assoc]
have hc_pos : 0 < f c := lt_of_le_of_ne (apply_nonneg f _) hc.symm
apply le_trans ((div_le_div_iff_of_pos_right (pow_pos hc_pos _)).mpr (map_mul_le_mul f _ _))
cases hmn.eq_or_lt with
| inl heq =>
have hnm : n - m = 0 := by rw [heq, Nat.sub_self n]
rw [hnm, heq, div_le_div_iff_of_pos_right (pow_pos hc_pos _), pow_zero]
conv_rhs => rw [← mul_one (f (x * c ^ n))]
exact mul_le_mul_of_nonneg_left hf1 (apply_nonneg f _)
| inr
hlt =>
have h1 : 1 ≤ n - m := by
rw [Nat.one_le_iff_ne_zero]
exact Nat.sub_ne_zero_of_lt hlt
rw [hpm c h1, mul_div_assoc, div_eq_mul_inv, pow_sub₀ _ hc hmn, mul_assoc, mul_comm (f c ^ m)⁻¹, ←
mul_assoc (f c ^ n), mul_inv_cancel₀ (pow_ne_zero n hc), one_mul, div_eq_mul_inv]
