## Stream: new members

Thanks!

(deleted)

#### Lucas Viana (Jun 07 2020 at 03:23):

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 (Jun 07 2020 at 03:50):

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 (Jun 07 2020 at 04:03):

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 (Jun 07 2020 at 04:04):

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 (Jun 07 2020 at 04:08):

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 (Jun 07 2020 at 04:09):

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 (Jun 07 2020 at 04:10):

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 (Jun 07 2020 at 04:10):

*fract

#### Sam Lichtenstein (Jun 07 2020 at 04:10):

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

#### Mario Carneiro (Jun 07 2020 at 04:11):

Haar measure isn't unique though

#### Mario Carneiro (Jun 07 2020 at 04:11):

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

#### Mario Carneiro (Jun 07 2020 at 04:12):

But I don't think mathlib has Haar measure yet

#### Sam Lichtenstein (Jun 07 2020 at 04:12):

i just checked and didn’t see it

#### Lucas Viana (Jun 07 2020 at 04:12):

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

#### Mario Carneiro (Jun 07 2020 at 04:13):

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

#### Mario Carneiro (Jun 07 2020 at 04:13):

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

#### Mario Carneiro (Jun 07 2020 at 04:14):

fract is defined over any floor_ring

#### Mario Carneiro (Jun 07 2020 at 04:15):

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

#### Lucas Viana (Jun 07 2020 at 04:17):

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 (Jun 07 2020 at 04:18):

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

#### Mario Carneiro (Jun 07 2020 at 04:19):

Oh, it's using euclidean_domain.has_mod

#### Mario Carneiro (Jun 07 2020 at 04:19):

hm, that will complicate things

#### Mario Carneiro (Jun 07 2020 at 04:21):

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 (Jun 07 2020 at 04:22):

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


#### Lucas Viana (Jun 07 2020 at 04:24):

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 (Jun 07 2020 at 04:25):

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

#### Mario Carneiro (Jun 07 2020 at 04:26):

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 (Jun 07 2020 at 04:26):

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

and 3 % 2 = 1

#### Mario Carneiro (Jun 07 2020 at 04:27):

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

#### Lucas Viana (Jun 07 2020 at 04:27):

Hm, this makes sense

#### Mario Carneiro (Jun 07 2020 at 04:28):

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


Thanks!

#### Mario Carneiro (Jun 07 2020 at 04:28):

#check (3.4 % 2 : ℝ)


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

#### Mario Carneiro (Jun 07 2020 at 04:29):

but it is provably zero as shown above

#### Mario Carneiro (Jun 07 2020 at 04:30):

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

Last updated: Dec 20 2023 at 11:08 UTC