Real number is an integer

Stream: new members

[Gareth Ma]

Hi. How should I express that a real number is an integer, in the sense that there exists an integer that casts to it? I wrote it as it is right now ∃ N : ℕ, ↑N = r, but I was wondering if there were better ways.

[Gareth Ma]

In particular, if I want to prove this statement for some r, then I will have to construct N, but sometimes I cannot

[Johan Commelin]

@Gareth Ma I think this is the best way. If you don't want to construct an N what other method would you like to use instead? (You can give an informal mathematical answer, no Lean code required.)

[Gareth Ma]

Here is my actual use case:

lemma aux_exp_mul_int {n : ℕ} :
∃ N : ℕ, ↑N = (Icc 1 (2 * n + 1)).lcm (coe : ℕ → ℝ) * (∫ x : ℝ in 0..1, x ^ n * (1 - x) ^ n) :=
begin

end

I don't know how to provide a more minimal example to demonstrate the complexity. The idea is that the term x ^ n * (1 - x) ^ n is a polynomial in x with degree 2n, so after integrating and evaluating at 1, it is a rational number where the denominator dives lcm(1, ..., 2n + 1), or more specifically sum of fractions with denominators <= (2n + 1). and hence the whole thing is an integer.

[Johan Commelin]

I think you should first simplify away that integral.

[Johan Commelin]

After that, you will still have a polynomial expression. But you will be able to show that it is equal to polynomial.eval of an explicit polynomial with rational coefficients.

[Johan Commelin]

After more simplifications, you'll get to a point where you can actually plug in the N.

[Gareth Ma]

That sounds scary but I will try that!

[Gareth Ma]

So essentially "just do it explicitly"

[Johan Commelin]

We currently don't have tactic support for these calculations, unfortunately.

[Johan Commelin]

But do we already have the theory to simplify that integral?

[Gareth Ma]

We essentially want something like this:

lemma eval_integral_thing_idk {N : ℕ} {a : ℕ → ℝ} :
∫ x : ℝ in 0..1, ∑ n in range N, (a n) * x ^ n = ∑ n in range (N + 1), a n / ↑(n + 1) :=
begin

end

Which seems quite easy?

[Gareth Ma]

binomial theorem exists in add_pow

[Gareth Ma]

lemma eval_integral_thing_idk {N : ℕ} {a : ℕ → ℝ} :
∫ x : ℝ in 0..1, ∑ n in range N, (a n) * x ^ n = ∑ n in range N, a n / ↑(n + 1) :=
begin
  rw interval_integral.integral_finset_sum,
  -- swap signs since it's finite sum
  simp_rw [integral_const_mul, nat.cast_add, algebra_map.coe_one, integral_pow, one_pow,
           zero_pow (nat.zero_lt_succ _), sub_zero, mul_div, mul_one],
  -- prove integrable
  { intros k hk,
    simp only [interval_integral.interval_integrable.const_mul, interval_integrable_pow], },
end