floor vs sum ite

Stream: new members

[Alex Kontorovich]

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]

(The assumption d≤x isn't necessary, as then both sides are zero... But in case it helps...)

[Ruben Van de Velde]

What's the maths proof?

[Alex Kontorovich]

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]

What are the imports/open_locales?

[Ruben Van de Velde]

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

[Alex Kontorovich]

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]

Sure, make x a natural; can you get it to work then?

[Eric Rodriguez]

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]

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

[Eric Rodriguez]

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

[Alex Kontorovich]

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

[Eric Rodriguez]

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

[Alex Kontorovich]

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]

ℕ-division is truncating division, yea