diamond problem with edist on Lp space

Stream: new members

[Vincent Beffara]

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*} {mα : 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]

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]

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]

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]

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]

(docs#Lp.has_edist for reference)

[Eric Wieser]

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

[Eric Wieser]

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

[Vincent Beffara]

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]

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

[Vincent Beffara]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

Fixed in #13388

[Sebastien Gouezel]

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]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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