interior of le is lt

Stream: Is there code for X?

[Alex Kontorovich]

We have isOpen_lt and isClosed_le. Do we have something like the following (and what are the conditions under which it's even true)?

theorem interior_of_le_is_lt {α : Type _} {β : Type _} [TopologicalSpace α] [LinearOrder α]
    [OrderClosedTopology α] [TopologicalSpace β] {f : β → α} {g : β → α}
    (hf : Continuous f) (hg : Continuous g) : interior {b | f b ≤ g b} = {b | f b < g b} := sorry

[Anatole Dedecker]

This is always false for f = g right?

[Kevin Buzzard]

No, because beta could be empty.

[Kevin Buzzard]

It's just almost always false.

[Anatole Dedecker]

The funny part is I thought about it and decided "oh there’s no need to mention it, after all my friends always get annoyed why I mention these empty sets subtleties". But thanks for reminding me there’s no need to be ashamed of that here 😜

[Antoine Chambert-Loir]

No need to be afraid of the empty set.

[Anatole Dedecker]

Oh I completely agree! I’ve just learned not to insist on it too much otherwise it annoys people. Reminds me of that time when we were asked "when is the direct sum of vector spaces (considered as the subset of the product) equal to their product", the expected answer being "when there are finitely many factors", but I had to explain that the right answer was "when there are finitely many nontrivial factors"

[Eric Wieser]

Is Countable {x | f x = g x} sufficient to make it true?

[Jireh Loreaux]

Not in general. E.g., what if the topology has an isolated point?

[Anatole Dedecker]

There are many things that can go wrong here. One way is indeed when f and g are equal on a set with nonempty interior, but even when f equals g at a single non-isolated point bad things can still happen, for example if f is always smaller than g

[Eric Rodriguez]

Is this true in R^n with the countability/nonempty interior of the equal points?

[Anatole Dedecker]

No, see my last message

[Anatole Dedecker]

E.g f := 0 and g := fun x => x^2

[Anatole Dedecker]

I don't know enough of differential topology to give more useful conditions, but this reminds me of transersality in some way: you want your functions to cross not too often, and to cross for real when they do (and in some sense this second condition implies the first)

[Anatole Dedecker]

Well actually it's a bit more than "reminding me" because it definitely works if $g - f : \mathbb{R}^n \to \mathbb{R}$ is differentiable and has $0$ as a regular value

[Anatole Dedecker]

(right?)

[Kevin Buzzard]

Is 0 a regular value if n=0 because it doesn't work then

[Anatole Dedecker]

You made me doubt for a second but I don't think it is because the differential can't be surjective from $\mathbb{R}^0$ to $\mathbb{R}$.

[Yury G. Kudryashov]

We have docs#lt_subset_interior_le

[Yury G. Kudryashov]

Added by @Yaël Dillies in !3#10653

[Alex Kontorovich]

Ok let's specialize things a bit. Say we have a MetricSpace. Do we know that interior {x | dist x y ≤ z} = {x | dist x y < z}? (What conditions on the metric space are needed for this to be true?...)

[Kevin Buzzard]

That's not true for eg the integers.

[Alex Kontorovich]

Right, so under what conditions is it true?

[Alex Kontorovich]

We do know that the former is closed (Metric.isClosed_ball) and the latter open (Metric.isOpen_ball)

[Eric Wieser]

docs#interior_closedBall looks like it is practically defeq to your question.

[Alex Kontorovich]

Ah perfect, thanks!

[Eric Wieser]

(it assumes NormedSpace ℝ E, I have no idea if it generalizes)

[Alex Kontorovich]

Yes, I'll probably need to assume that as well.

[Yury G. Kudryashov]

There are 2 versions. One assumes [Nontrivial E], another one assumes r ≠ 0.

[Alex Kontorovich]

Yeah, I poked around a bit, and this should be true much more generally than for NormedSpaces... But seems not entirely trivial to get the correct generality...

[Yury G. Kudryashov]

E.g., it is true in the hyperbolic geometry but fails for one positive radius on the sphere.

[Jireh Loreaux]

Nontrivial metric spaces where the interior of every closed ball is the open ball are necessarily perfect, but this condition isn't sufficient in general.

[Alex Kontorovich]

Yes, so what would be sufficient in general. I'm still looking around, and maybe it's its own class???

[Kevin Buzzard]

It probably won't be true for any nonempty compact space because the metric will be bounded and will attain its bounds

[Anatole Dedecker]

Well the obvious condition is ∀ x y, ∃ᶠ z in 𝓝 y, dist x y < dist x z, but that's almost tautological...

[Alex Kontorovich]

Yes, what I'm learning is that such a condition seems not to have been considered previously? It doesn't have a "name" (not that names are all that great - I'm looking at you, Perfect...).

[Anatole Dedecker]

Well we certainly don't have it in mathlib, and I've never heard of it. What is your use case?

[Alex Kontorovich]

Yes, I've been looking for it and this issue seems not to be addressed anywhere as far as I can tell? Seems like a fundamental question?? Here's the use case:

[Alex Kontorovich]

I'm trying out a purely topological version of fundamental domains. To allow the domain to be as general as possible, I assume that the translates of the closures cover, while the interiors are pairwise disjoint:

structure IsFundamentalDomain (G : Type _) {α : Type _} [One G] [SMul G α] [TopologicalSpace α]
    (s : Set α) : Prop where
  protected covers : (⋃ g : G, closure (g • s)) = univ
  protected disjoint : Pairwise <| (Disjoint on fun g : G ↦ interior (g • s))

(I'm renaming the old IsFundamentalDomain to IsAEFundamentalDomain, as @Yury G. Kudryashov suggested. We'll see if this experiment works out...)

[Alex Kontorovich]

Then I define, for a MetricSpace, a DirichletPolyhedron (for which it's useful to have "DirichletSet"s isolated):

variable (G : Type _) [Group G] [Countable G] {α : Type _} [MetricSpace α] [MulAction G α]

def DirichletSet (x : α) (g : G) : Set α := { y : α | dist x y ≤ dist (g • x) y }

def DirichletPolyhedron (x : α) : Set α := ⋂ g : G, DirichletSet G x g

[Alex Kontorovich]

I'm able to prove that these indeed cover. (It's nontrivial; quite fun actually, first year grad stuff...)

theorem IsCover_of_DirichletPolyhedron [ProperSpace α] [i₁ : ProperlyDiscontinuousSMul G α]
    (x : α) : ⋃ (g : G), closure (g • DirichletPolyhedron G x) = univ := ...

[Alex Kontorovich]

(As you see, I need to assume ProperlyDiscontinuousSMul, as expected. I also need to assume ProperSpace, as it turns out. I have no problems with that.)

[Alex Kontorovich]

The issue comes with pairwise disjointedness:

theorem IsDisjoint_of_DirichletPolyhedron (x : α) (hx : ∀ g : G, g • x ≠ x) : ∀ (g₁ g₂ : G),
    g₁ ≠ g₂ →
    Disjoint (interior (g₁ • DirichletPolyhedron G x)) (interior (g₂ • DirichletPolyhedron G x))
    :=

[Alex Kontorovich]

Of course now I need to assume that x is not the fixed point of any g : G

[Alex Kontorovich]

If I can prove that, then of course I can conclude that a DirichletPolyhedron is indeed a fundamental domain:

theorem IsFundamentalDomain_of_DirichletPolyhedron [ProperSpace α]
    [i₁ : ProperlyDiscontinuousSMul G α] (x : α) (hx : ∀ g : G, g • x ≠ x) :
    IsFundamentalDomain G (DirichletPolyhedron G x) where
      covers := IsCover_of_DirichletPolyhedron G x
      disjoint := IsDisjoint_of_DirichletPolyhedron G x hx

[Alex Kontorovich]

For IsDisjoint_of_DirichletPolyhedron, the argument I have in mind is of course that

def DirichletSet₀ (x : α) (g : G) : Set α := { y : α | dist x y < dist (g • x) y }

lemma interior_DirichletSet (x : α) (g : G) :
    interior (DirichletSet G x g) = DirichletSet₀ G x g := ...?

But what are some "natural" conditions under which this is true?? That's the use case...

[Alex Kontorovich]

At the moment, I don't have a better idea than to make a new definition for this condition (that is, ∀ x y, ∃ᶠ z in 𝓝 y, dist x y < dist x z), and assume it to continue making progress...?

[Anatole Dedecker]

I think it can work only with a condition on the action (and the chosen x, but you could also require it for all x) which seems quite natural to me: for all g, h, the set of ys which are the same distance from g • x and h • x has empty interior

[Anatole Dedecker]

(Sorry I’m on my phone)

[Arend Mellendijk]

Alex Kontorovich said:

Of course now I need to assume that x is not the fixed point of any g : G

To be pedantic, there is one exception!

[Anatole Dedecker]

Alex Kontorovich said:

For IsDisjoint_of_DirichletPolyhedron, the argument I have in mind is of course that

def DirichletSet₀ (x : α) (g : G) : Set α := { y : α | dist x y < dist (g • x) y }

lemma interior_DirichletSet (x : α) (g : G) :
    interior (DirichletSet G x g) = DirichletSet₀ G x g := ...?

But what are some "natural" conditions under which this is true?? That's the use case...

To be clear this lemma would still be false (I think at least)

[Anatole Dedecker]

Alex Kontorovich said:

The issue comes with pairwise disjointedness:

theorem IsDisjoint_of_DirichletPolyhedron (x : α) (hx : ∀ g : G, g • x ≠ x) : ∀ (g₁ g₂ : G),
    g₁ ≠ g₂ →
    Disjoint (interior (g₁ • DirichletPolyhedron G x)) (interior (g₂ • DirichletPolyhedron G x))
    :=

But I think this one would work

[Alex Kontorovich]

Yes, as you say, interior_DirichletSet isn't important for the final goal, which is IsDisjoint_of_DirichletPolyhedron.

[Alex Kontorovich]

I'm still flabbergasted that this doesn't seem to be addressed in the literature? (This is a very well-known construction...) People just automatically/implicitly assume that something like interior_DirichletSet holds for any reasonable MetricSpace but there's not an agreed-upon definition of "reasonable"??..

[Arend Mellendijk]

Alex Kontorovich said:

The issue comes with pairwise disjointedness:

theorem IsDisjoint_of_DirichletPolyhedron (x : α) (hx : ∀ g : G, g • x ≠ x) : ∀ (g₁ g₂ : G),
    g₁ ≠ g₂ →
    Disjoint (interior (g₁ • DirichletPolyhedron G x)) (interior (g₂ • DirichletPolyhedron G x))
    :=

I hope I'm not missing something, but consider $\alpha = (\mathbb{R} \times \{0\}) \cup (\mathbb{Z} \times \{1\}) \subset \mathbb{R^2}$ with the translation action of $G=\mathbb{Z}$. Take $x=(1/2,0)$. Then the interior of the dirichlet polyhedron of x contains two isolated points from $\mathbb{Z}$ which intersect the interiors of its two neighbours.

[Anatole Dedecker]

Indeed you need assumptions, either on the action or on the space

[Alex Kontorovich]

Ok I think I've gotten to the bottom of this. The condition, which I'm calling ExtendableSpace is a very natural one, it seems to me, and turns out (though maybe it's "obvious") that it's completely equivalent to the question of interior of a closed ball being an open ball: (I added the condition x ≠ y to avoid nonsense with Nontrivial)

import Mathlib.Topology.MetricSpace.Basic

open Set
open scoped Topology

structure ExtendableSpace (α : Type _) [PseudoMetricSpace α] : Prop where
  protected extendable : ∀ x y : α, x ≠ y → ∃ᶠ z in 𝓝 y, dist x y < dist x z

lemma interior_closedBall'' {α : Type _} [PseudoMetricSpace α] {hα : ExtendableSpace α} (x : α)
    (r : ℝ) (hr : r ≠ 0) : interior (Metric.closedBall x r) = Metric.ball x r := by
  cases' hr.lt_or_lt with hr hr
  · rw [Metric.closedBall_eq_empty.2 hr, Metric.ball_eq_empty.2 hr.le, interior_empty]
  refine Subset.antisymm ?_ Metric.ball_subset_interior_closedBall
  intro y hy
  by_cases x_eq_y : x = y
  · rw [x_eq_y]
    exact Metric.mem_ball_self hr
  obtain ⟨t, ⟨t_isOpen, t_in_closedBall⟩, y_in_t⟩ := hy
  have extend := (hα.extendable x y x_eq_y)
  rw [Filter.frequently_iff] at extend
  obtain ⟨z, z_in_t, dist_xz⟩ := extend (IsOpen.mem_nhds t_isOpen y_in_t)
  have z_in_ball : z ∈ Metric.closedBall x r := mem_of_subset_of_mem t_in_closedBall z_in_t
  rw [Metric.mem_closedBall, dist_comm] at z_in_ball
  rw [Metric.mem_ball, dist_comm]
  linarith

theorem NotMemBallSelf {α : Type _} [PseudoMetricSpace α] (x y : α) :
    ¬ y ∈ Metric.ball x (dist x y) := by
  rw [Metric.mem_ball, dist_comm]
  linarith

lemma Extendable_of_interior_closedBall {α : Type _} [MetricSpace α]
    (h : ∀ x : α, ∀ (r : ℝ), r ≠ 0 → interior (Metric.closedBall x r) = Metric.ball x r) :
    ExtendableSpace α where
      extendable := by
        intro x y x_ne_y
        by_contra hh
        simp_rw [Filter.not_frequently, Filter.eventually_iff, not_lt] at hh
        have ball_in_𝓝 : Metric.closedBall x (dist x y) ∈ 𝓝 y
        · convert hh
          ext z
          simp [Metric.mem_closedBall, Metric.mem_ball, dist_comm, mem_setOf]
        have := interior_mem_nhds.mpr ball_in_𝓝
        rw [h x (dist x y) (ne_of_gt (dist_pos.mpr x_ne_y)), mem_nhds_iff] at this
        obtain ⟨t, t_in_ball, -, y_in_t⟩ := this
        have y_in : y ∈ Metric.ball x (dist x y) := mem_of_mem_of_subset y_in_t t_in_ball
        exact NotMemBallSelf x y y_in

theorem Extendable_iff_interior_closedBall {α : Type _} [MetricSpace α] :
    ExtendableSpace α ↔
    ∀ x : α, ∀ (r : ℝ), r ≠ 0 → interior (Metric.closedBall x r) = Metric.ball x r :=
  ⟨fun i ↦ @interior_closedBall'' α _ i, fun h ↦ Extendable_of_interior_closedBall h⟩

Then one can refactor interior_closedBall by proving that NormedSpaces are Extendable. Sound worthwhile to you all?

I'm guessing (but haven't worked out the details yet) that it's exactly what I need to get the DirichletPolyhedron stuff to work, TBD...

[Jireh Loreaux]

Since Extendable_iff_interior_closedBall is true, why wouldn't you just make the type class:

class InteriorClosedBall (α : Type _) [PseudoMetricSpace α] : Prop where
  protected interior_closedBall : ∀ (x : α) (r : ℝ), r ≠ 0 → interior (Metric.closedBall x r) = Metric.ball x r

If we were going to do this, that seems the more natural statement. However, at this point I don't yet see the value added. If the only instance you have is for normed spaces over ℝ, then that's still the only situation in which it applies, so why not just leave the normed space hypothesis instead? In addition, unless we can locate other use cases (and even if we can), it would be nice to have some reference to literature supporting this concept.

[Alex Kontorovich]

Yes, this concept seems to be completely missing from the literature!

[Alex Kontorovich]

My next use case is for Dirichlet domains

[Alex Kontorovich]

These are usually done in the context of group actions on Riemannian manifolds, but I don't (yet) see why they can't be done on general metric spaces, as long as one assumes ExtendableSpace

[Kevin Buzzard]

How about the upper half plane with the hyperbolic metric for an example which isn't a vector space?

[Alex Kontorovich]

The InteriorClosedBall structure seems less flexible to me; I feel like I'll need ExtendableSpace more directly...

[Alex Kontorovich]

Kevin Buzzard said:

How about the upper half plane with the hyperbolic metric for an example which isn't a vector space?

That's certainly a use case! We could show that the "standard" fundamental domain for the action of $SL(2,\Z)$ is a Dirichlet domain...

[Anatole Dedecker]

Anatole Dedecker said:

I think it can work only with a condition on the action (and the chosen x, but you could also require it for all x) which seems quite natural to me: for all g, h distinct, the set of ys which are the same distance from g • x and h • x has empty interior

For your use case this much weaker (EDIT: it's not weaker at all!) assumption seems more adapted to me, and also geometrically intuitive. That doesn't mean we shouldn't add Extendable, but you could always say that the condition is always true assuming Extendable.

[Jireh Loreaux]

Well, okay, but the extendable condition could just be a lemma. The ball condition is what I would expect to be easier to check in practice (but maybe I'm wrong).

[Kevin Buzzard]

Right -- I thought that the upper half plane was the use case. What does Serre do in Course in Arithmetic?

[Alex Kontorovich]

I haven't checked Serre, but every other book/article I've scanned in the last few days just moves implicitly from interiors of closed balls to open balls, without as much as a comment...

[Alex Kontorovich]

Anatole Dedecker said:

Anatole Dedecker said:

I think it can work only with a condition on the action (and the chosen x, but you could also require it for all x) which seems quite natural to me: for all g, h distinct, the set of ys which are the same distance from g • x and h • x has empty interior

For your use case this much weaker assumption seems more adapted to me, and also geometrically intuitive. That doesn't mean we shouldn't add Extendable, but you could always say that the condition is always true assuming Extendable.

Yes, I thought about this condition as well. It requires an action, whereas I just want some "soft" condition on an abstract metric space...? Having played with it a bit, it seems to me that Extendable is a rather natural and useful notion!...?

[Jireh Loreaux]

See also this stack exchange answer which provides the extendable ↔ interior_closedBall fact.

[Jireh Loreaux]

(Or rather, closure of the open ball is the closed ball)

[Jireh Loreaux]

I suppose Extendable would also be satisfied by ℝ≥0-normed spaces, but that's a kind of artificial example (despite its potential utility). Nevermind, we don't have those

[Alex Kontorovich]

Damn, I did a google search for interiors of closed balls, but google didn't automatically also search for closures of open balls! We need better AI!...

[Alex Kontorovich]

Kevin Buzzard said:

Right -- I thought that the upper half plane was the use case. What does Serre do in Course in Arithmetic?

One comment is that the upper half plane has a Riemannian structure, so this Extendable condition will certainly hold in that context (we'll see how easy it is to formalize...)

[Jireh Loreaux]

Also this Math Overflow which hints at a different characterization, but the link on that answer is broken.

[Alex Kontorovich]

Yes, so maybe that's a more natural way of phrasing it, that for any fixed x, the map y ↦ dist x y has no local extrema?

[Jireh Loreaux]

Oh, interesting: this shows that in a locally separable metric space the condition can only fail for countably many radii.

[Jireh Loreaux]

Yeah, at this point, I'm just trying to get a feel for what exists, I retract my claim about which condition may be easiest/most natural.

[Anatole Dedecker]

Alex Kontorovich said:

Yes, so maybe that's a more natural way of phrasing it, that for any fixed x, the map y ↦ dist x y has no local extrema?

That's basically the condition I gave but probably nicer to work with indeed

[Alex Kontorovich]

Jireh Loreaux said:

Oh, interesting: this shows that in a locally separable metric space the condition can only fail for countably many radii.

Yes, I thought about separability as well, and came to the same conclusion. (It's not enough in my application to have this fail for countably many radii!...) You're obviously much better at google than I am! I don't know why I didn't find these when I searched. (Like an idiot, I went to textbooks...)

[Arend Mellendijk]

Anatole Dedecker said:

I think it can work only with a condition on the action (and the chosen x, but you could also require it for all x) which seems quite natural to me: for all g, h, the set of ys which are the same distance from g • x and h • x has empty interior

One worrying thing: this condition doesn't automatically hold on normed vector spaces.
Consider $\mathbb{R}^2$ with the $L^1$ norm. All points with $x>1$ and $y<0$ are the same distance from both $(0,0)$ and $(1,1)$

[Anatole Dedecker]

Oh indeed!

[Anatole Dedecker]

But wait there's a problem then

[Anatole Dedecker]

Because that's also a counterexample to @Alex Kontorovich's theorem, even though the space is extendable!

[Anatole Dedecker]

Namely if you consider the action of $\mathbb{Z}$ on $\mathbb{R}^2$ with the $L^1$ norm by diagonal translation (so the action of $1$ is translation by $(1, 1)$)

[Jireh Loreaux]

@Anatole Dedecker, can you specify exactly which theorem please?

[Anatole Dedecker]

Then I think that if you take the intersection of the Dirichlet polyhedron at $(0, 0)$ and its image under the action of $1$, you get a set with nonempty interior

[Anatole Dedecker]

Alex Kontorovich said:

The issue comes with pairwise disjointedness:

theorem IsDisjoint_of_DirichletPolyhedron (x : α) (hx : ∀ g : G, g • x ≠ x) : ∀ (g₁ g₂ : G),
    g₁ ≠ g₂ →
    Disjoint (interior (g₁ • DirichletPolyhedron G x)) (interior (g₂ • DirichletPolyhedron G x))
    :=

This one (in an extendable metric space)

[Anatole Dedecker]

Alex Kontorovich said:

For IsDisjoint_of_DirichletPolyhedron, the argument I have in mind is of course that

def DirichletSet₀ (x : α) (g : G) : Set α := { y : α | dist x y < dist (g • x) y }

lemma interior_DirichletSet (x : α) (g : G) :
    interior (DirichletSet G x g) = DirichletSet₀ G x g := ...?

But what are some "natural" conditions under which this is true?? That's the use case...

In other words, I don't think this is enough to get the wanted result

[Anatole Dedecker]

I may be missing something obvious

[Alex Kontorovich]

Yeah, argh. I should really stop futzing around and do this properly. Luckily, it looks like Misha Kapovich has just recently done exactly that for me! https://arxiv.org/abs/2301.05325 (See Prop 24. May not be so impossible, as we already have things like Lemma 9: t2Space_of_properlyDiscontinuousSMul_of_t2Space...)

[Anatole Dedecker]

Indeed that looks like a nice reference. This is also an interesting point for me to mention that, now that we have docs#IsProperMap (which corresponds to "Bourbaki-proper" in that paper), I will at some point develop the full theory of proper group actions and redefine docs#ProperlyDiscontinuousSMul in terms of it. I have some things I want to discuss about the implementation, but that'll wait for a bit.