# Zulip Chat Archive

## Stream: new members

### Topic: About measures

#### Lucas Viana (Jun 07 2020 at 02:20):

Thanks!

#### Lucas Viana (Jun 07 2020 at 02:22):

(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

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

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
```

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

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