Zulip Chat Archive

Stream: new members

Topic: diamond problem with edist on Lp space


Vincent Beffara (Apr 12 2022 at 07:29):

I wanted to prove that there is an isometric embedding of Lp of a sub-sigma-field onto Lp (which should be trivial), but am having problem with instances of emetric spaces. Boiling it down to a MWE:

import measure_theory.function.lp_space
import topology.metric_space.isometry
open measure_theory
variables {α : Type*} { : measurable_space α} {μ : measure α}

example : isometry (id : Lp  1 μ  Lp  1 μ) :=
begin
  intros a b,
  rw [Lp.edist_def]
  -- rewrite tactic failed, did not find instance of the pattern
end

example : isometry (id : Lp  1 μ  Lp  1 μ) :=
begin
  intros a b,
  convert (rfl : edist (id a) (id b) = edist a b),
  -- new goal: pseudo_emetric_space.to_has_edist = Lp.has_edist
end

How am I supposed to do this proof using the Lp API? (Well, for this particular case refl works, but that will not help me in my actual problem.)

Rémy Degenne (Apr 12 2022 at 07:39):

I know I am not answering your question here, but isn't the isometry you want something like docs#measure_theory.Lp_meas_to_Lp_trim_lie, composed with docs#submodule.subtypeₗᵢ in order to go from Lp_meas to Lp ?

Vincent Beffara (Apr 12 2022 at 07:56):

Yes, I know must be obtainable this way (and in any case the immediate reason I need the isometry is to get continuity from it to play around with induction principles, but I can prove continuity by hand because I know ae-equality of the relevant functions - in fact stating the equality of dist or edist works). It's just that for some reason that I would like to understand, explicit dist picks the right instance but isometry choses the wrong one - my current mental model is that the one isometry chooses is the more generic one, while Lp.dist knows to pick the more specific one.

Don't worry I am starting to get your hints that Lp_meas is nicer to handle that Lp _ _ (\mu.trim _) :-)

Rémy Degenne (Apr 12 2022 at 07:57):

def Lp_trim_to_Lp_li {F α : Type*} [normed_group F] [normed_space  F]
  {p : 0} [hp : fact (1  p)] {m m0 : measurable_space α} {μ : measure α}
  (hm : m  m0) :
  (Lp F p (μ.trim hm)) →ₗᵢ[] Lp F p μ :=
(submodule.subtypeₗ (Lp_meas F  m p μ)).comp
  (Lp_meas_to_Lp_trim_lie F  p μ hm).symm.to_linear_isometry

Rémy Degenne (Apr 12 2022 at 08:00):

Sorry, but I can't help you with that dist problem. I have no idea of what happens. Maybe someone else can help.

Eric Wieser (Apr 12 2022 at 08:14):

(docs#Lp.has_edist for reference)

Eric Wieser (Apr 12 2022 at 08:15):

My guess is that that shouldn't be defined in terms of ennreal.of_real

Eric Wieser (Apr 12 2022 at 08:16):

Because that's not how the default in src#pseudo_metric_space is defined

Vincent Beffara (Apr 12 2022 at 09:46):

Ah so IIUC, Lp has a pseudo_emetric_space instance so it gets pseudo_emetric_space.to_has_edist from that, but Lp.has_edist is conflicting with it. Would a solution be to simply remove Lp.has_edist then?

(BTW, is there a way to ask lean to show where an instance is coming from, like trace_instance {pseudo_emetric_space (Lp ...)} would tell me that is comes from emetric_space from metric_space from normed_space from a particular definition? Here I traced it back to docs#measure_theory.Lp.has_norm which is like 4 lines higher in the lean file but many instance layers above, but that was mostly browsing the docs and guessing.)

Eric Wieser (Apr 12 2022 at 10:06):

You can hover over the diamond in the goal view to trace it back

Vincent Beffara (Apr 12 2022 at 10:18):

Thanks for the tip! I finally realized also that after saying letI : metric_space (Lp ℝ 1 μ) := by apply_instance I see

_inst: metric_space (Lp  1 μ) := normed_group.to_metric_space

and clicking on the right-hand side takes me to the definition even if there is no diamond.

Vincent Beffara (Apr 12 2022 at 10:28):

Ah, slowly realizing that the point of Lp.has_edist is that it does not depend on [hp : fact (1 ≤ p)]

Eric Wieser (Apr 12 2022 at 11:55):

The bug here is the normed_space.of_core in docs#measure_theory.Lp.normed_space

Eric Wieser (Apr 12 2022 at 11:58):

Which says "discard the existing edist and dist definitions, and define brand new ones"

Eric Wieser (Apr 12 2022 at 12:10):

Fixed in #13388

Sebastien Gouezel (Apr 12 2022 at 12:19):

Isn't the bug rather in the definition of edist: one could make sure that it is defeq to the one corresponding to the of_core construction, no?

Sebastien Gouezel (Apr 12 2022 at 12:24):

In fact I agree that your approach in #13388 is better, as it allows to have a nicer definitional formula for the edist.

Eric Wieser (Apr 12 2022 at 12:24):

The natural choice of edist is neither the one we actually have right now, or the one that's generated by normed_group.of_core

Sebastien Gouezel (Apr 12 2022 at 12:25):

Yes, let me fix that on #13388 if you don't mind.

Eric Wieser (Apr 12 2022 at 12:25):

Probably making docs#measure_theory.Lp.edist_def true by rfl is the right definition

Eric Wieser (Apr 12 2022 at 12:25):

Go for it - I left if out because I didn't know if anyone cared, and wanted to keep the PR small


Last updated: Dec 20 2023 at 11:08 UTC