## Stream: new members

### Topic: Real number is an integer

#### Gareth Ma (Feb 07 2023 at 05:34):

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 (Feb 07 2023 at 05:36):

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 (Feb 07 2023 at 06:44):

@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 (Feb 07 2023 at 06:46):

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 (Feb 07 2023 at 06:49):

I think you should first simplify away that integral.

#### Johan Commelin (Feb 07 2023 at 06:49):

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 (Feb 07 2023 at 06:51):

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

#### Gareth Ma (Feb 07 2023 at 06:51):

That sounds scary but I will try that!

#### Gareth Ma (Feb 07 2023 at 06:52):

So essentially "just do it explicitly"

#### Johan Commelin (Feb 07 2023 at 06:52):

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

#### Johan Commelin (Feb 07 2023 at 06:54):

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

#### Gareth Ma (Feb 07 2023 at 07:03):

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 (Feb 07 2023 at 07:03):

binomial theorem exists in add_pow

#### Gareth Ma (Feb 07 2023 at 07:12):

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


Last updated: Dec 20 2023 at 11:08 UTC