English
If a function on a product space is continuous along vertical fibers {a}×t for a∈s and Lipschitz along horizontal fibers s×{b} with the same constant K, then it is continuous on s×t (under subset/closure hypotheses).
Русский
Если функция на произведении пространств непрерывна вдоль вертикальных волокон {a}×t для a∈s и липшицева вдоль горизонтальных волокон s×{b} с единым константным K, то она непрерывна на s×t при некоторых условиях про замыкание.
LaTeX
$$$\\forall f,\\forall s,t, (hs' : s'\\subseteq s) (hss': s \\subseteq \\overline{s'}) (K: \\mathbb{R}_{\\ge 0}) \quad (ha: \\forall a\\in s', ContinuousOn (\\lambda y. f(a,y)) t) (hb: \\forall b\\in t, LipschitzOnWith K (\\lambda x. f(x,b)) s) \\Rightarrow ContinuousOn f (s ×ˢ t)$$$
Lean4
/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical fiber”
`{a} × t`, `a ∈ s`, and is Lipschitz continuous on each “horizontal fiber” `s × {b}`, `b ∈ t`
with the same Lipschitz constant `K`. Then it is continuous on `s × t`. Moreover, it suffices
to require continuity on vertical fibers for `a` from a subset `s' ⊆ s` that is dense in `s`.
The actual statement uses (Lipschitz) continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`
instead of continuity of `f` on subsets of the product space. -/
theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith [PseudoEMetricSpace α] [TopologicalSpace β]
[PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β} (hs' : s' ⊆ s) (hss' : s ⊆ closure s') (K : ℝ≥0)
(ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t) (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) :
ContinuousOn f (s ×ˢ t) := by
rintro ⟨x, y⟩ ⟨hx : x ∈ s, hy : y ∈ t⟩
refine EMetric.nhds_basis_closed_eball.tendsto_right_iff.2 fun ε (ε0 : 0 < ε) => ?_
replace ε0 : 0 < ε / 2 := ENNReal.half_pos ε0.ne'
obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ (δ : ℝ≥0∞) * ↑(3 * K) < ε / 2 :=
ENNReal.exists_nnreal_pos_mul_lt ENNReal.coe_ne_top ε0.ne'
rw [← ENNReal.coe_pos] at δpos
rcases EMetric.mem_closure_iff.1 (hss' hx) δ δpos with ⟨x', hx', hxx'⟩
have A : s ∩ EMetric.ball x δ ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds _ δpos)
have B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y :=
inter_mem self_mem_nhdsWithin (ha x' hx' y hy (EMetric.closedBall_mem_nhds (f (x', y)) ε0))
filter_upwards [nhdsWithin_prod A B] with ⟨a, b⟩ ⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩
calc
edist (f (a, b)) (f (x, y)) ≤
edist (f (a, b)) (f (x', b)) + edist (f (x', b)) (f (x', y)) + edist (f (x', y)) (f (x, y)) :=
edist_triangle4 _ _ _ _
_ ≤ K * (δ + δ) + ε / 2 + K * δ := by
gcongr
· refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
exact (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)
· exact hby
· exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)
_ = δ * ↑(3 * K) + ε / 2 := by push_cast; ring
_ ≤ ε / 2 + ε / 2 := by gcongr
_ = ε := ENNReal.add_halves _
