Nonnegative doubling factor

Stream: Carleson

[Edward van de Meent]

would it be acceptable to assume the doubling factor A to be nonnegative by definition (has type NNReal rather than Real)? This is provably true for nonempty X, but having it as a type leads to some nicer api

[Edward van de Meent]

this is also the approach in IsUnifLocDoublingMeasure, which is in Mathlib

[Floris van Doorn]

@Edward van de Meent Ah, oops. I thought it followed automatically, but of course I forgot about the empty X.

I prefer not to change the type of A to NNReal, and for this project I'm definitely happy to assume Nonempty X. The way DoublingMeasure is stated currently, it will not go into Mathlib anyway, so maybe we should just have it extend Nonempty X as well?

[Edward van de Meent]

is there a reason why you'd rather not change the type?

[Floris van Doorn]

The statement makes perfect sense for all real numbers A, and if you have a real number, it's annoying that you cannot state something without proving that the number is nonnegative.

[Floris van Doorn]

In the same way, I find it annoying that docs#HolderWith doesn't use real numbers.

[Edward van de Meent]

i see... then how about we add a constructor for the class where we allow the number to be any real, giving the corresponding instance for NNReal?

[Yaël Dillies]

... or docs#LipschitzWith ?

[Floris van Doorn]

Not sure what you mean Edward... I'm not talking about constructing an instance, but stating that it holds.

[Edward van de Meent]

my point is that for any real A, there is an instance of the class with a nonnegative A.

[Edward van de Meent]

and you can add api saying that indeed the instance you get is the one you want if you have Nonempty X

[Floris van Doorn]

And then we can state it as DoublingMeasure X (Real.toNNReal A)?
Alternative proposal: we keep the definition as is, but change all lemmas that require nonnegativity have an argument in NNReal? Or maybe [Fact (0 ≤ A)]?

[Edward van de Meent]

the reason i prefer working with NNReal in this case is that in my experience, the api for working with ENNReal works better with NNReal than with Real.

[Floris van Doorn]

That is true... When casting to ENNReal it's much nicer to have NNReal...

[Floris van Doorn]

We can try to switch.

[Notification Bot]

13 messages were moved here from #Carleson > Outstanding Tasks, V1 by Floris van Doorn.