Floor division hell in asymptotics

Stream: new members

[Gareth Ma]

(Not surprisingly) I am struggling to prove the following result:

example {b : ℤ} (hb : 2 <= b) :
    ∃ c > 0, |((b / 2 * (b / 2 - 1) / 2) : ℝ) - (b : ℝ) ^ 2 / 8| ≤ c * |(b : ℝ)| / 2 := by
  sorry

Is there any general tips on how to tackle these? In particular, I just want to prove some messy division stuff is $O(\text{highest order term})$, but it's all in floor division :(

[Gareth Ma]

(This basically comes from $\sum_{0 \leq k \leq b} b - k$ or something, so some floor(s / divisions) are unavoidable?)

[Richard Copley]

All of those divisions are ℝ → ℝ → ℝ, fyi

[Mario Carneiro]

you can lower and upper bound floor division wrt regular division, and apply asymptotics on the result

[Gareth Ma]

That's the idea but implementing it still seems hard, can you provide some help? For example I guess a generous estimate would be to lower bound $\frac{b - k}{k} \leq \lfloor\frac{b}{k}\rfloor$, so I want to prove

example {b : ℤ} (hb : 2 ≤ b) :
    ((b : ℚ) - 2) * (b - 2) / 8 - (b - 2) / 4 ≤ ((b / 2) * (b / 2 - 1) / 2 : ℤ) := by
  sorry

I think.

[Mario Carneiro]

does gcongr help?

[Gareth Ma]

Nope 0 progress

[Mario Carneiro]

looks like you did some simplifications on that expression too

[Gareth Ma]

example {b : ℤ} (hb : 2 ≤ b) :
    (((b - 2 : ℚ) / 2) * ((b - 2 : ℚ) / 2 - 1) - 2) / 2 ≤ ((b / 2) * (b / 2 - 1) / 2 : ℤ) := by
  gcongr

I reverted the manual simplifiactions I did, but still 0 progress

[Gareth Ma]

It fails for this too:

example {a b : ℤ} (hb : a ≤ b) :
    ((a : ℚ) - 2) / 2 ≤ (b / 2 : ℤ) := by
  gcongr

So I don't think it can help with floor divisions.

[Mario Carneiro]

it helps with all the stuff which isn't the floor divisions here

[Mario Carneiro]

for the floor division itself you need a lemma

[Gareth Ma]

I will start with

lemma aux_floor_div {a b k : ℤ} (hb : a ≤ b) (hk : 0 < k) :
    ((a : ℚ) - k + 1) / k ≤ (b / k : ℤ) := by
  rw [div_le_iff (by norm_cast), ← add_sub_right_comm, sub_le_iff_le_add]
  norm_cast
  rw [add_one_le_iff]
  apply lt_of_le_of_lt hb
  rw [← add_one_mul, ← Int.ediv_lt_iff_lt_mul hk]
  exact lt_succ _

lemma aux_floor_div' {a b k : ℤ} (hb : a ≤ b) (hk : 0 < k) :
    ((a : ℚ) - k) / k ≤ (b / k : ℤ) := by
  apply le_trans ?_ (aux_floor_div hb hk)
  gcongr
  exact le_add_of_nonneg_right zero_le_one

and "build" the blocks one by one I guess. Thanks!

[Mario Carneiro]

I think your original expression is off, it seems to work except for that

[Gareth Ma]

The very first message? Yes I put the type casting wrong, let me fix it

[Mario Carneiro]

no, the numbers are wrong

[Gareth Ma]

which one?

[Mario Carneiro]

import Mathlib.Tactic.Linarith
import Mathlib.Data.Real.Basic

theorem todo (a b : ℤ) : (a / b - 1 : ℚ) ≤ (a / b : ℤ) := sorry

example {b : ℤ} (hb : 4 ≤ b) :
    ((b : ℚ) - 2) * (b - 4) / 8 - 1 ≤ ((b / 2) * (b / 2 - 1) / 2 : ℤ) := by
  calc  ((b : ℚ) - 2) * (b - 4) / 8 - 1
    _ = ((b / 2 - 1) * ((b / 2 - 1) - 1)) / 2 - 1 := by ring
    _ ≤ ((b / 2 : ℤ) * ((b / 2 : ℤ) - 1)) / 2 - 1 := by
      gcongr
      · linarith [show 4 ≤ (b:ℚ) by exact_mod_cast hb]
      · apply todo
      · apply todo
    _ ≤ ((b / 2) * (b / 2 - 1) : ℤ) / 2 - 1 := by simp
    _ ≤ ((b / 2) * (b / 2 - 1) / 2 : ℤ) := todo ..

[Gareth Ma]

Oh my god lol thanks so much...

[Gareth Ma]

Ohhhhhh wait I had a realisation. I shouldn't be bounding the final term (b/2)*(b/2-1)/2 directly (every / is floor division here)

[Gareth Ma]

The term is obtained from a sum $S_{\lfloor b / 2 \rfloor - 1} = 1 + \cdots + (\lfloor b / 2 \rfloor - 1)$, so I should bound $|S_{\lfloor b / 2 \rfloor - 1} - S_{b / 2 - 1}| = |S_{\lfloor b / 2 \rfloor - 1} - S_{\lfloor b / 2 - 1 \rfloor}|$, which is easier because $S_y - S_x \leq y(y - x)$ for integers $y \geq x$.

[Gareth Ma]

Where $S_a = \sum_{k = 1}^{\lfloor a \rfloor} k$