pseudoEmetricAux — Mathlib

English

PiLp p α is endowed with the Lp distance, defined coordinatewise with the same case distinction as edist.

Русский

PiLp p α наделено расстоянием Lp, определяемым координатно с тем же разделением по случаям, что и edist.

LaTeX

$$$$\\mathrm{dist}(f,g)=\\begin{cases} \\lvert\\{i\\;|\\;\\mathrm{dist}(f_i,g_i)\\neq 0\\}\\rvert,& p=0,\\\\[2mm] \\bigl(\\sum_i \\mathrm{dist}(f_i,g_i)^{p^{\\mathrm{toReal}}}\\bigr)^{1/p^{\\mathrm{toReal}}},& 0

Lean4

/-- Endowing the space `PiLp 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 pseudoEmetricAux : PseudoEMetricSpace (PiLp p β)
    where
  edist_self := PiLp.edist_self p
  edist_comm := PiLp.edist_comm p
  edist_triangle f g
    h := by
    rcases p.dichotomy with (rfl | hp)
    · simp only [edist_eq_iSup]
      cases isEmpty_or_nonempty ι
      ·
        simp only [ciSup_of_empty, ENNReal.bot_eq_zero, add_zero, nonpos_iff_eq_zero]
          -- Porting note: `le_iSup` needed some help

      refine
        iSup_le fun i =>
          (edist_triangle _ (g i) _).trans <|
            add_le_add (le_iSup (fun k => edist (f k) (g k)) i) (le_iSup (fun k => edist (g k) (h k)) i)
    · simp only [edist_eq_sum (zero_lt_one.trans_le hp)]
      calc
        (∑ i, edist (f i) (h i) ^ p.toReal) ^ (1 / p.toReal) ≤
            (∑ i, (edist (f i) (g i) + edist (g i) (h i)) ^ p.toReal) ^ (1 / p.toReal) :=
          by
          gcongr
          apply edist_triangle
        _ ≤
            (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal) +
              (∑ i, edist (g i) (h i) ^ p.toReal) ^ (1 / p.toReal) :=
          ENNReal.Lp_add_le _ _ _ hp

Похожие утверждения