## Stream: new members

### Topic: floor vs sum ite

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

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