English
A Lipschitz map on lp(E,p) is Lipschitz in each coordinate when restricted to that coordinate function.
Русский
Липшицево отображение на lp(E,p) имеет Lipschitz-свойство по каждой координате при ограничении на соответствующую координатную функцию.
LaTeX
$$$\\forall i,\\; \\text{LipschitzWith } K (f \\mapsto f_i) \\Rightarrow f \\text{ Lipschitz in i-th coordinate}$$$
Lean4
theorem coordinate [PseudoMetricSpace α] (f : α → ℓ^∞(ι)) (s : Set α) (K : ℝ≥0) :
LipschitzOnWith K f s ↔ ∀ i : ι, LipschitzOnWith K (fun a : α ↦ f a i) s :=
by
simp_rw [lipschitzOnWith_iff_dist_le_mul]
constructor
· intro hfl i x hx y hy
calc
dist (f x i) (f y i) ≤ dist (f x) (f y) := lp.norm_apply_le_norm top_ne_zero (f x - f y) i
_ ≤ K * dist x y := hfl x hx y hy
· intro hgl x hx y hy
apply lp.norm_le_of_forall_le
· positivity
intro i
apply hgl i x hx y hy
