English
The map prod_continuous_toLp asserts that the map toLp is continuous from WithLp p (α × β) to α × β.
Русский
Пусть выполнено: отображение toLp непрерывно от WithLp p (α × β) к α × β.
LaTeX
$$$$\\text{Continuous}(\\mathrm{toLp}\, p\, (α × β))$$$$
Lean4
/-- Endowing the space `WithLp p (α × β)` with the `L^p` pseudoemetric structure. This definition is
not satisfactory, as it does not register the fact that the topology and the uniform structure
coincide with the product one. Therefore, we do not register it as an instance. Using this as a
temporary pseudoemetric space instance, we will show that the uniform structure is equal (but not
defeq) to the product one, and then register an instance in which we replace the uniform structure
by the product one using this pseudoemetric space and `PseudoEMetricSpace.replaceUniformity`. -/
def prodPseudoEMetricAux [PseudoEMetricSpace α] [PseudoEMetricSpace β] : PseudoEMetricSpace (WithLp p (α × β))
where
edist_self := prod_edist_self p
edist_comm := prod_edist_comm p
edist_triangle f g
h := by
rcases p.dichotomy with (rfl | hp)
· simp only [prod_edist_eq_sup]
exact
sup_le ((edist_triangle _ g.fst _).trans <| add_le_add le_sup_left le_sup_left)
((edist_triangle _ g.snd _).trans <| add_le_add le_sup_right le_sup_right)
· simp only [prod_edist_eq_add (zero_lt_one.trans_le hp)]
calc
(edist f.fst h.fst ^ p.toReal + edist f.snd h.snd ^ p.toReal) ^ (1 / p.toReal) ≤
((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal + (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^
(1 / p.toReal) :=
by gcongr <;> apply edist_triangle
_ ≤
(edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
(edist g.fst h.fst ^ p.toReal + edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal) :=
by
have :=
ENNReal.Lp_add_le {0, 1} (if · = 0 then edist f.fst g.fst else edist f.snd g.snd)
(if · = 0 then edist g.fst h.fst else edist g.snd h.snd) hp
simp only [Finset.mem_singleton, not_false_eq_true, Finset.sum_insert, Finset.sum_singleton,
reduceCtorEq] at this
exact this
