multipliableUniformlyOn_euler_sin_prod_on_compact

English

On any compact set Z, the family (1 + sineTerm z n) is MultipliableUniformlyOn over n and z ∈ Z.

Русский

На любом компактном множестве Z семейство (1 + sineTerm z n) имеет свойство MultipliableUniformlyOn по n и z ∈ Z.

LaTeX

$$$$\forall Z, \; \text{IsCompact}(Z) \Rightarrow \text{MultipliableUniformlyOn}(\lambda n z. 1 + \text{sineTerm}(z, n), \{Z\}).$$$$

Lean4

theorem multipliableUniformlyOn_euler_sin_prod_on_compact (hZC : IsCompact Z) :
    MultipliableUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n)) { Z } :=
  by
  obtain ⟨u, hu, hu2⟩ := sineTerm_bound_aux hZC
  refine Summable.multipliableUniformlyOn_nat_one_add hZC hu ?_ ?_
  · filter_upwards with n z hz using hu2 n z hz
  · fun_prop

Похожие утверждения