English
If f is analytic at z and f(z) ≠ 0, then g is analytic at z if and only if the scaled function z ↦ f(z) · g(z) is analytic at z.
Русский
Если f аналитична в точке z и f(z) ≠ 0, то g аналитична в z тогда и только тогда, когда функция z ↦ f(z)·g(z) аналитична в z.
LaTeX
$$$\mathit{AnalyticAt}_{\mathfrak k}(f,z) \land f(z) \neq 0 \Rightarrow \left( \mathit{AnalyticAt}_{\mathfrak k}(g,z) \iff \mathit{AnalyticAt}_{\mathfrak k}\bigl(\lambda w. f(w)\,g(w)\bigr)(z) \right).$$$
Lean4
theorem analyticAt_iff_analytic_fun_smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {z : E}
(h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) : AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z ↦ f z • g z) z :=
by
constructor
· exact fun a ↦ h₁f.smul a
· intro hprod
rw [analyticAt_congr (g := (f⁻¹ • f) • g), smul_assoc]
· exact (h₁f.inv h₂f).fun_smul hprod
· filter_upwards [h₁f.continuousAt.preimage_mem_nhds (compl_singleton_mem_nhds_iff.2 h₂f)]
intro y hy
rw [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff] at hy
simp [hy]
/- A function is analytic at a point iff it is analytic after scalar
multiplication with a non-vanishing analytic function. -/
