English
The distance structure on PiLp p α is given by the formula dist f g = ... (coordinatewise as above).
Русский
Структура расстояния на PiLp p α задается по формуле dist f g = ... (координатно как выше).
LaTeX
$$$$\\mathrm{dist}\\text{(definition)}\\; = \\;\\text{coordinatewise formula as above}$$$$
Lean4
/-- Endowing the space `PiLp 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 pseudoMetricAux : PseudoMetricSpace (PiLp p α) :=
PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist
(fun f g => by
rcases p.dichotomy with (rfl | h)
· exact iSup_edist_ne_top_aux f g
· rw [edist_eq_sum (zero_lt_one.trans_le h)]
exact ENNReal.rpow_ne_top_of_nonneg (by positivity) <| ENNReal.sum_ne_top.2 fun _ _ ↦ by finiteness)
fun f g => by
rcases p.dichotomy with (rfl | h)
· rw [edist_eq_iSup, dist_eq_iSup]
cases isEmpty_or_nonempty ι
· simp only [Real.iSup_of_isEmpty, ciSup_of_empty, ENNReal.bot_eq_zero, ENNReal.toReal_zero]
· refine le_antisymm (ciSup_le fun i => ?_) ?_
· rw [← ENNReal.ofReal_le_iff_le_toReal (iSup_edist_ne_top_aux f g), ← PseudoMetricSpace.edist_dist]
-- Porting note: `le_iSup` needed some help
exact le_iSup (fun k => edist (f k) (g k)) i
· refine ENNReal.toReal_le_of_le_ofReal (Real.sSup_nonneg ?_) (iSup_le fun i => ?_)
· rintro - ⟨i, rfl⟩
exact dist_nonneg
· change PseudoMetricSpace.edist _ _ ≤ _
rw [PseudoMetricSpace.edist_dist]
-- Porting note: `le_ciSup` needed some help
exact ENNReal.ofReal_le_ofReal (le_ciSup (Finite.bddAbove_range (fun k => dist (f k) (g k))) i)
· have A (i) : edist (f i) (g i) ^ p.toReal ≠ ⊤ := by finiteness
simp only [edist_eq_sum (zero_lt_one.trans_le h), dist_edist, ENNReal.toReal_rpow,
dist_eq_sum (zero_lt_one.trans_le h), ← ENNReal.toReal_sum fun i _ => A i]
