English
Definition of a pseudo-emetric structure on WithLp p (α × β) built from the distance dist, choosing the appropriate formula depending on p to ensure the uniform structure mirrors the product.
Русский
Определение псевдоэмэтерического пространства для WithLp p (α × β) через расстояние dist, соChoosing формулой в зависимости от p так, чтобы единичная и мультипликативная структуры совпадали с произведением.
LaTeX
$$$$\text{prodPseudoEMetricAux} : PseudoEMetricSpace (WithLp p (α × β))\;\text{где}\; edist = \text{dist}\,,$$$$
Lean4
/-- Endowing the space `WithLp p (α × β)` with the `L^p` pseudometric structure. This definition is
not satisfactory, as it does not register the fact that the topology, the uniform structure, and the
bornology coincide with the product ones. 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 and the bornology by the product ones using this pseudometric space,
`PseudoMetricSpace.replaceUniformity`, and `PseudoMetricSpace.replaceBornology`.
See note [reducible non-instances] -/
abbrev prodPseudoMetricAux [PseudoMetricSpace α] [PseudoMetricSpace β] : PseudoMetricSpace (WithLp p (α × β)) :=
PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist
(fun f g => by
rcases p.dichotomy with (rfl | h)
· exact prod_sup_edist_ne_top_aux f g
· rw [prod_edist_eq_add (zero_lt_one.trans_le h)]
finiteness)
fun f g => by
rcases p.dichotomy with (rfl | h)
· rw [prod_edist_eq_sup, prod_dist_eq_sup]
refine le_antisymm (sup_le ?_ ?_) ?_
· rw [← ENNReal.ofReal_le_iff_le_toReal (prod_sup_edist_ne_top_aux f g), ← PseudoMetricSpace.edist_dist]
exact le_sup_left
· rw [← ENNReal.ofReal_le_iff_le_toReal (prod_sup_edist_ne_top_aux f g), ← PseudoMetricSpace.edist_dist]
exact le_sup_right
· refine ENNReal.toReal_le_of_le_ofReal ?_ ?_
· simp only [le_sup_iff, dist_nonneg, or_self]
· simp [-ofReal_max]
· have h1 : edist f.fst g.fst ^ p.toReal ≠ ⊤ := by finiteness
have h2 : edist f.snd g.snd ^ p.toReal ≠ ⊤ := by finiteness
simp only [prod_edist_eq_add (zero_lt_one.trans_le h), dist_edist, ENNReal.toReal_rpow,
prod_dist_eq_add (zero_lt_one.trans_le h), ← ENNReal.toReal_add h1 h2]
