definition of doubling measures

Stream: maths

[Jireh Loreaux]

@Oliver Nash: docs#is_doubling_measure requires the doubling property to hold only for balls of sufficiently small radius. The docstring gives an explanation for the reason (i.e., we want the volume measure in hyperbolic space to be doubling), but this stands in contrast to the standard literature. I can understand the desire to encompass as many things as possilbe with a single type class, but are we sure this isn't a bad idea? That is, do the standard results like Assouad's snowflaking embedding theorem obviously (or even non-obviously) still hold?

[Oliver Nash]

I think the class as it stands is a good definition: it is sufficient to prove useful theorems (like Lebesgue's density theorem) but general enough to apply quite broadly. However you're suggesting perhaps the name isn't right?

[Oliver Nash]

I.e., IIUC you're saying that there is a common usage of the term "doubling measure" which is more restrictive? And presumably results that only hold with this stronger meaning of "doubling measure"?

[Jireh Loreaux]

Well, I've certainly only ever seen doubling measure mean μ (ball x (2 * r)) ≤ C * μ (ball x r) for all r. I wouldn't be surprised if things "at infinity" mattered as well, which is essentially the subject of coarse geometry.

[Oliver Nash]

I see. Well we can always rename this class to have some prefix like locally_ or pre_ or eventually_. I don't claim more than a passing familiarity with this sort of thing. I'll take a look now to see if I can find any references to help decide on the name (I wouldn't be all that surprised if the informal literature is not consistent).

[Oliver Nash]

Oh dear, first three web links support your terminology. I'd better keep digging!

[Jireh Loreaux]

I know an expert in this area. Let me ask her the ramifications of requiring the property hold only for sufficiently small radii.

[Oliver Nash]

That would be great, thanks!

[Sebastien Gouezel]

The large scale assumption definitely plays a role in some results. For instance, Assouad's theorem you mentioned can not hold if you only put the assumptions at small scales (a counterexample is the hyperbolic disk).

[Oliver Nash]

@Sebastien Gouezel do you think we should rename our class, e.g., to is_locally_doubling_measure?

[Sebastien Gouezel]

That would definitely make sense, yes. In all the interesting applications I have in mind the space is compact so it doesn't make a difference.

[Jireh Loreaux]

@Sebastien Gouezel can you explain how exactly the hyperbolic disk is a counterexample? It's still not immediately clear to me.

[Sebastien Gouezel]

It's just too big at infinity to fit in any ℝ^N, even in a Hölder way, because the growth rate of balls is exponential while it is only polynomial in ℝ^N.

[Oliver Nash]

I've created #18709 to attempt a rename.

[Jireh Loreaux]

@Oliver Nash the expert I know says that these are called uniformly locally doubling measures. It seems that a locally doubling measure is one where the doubling constant depends on x (the center of the balls involved).

[Oliver Nash]

Is she aware that we have a line length limit of 100 characters!?

[Oliver Nash]

More seriously, thanks very much. This is really useful. I'll adjust the PR!

[Oliver Nash]

Though I think is_uniformly_locally_doubling_measure is too long.

[Oliver Nash]

I'm open to suggestions.

[Yaël Dillies]

is_unif_loc_doubling_measure?

[Oliver Nash]

Sounds good to me.

[Jeremy Tan]

Oliver Nash said:

Is she aware that we have a line length limit of 100 characters!?

Who is that she?

[Yaël Dillies]

We could even go for is_unif_loc_doub_measure if you have no doub that this will be clear.

[Jireh Loreaux]

Jeremy, the expert I know. I'm preserving her anonymity because I haven't asked her if I can use her name publicly (and she's not present on Zulip); it was private correspondence.

[Yaël Dillies]

We shouldn't know who is trying to sabotage our line length.

[Jireh Loreaux]

Oliver (or anyone), if you are feeling bored, you could add the actual definition of doubling measure, show that it trivially has an instance for is_unif_loc_doubling_measure, and then go strengthen all the applicable instances. If no one else does it, I might do it this weekend.

[Oliver Nash]

I'm scrambling to have any time at all for Lean at the moment so I don't think I'll get to this but I agree it is worth doing.