## Stream: new members

### Topic: sqrt(3^2) = 3

#### Lars Ericson (Jan 05 2021 at 04:58):

I am trying to prove that the square root of 3^2 is 3. I am trying to introduce some facts:

lemma three_sqrt_squared_equals_three : (((3:ℝ) ^ 2) ^ (1/2: ℝ )) = (3: ℝ)  :=
begin
have h1 := zero_le 3,                --OK
have h2 := real.sqrt_sqr h1, -- ERROR
end


The second fact gives an error:

type mismatch at application
real.sqrt_sqr h1
term
h1
has type
0 ≤ 3
but is expected to have type
0 ≤ ?m_1
state:
h1 : 0 ≤ 3
⊢ (3 ^ 2) ^ (1 / 2) = 3


I need a lifeline.

#### Alex J. Best (Jan 05 2021 at 05:00):

zero_le 3 refers to the natural number 3, you probably want  have h1 := zero_le (3: ℝ),

#### Lars Ericson (Jan 05 2021 at 05:06):

Alas this

import data.real.basic
import analysis.special_functions.pow

lemma three_sqrt_squared_equals_three : (((3:ℝ) ^ 2) ^ (1/2: ℝ )) = (3: ℝ)  :=
begin
have h1 := zero_le (3:ℝ),
end


gives me a different error:

failed to synthesize type class instance for
state:
⊢ (3 ^ 2) ^ (1 / 2) = 3


#### Alex J. Best (Jan 05 2021 at 05:07):

Right, the real number 3 isn't automatically greater or equal to zero (unlike the natural number 3, where every natural number is nonnegative), so you need to prove it.
maybe have h1 : 0\le 3 := by norm_num does what you want

#### Lars Ericson (Jan 05 2021 at 05:35):

That resolves that issue but then the problem expands. I need a definitional equality for square root. This leads to deterministic timeout. If I say sorry for that, then I get almost there, but I get a error message at the end regarding the mix of types. The final goal state of

h3 : (3 ^ 2) ^ (1 / 2) = 3
⊢ (3 ^ 2) ^ (1 / 2) = 3


does not give a clear indication that there is a type mismatch between h3 and goal in :

import data.real.basic
import analysis.special_functions.pow

lemma sqrt_x_equals_sqrt_x (x : ℝ ): real.sqrt x =  x ^ (1 / 2) :=
begin
sorry -- deterministic timeout for library_search! and suggest
end

lemma three_sqrt_squared_equals_three : (((3:ℝ) ^ 2) ^ (1/2: ℝ )) = (3: ℝ)  :=
begin
have h1 : 0 ≤ (3:ℝ), by norm_num,
have h2 := real.sqrt_sqr h1,
have h3 := sqrt_x_equals_sqrt_x ((3:ℝ)^2),
rw h2 at h3,
rw eq_comm at h3,
exact h3,
end


The error message at exact h3 is:

invalid type ascription, term has type
@eq real
(@has_pow.pow real nat (@monoid.has_pow real real.monoid)
(@has_pow.pow real nat (@monoid.has_pow real real.monoid) 3 2)
(@has_div.div nat nat.has_div 1 2))
3
but is expected to have type
@eq real
(@has_pow.pow real real real.has_pow (@has_pow.pow real nat (@monoid.has_pow real real.monoid) 3 2)
(@has_div.div real (@div_inv_monoid.to_has_div real (@division_ring.to_div_inv_monoid real real.division_ring)) 1
2))
3
state:
h1 : 0 ≤ 3,
h2 : real.sqrt (3 ^ 2) = 3,
h3 : (3 ^ 2) ^ (1 / 2) = 3
⊢ (3 ^ 2) ^ (1 / 2) = 3


#### Alex J. Best (Jan 05 2021 at 05:39):

Once again one of the problems here is the types of things not being what you think they are, you should get into the habit of using the widgets like in this gif Patrick made
Patrick Massot said:

nat_vs_int.gif

to check the types are what you expect.

In your first lemma, 1/2 is the natural number floor division 1/2 which is in fact 0. So the lemma isn't true

#### Alex J. Best (Jan 05 2021 at 05:44):

The version first lemma you really want is in mathlib as docs#real.sqrt_eq_rpow btw

#### Lars Ericson (Jan 05 2021 at 14:54):

Just out of curiosity, given that there is a spot-on theorem for this, why is library search timing out?

import data.real.basic
import analysis.special_functions.pow

lemma sqrt_x_equals_sqrt_x (x : ℝ ): real.sqrt x =  x ^ ((1:ℝ )/ (2: ℝ) ) :=
begin
--rw real.sqrt_eq_rpow,
library_search!
end


#### Alex J. Best (Jan 05 2021 at 14:56):

The theorem in the library is an equality of functions, whereas your statement is about the functions applied to some specific x

Last updated: May 14 2021 at 07:19 UTC