# Zulip Chat Archive

## Stream: new members

### Topic: floor vs sum ite

#### Alex Kontorovich (Feb 03 2022 at 15:35):

Help with this please?

```
example (x : ℝ) (d : ℕ) (h : d ∈ finset.Icc 1 ⌊x⌋₊):
∑ n in finset.Icc 1 ⌊x⌋₊, (ite (d ∣ n) 1 0) = ⌊(x / d)⌋₊ :=
begin
sorry
end
```

That is, the number of multiples of `d`

up to `x`

(assuming `d≤x`

) is the floor of `x/d`

...? Thank you!

#### Alex Kontorovich (Feb 03 2022 at 15:40):

(The assumption `d≤x`

isn't necessary, as then both sides are zero... But in case it helps...)

#### Ruben Van de Velde (Feb 03 2022 at 15:45):

What's the maths proof?

#### Alex Kontorovich (Feb 03 2022 at 15:47):

Well, that's the problem I'm having. The math proof is "obvious"... How many multiples of `d`

are there up to `x`

? Well, it's just `x/d`

... But Lean won't accept "duh" as a proof. Do I need to set up a bijection between the integers less than `x/d`

and multiples of `d`

up to `x`

or some god-awful nonsense like that? Or is there a slicker way?

#### Alex J. Best (Feb 03 2022 at 15:53):

What are the imports/open_locales?

#### Ruben Van de Velde (Feb 03 2022 at 15:53):

I'd probably try to reduce it to a statement that doesn't include reals - does that work?

#### Alex Kontorovich (Feb 03 2022 at 15:54):

This is surely overkill, but here's the full list:

```
import analysis.special_functions.integrals
import analysis.special_functions.pow
import number_theory.arithmetic_function
import measure_theory.function.floor
import measure_theory.integral.integral_eq_improper
import number_theory.divisors
noncomputable theory
open_locale big_operators nnreal filter topological_space arithmetic_function
open filter asymptotics real set
```

#### Alex Kontorovich (Feb 03 2022 at 15:55):

Sure, make `x`

a natural; can you get it to work then?

#### Eric Rodriguez (Feb 03 2022 at 15:57):

I think this is nearly there:

```
import data.real.basic
import algebra.big_operators.intervals
open_locale big_operators
lemma my_lemma {d n : ℕ} : (finset.filter (has_dvd.dvd d) (finset.Icc 1 n)).card = n / d :=
begin
induction n with k hk,
{ simp },
have : finset.Icc 1 k.succ = finset.Icc 1 k ∪ {k.succ},
{ ext, simp, sorry },
rw [this, finset.filter_union, finset.filter_singleton],
by_cases h : d ∣ k.succ,
{ sorry },
{ simp [h, hk], sorry },
end
example (x : ℝ) (d : ℕ) (h : d ∈ finset.Icc 1 ⌊x⌋₊):
∑ n in finset.Icc 1 ⌊x⌋₊, (ite (d ∣ n) 1 0) = ⌊x⌋₊ / d :=
begin
rw finset.sum_ite,
simp,
exact my_lemma
end
```

there's some lemmas about `nat.div`

and division and `succ`

that need to be added, but apart from that I think it should work...

#### Eric Rodriguez (Feb 03 2022 at 15:58):

(precisely that `n + 1 / k = n / k + ite (k | n + 1) 1 0`

)

#### Eric Rodriguez (Feb 03 2022 at 15:58):

I'm also not sure if your original floor that you wrote is right, but probably it is

#### Alex Kontorovich (Feb 03 2022 at 16:02):

Great, thanks! I'll try to get that to work...

#### Eric Rodriguez (Feb 03 2022 at 16:04):

ahh, I was looking in the wrong order - the lemma you'll want is `nat.succ_div`

#### Alex Kontorovich (Feb 03 2022 at 16:06):

You don't need the floor function in `my_lemma`

? Is `n/d`

defined to be the floor or something? Good to know...

#### Eric Rodriguez (Feb 03 2022 at 16:08):

ℕ-division is truncating division, yea

Last updated: Dec 20 2023 at 11:08 UTC