About measures

Stream: new members

[Lucas Viana]

Thanks!

[Lucas Viana]

(deleted)

[Lucas Viana]

I am now stuck defining a measure on R/Z1 identified with the unit interval. Like, I can use quot to define the type and have my real functions lifted to the interval, but how can I then use the identification to "lift" the lebesgue measure to it (pushforward measure)?

[Lucas Viana]

So I thought I had defined the equivalence relation with % as mod, but it turns out it just outputs the mod of the floor of the real number. Is there a proper mod function for real numbers?

[Pedro Minicz]

The first thing I looked for was also mod for reals. Couldn't find it on mathlib and I believe its not defined anywhere.

[Pedro Minicz]

I think you may have seen it on my thread, but I settled for a ~ b defined as b - a ∈ ℤ, which should work nice (caution: unverified assertion).

[Mario Carneiro]

Couldn't you take the preimage of the set under the quotient map (resulting in a periodic subset of R), and then intersect with [0, 1] and read off the measure that way?

[Mario Carneiro]

Is this an instance of a general construction? It's not obvious to me how to do this in general because the preimage alone doesn't cut it

[Mario Carneiro]

While mod may not be defined on real, I think there is a frac function (which returns the fractional part of a real number) IIRC

[Mario Carneiro]

*fract

[Sam Lichtenstein]

Haar measure for quotient of locally compact top groups by nice subgroups?

[Mario Carneiro]

Haar measure isn't unique though

[Mario Carneiro]

at the very least it would have to have a reference subset as input

[Mario Carneiro]

But I don't think mathlib has Haar measure yet

[Sam Lichtenstein]

i just checked and didn’t see it

[Lucas Viana]

If it has fract it should be easy to define x % k as k * fract (x / k), no?

[Mario Carneiro]

There is nothing fundamental blocking mod from being defined, I think we just didn't need it for anything

[Mario Carneiro]

although it is worth thinking about in what generality to state it

[Mario Carneiro]

fract is defined over any floor_ring

[Mario Carneiro]

(I still don't see a reason for it from this conversation though)

[Lucas Viana]

Maybe it is not necessary, but I found it confusing that % in the reals returns integers (it took me a while before I realized what it was doing)

[Mario Carneiro]

That sounds odd to me as well, I'm not sure what coercions made that happen

[Mario Carneiro]

Oh, it's using euclidean_domain.has_mod

[Mario Carneiro]

hm, that will complicate things

[Mario Carneiro]

wait no, the definition of remainder in a field is λ a b, a - a * b / b which should be 0 in all reasonable cases

[Mario Carneiro]

example (x y : ℝ) (h : y ≠ 0) : x % y = 0 :=
show x - _ = 0, by simp [h]

[Lucas Viana]

But if y is a Int does this holds? I am away from my computer now, but I remember #eval 3.4 % 2 would return 1

[Mario Carneiro]

You didn't provide any type there, so it probably defaults to nat

[Mario Carneiro]

set_option pp.implicit true
set_option pp.notation false
#check 3.4 % 2
-- @has_mod.mod nat nat.has_mod (@has_div.div nat nat.has_div 17 5) 2 : nat

[Mario Carneiro]

3.4 is being interpreted as 17 / 5 : nat which is floored division resulting in 3

[Mario Carneiro]

and 3 % 2 = 1

[Mario Carneiro]

If y is an int then it will infer that everything is an int and you will still get 1

[Lucas Viana]

Hm, this makes sense

[Mario Carneiro]

set_option pp.implicit true
set_option pp.notation false
#check 3.4 % (2 : ℤ)
-- @has_mod.mod int int.has_mod (@has_div.div int int.has_div 17 5) 2 : int

[Lucas Viana]

Thanks!

[Mario Carneiro]

#check (3.4 % 2 : ℝ)

works, but you can't eval it because it's a real

[Mario Carneiro]

but it is provably zero as shown above

[Mario Carneiro]

I think euclidean_domain should probably be decoupled from the div and mod notations