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