borelize gives "failed to create binder..."

Stream: mathlib4

[Felix Weilacher]

I'm testing out adding a StandardBorelSpace class whose relationship to PolishSpace is analogous to the relationship between PolishSpace and MetricSpace + CompleteSpace. Using the PolishSpace code as a model, here's my attempt.

import Mathlib.Topology.MetricSpace.Polish
import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

variable (α : Type*)

class StandardBorelSpace [MeasurableSpace α] : Prop where
  polish : ∃ _ : TopologicalSpace α, BorelSpace α ∧ PolishSpace α

class UpgradedStandardBorel extends MeasurableSpace α, TopologicalSpace α,
  BorelSpace α, PolishSpace α

noncomputable
def upgradeStandardBorel [MeasurableSpace α] [h : StandardBorelSpace α] :
    UpgradedStandardBorel α := by
  choose τ hb hp using h.polish
  constructor

The idea is to use letI := upgradeStandardBorel X if one needs to fix a compatible Polish topology on a given Standard Borel Space X. This seems to work for some basic stuff, but when combining the above step with borelize X I get an error:

example [i : MeasurableSpace α] [StandardBorelSpace α] : False := by
  letI := upgradeStandardBorel α
  borelize α -- failed to create binder due to failure when reverting variable dependencies

I have no idea what this error message means. I can still manually prove i = borel α, which is what I want borelize to be doing:

example [i : MeasurableSpace α] [StandardBorelSpace α] : False := by
  letI := upgradeStandardBorel α
  have : i = borel α := BorelSpace.measurable_eq --works

[Eric Wieser]

I'd be curious to know how this kind of error can be debugged; is there any way to get a stack trace?

[Eric Wieser]

Note you can also use the lift tactic here:

instance : CanLift (MeasurableSpace α) (UpgradedStandardBorel α)
  (fun x => by infer_instance) (fun x => StandardBorelSpace α) where
    prf x hx := by
      obtain ⟨_, _, _⟩ := hx.polish
      exact ⟨⟨⟩, rfl⟩

example [i : MeasurableSpace α] [StandardBorelSpace α] : False := by
  lift i to UpgradedStandardBorel α using inferInstance
  sorry

[Felix Weilacher]

thanks! that does seem to work with borelize.

Is there a way to do lift i to UpgradedStandardBorel α using inferInstance without a name for the MeasurableSpace instance (since typically we won't have one)?

[Eric Wieser]

Yes, lift ‹MeasurableSpace α› to UpgradedStandardBorel α using inferInstance

[Felix Weilacher]

thanks!

[Felix Weilacher]

Just to try and understand the original error, it seems the issue occurs with subst:

example [i : MeasurableSpace α] [StandardBorelSpace α] : False := by
  letI := upgradeStandardBorel α
  have : i = borel α := BorelSpace.measurable_eq
  subst i -- -- failed to create binder due to failure when reverting variable dependencies

[Felix Weilacher]

actually, though borelize does not give any errors after the lift tactic, it still does not have the desired behavior. For example.

example [i : MeasurableSpace α] [StandardBorelSpace α] (s : Set α) (hs : MeasurableSet s): False := by
  lift i to UpgradedStandardBorel α using inferInstance
  borelize α

The type of hs after this is @MeasurableSet α inferInstance s when I'd like it to be @MeasurableSet α (borel α) s.
Here is a more typical case where the latter type is achieved:

example [i : MeasurableSpace α] [TopologicalSpace α] [BorelSpace α] (s : Set α) (hs : MeasurableSet s): False := by
  borelize α

[Eric Wieser]

I'm not sure why you need borelize after the lift tactic; isn't BorelSpace α enough, which is now in the context?

[Felix Weilacher]

from the docstring for borelize:
"if α is a topological space with instances [MeasurableSpace α] [BorelSpace α], then borelize α replaces the former instance by borel α"
For example:

example [i : MeasurableSpace α] [TopologicalSpace α] [BorelSpace α] (s : Set α) (hs : MeasurableSet s): False := by
  --have : @MeasurableSet _ (borel α) s := hs
  /- type mismatch
  hs
has type
  @MeasurableSet α i s : Prop
but is expected to have type
  @MeasurableSet α (borel α) s : Prop
  -/
  borelize α
  have : @MeasurableSet _ (borel α) s := hs --works

[Felix Weilacher]

The BorelSpace instance is enough to manually get things done by rewriting with BorelSpace.measurable_eq as needed, but one of the main uses of borelize is to make this happen automatically.

[Eric Wieser]

I guess my question is, why do you need borel α instead of [BorelSpace α]? Are there any lemmas that only work for borel α?

[Felix Weilacher]

I don't understand your question. borel α is a sigma algebra on α and BorelSpace α says that ‹MeasurableSpace α› = borel α. The borelize tactic is a common way to make use of a [BorelSpace α] hypothesis.

[Felix Weilacher]

Oh maybe I understand your question. For instance when changing topologies, it is useful to be able to make direct reference to @borel α t for various t

[Notification Bot]

This topic was moved here from #lean4 > borelize gives "failed to create binder..." by Scott Morrison.

[Eric Wieser]

Felix Weilacher said:

For instance when changing topologies, it is useful to be able to make direct reference to @borel α t for various t

I guess in this case the analogy is having [@BorelSpace α t] for various t, which I claim is equally useful, but perhaps harder to end up with

[Felix Weilacher]

note that it would actually be [@BorelSpace α t m] for various topologies t and sigma algebras m = borel t.

[Felix Weilacher]

which seems to defeat the point

[Eric Wieser]

You don't ever care that m = borel t by definition though, unless you have a lemma in mind that specifically mentions borel t

[Eric Wieser]

It's hard for me to tell if there's an #xy problem here, because your y is currently just sorry in all your examples!

[Felix Weilacher]

ok, here's an example currently in mathlib which I believe is a good example of borelize being used in the way I'd like to use it.

theorem _root_.MeasurableSet.analyticSet_image {X Y : Type*} [TopologicalSpace X] [PolishSpace X]
    [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y]
    [OpensMeasurableSpace Y] {f : X → Y} [SecondCountableTopology (range f)] {s : Set X}
    (hs : MeasurableSet s) (hf : Measurable f) : AnalyticSet (f '' s) := by
  borelize X
  rcases hf.exists_continuous with ⟨τ', hle, hfc, hτ'⟩
  letI m' : MeasurableSpace X := @borel _ τ'
  haveI b' : BorelSpace X := ⟨rfl⟩
  have hle := borel_anti hle
  exact (hle _ hs).analyticSet.image_of_continuous hfc

note that borel_anti is a lemma which specifically mentions borel t. Since the conclusion does not mention the topology on X. I'd like to replace [TopologicalSpace X] [PolishSpace X][BorelSpace X] with [h : StandardBorelSpace X]. And add something to the effect of letI := upgradeStandardBorel to the start of the proof to add in instances of [TopologicalSpace X] [PolishSpace X][BorelSpace X] to the context. I have also tried doing this more directly with

  letI := h.polish.choose
  letI := h.polish.choose_spec.1
  letI := h.polish.choose_spec.2

Both result in borelize X giving the error message "failed to create binder due to failure when reverting variable dependencies".

btw I am able to prove my version of this lemma without borelize X by doing a rewrite manually.

[Pol'tta / Miyahara Kō]

Who ported the borelize tactic is me.
The cause of this error seems that i = borel α's RHS is depends on i.
borel requires TopologicalSpace, but this is synthesized from i in this case:

[i : MeasurableSpace α] →(upgradeStandardBorel) [UpgradedStandardBorel α] → [TopologicalSpace α]

So, subst fails. borelize should give better error message in this case. I will open the PR later.

[Felix Weilacher]

Thanks for the explanation. It seems like there's no hope of using subst in this situation then? For now I will add a lemma

theorem eq_borel_upgradeStandardBorel [MeasurableSpace α] [StandardBorelSpace α] :
    ‹MeasurableSpace α› = @borel α (upgradeStandardBorel α).toTopologicalSpace :=
  @BorelSpace.measurable_eq _ (upgradeStandardBorel α).toTopologicalSpace _
    (upgradeStandardBorel α).toBorelSpace

and just rewrite with it when necessary.

[Pol'tta / Miyahara Kō]

It seem hard to use subst.
By the way, I could to prove this lemma without borelize:

theorem _root_.MeasurableSet.analyticSet_image {X Y : Type*} [MeasurableSpace X]
    [StandardBorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y]
    [OpensMeasurableSpace Y] {f : X → Y} [SecondCountableTopology (range f)] {s : Set X}
    (hs : MeasurableSet s) (hf : Measurable f) : AnalyticSet (f '' s) := by
  letI := upgradeStandardBorel X
  rw [BorelSpace.measurable_eq (α := X)] at hs
  rcases hf.exists_continuous with ⟨τ', hle, hfc, hτ'⟩
  letI m' : MeasurableSpace X := @borel _ τ'
  haveI b' : BorelSpace X := ⟨rfl⟩
  have hle := borel_anti hle
  exact (hle _ hs).analyticSet.image_of_continuous hfc

[Felix Weilacher]

Felix Weilacher said:

btw I am able to prove my version of this lemma without borelize X by doing a rewrite manually.

Yes, this is what I ended up doing as well.

[Felix Weilacher]

It's still nicer when borelize handles it automatically, but oh well.

[Pol'tta / Miyahara Kō]

#7231

[Yaël Dillies]

Felix Weilacher said:

note that it would actually be [@BorelSpace α t m] for various topologies t and sigma algebras m = borel t.

I think that also means you could introduce a BorelSpace[t] notation.

[Yaël Dillies]

See Continuous[t], IsOpen[t]...