English
The cartesian product of analytic functions in a neighborhood is analytic.
Русский
Каркасная пара аналитичных функций в окрестности является аналитичной.
LaTeX
$$$\text{AnalyticOnNhd}(f, s) \land \text{AnalyticOnNhd}(g, s) \Rightarrow \text{AnalyticOnNhd}(x \mapsto (f(x), g(x)), s)$$$
Lean4
/-- The radius of the Cartesian product of two formal series is the minimum of their radii. -/
theorem radius_prod_eq_min (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G) :
(p.prod q).radius = min p.radius q.radius := by
apply le_antisymm
· refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
rw [le_min_iff]
have := (p.prod q).isLittleO_one_of_lt_radius hr
constructor
all_goals
apply FormalMultilinearSeries.le_radius_of_isBigO
refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO
rw [norm_mul, norm_norm, norm_mul, norm_norm]
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
· apply le_max_left
· apply le_max_right
· refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
rw [lt_min_iff] at hr
have := ((p.isLittleO_one_of_lt_radius hr.1).add (q.isLittleO_one_of_lt_radius hr.2)).isBigO
refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)
rw [norm_mul, norm_norm, ← add_mul, norm_mul]
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_
apply Real.le_norm_self
