## Stream: general

### Topic: can you take cos of both sides?

#### James Arthur (Jul 15 2020 at 09:32):

Hi, I have a proof where I am trying to show that you can divide a version of generalised tangent and it's the same as tangent as $tan_m x = \frac{sin_m x}{cos_m x} = \frac{sin x * f(x)}{cos x * f(x)}$, where $f(x)$ is my radius function. I have got the following code thus far:

import tactic
import basic
import data.real.basic
import data.complex.exponential
import analysis.special_functions.pow

noncomputable theory
open_locale classical

open real

notation |x| := abs x

/- 002 -/
def radius (x m : ℝ) := 1 / ( |sin x| ^ m + |cos x| ^ m ) ^ (1/m)

/- 003 -/
def sinm (θ m : ℝ) := sin θ * radius θ m
-- trigonometric sin is defined!!

/- 004 -/
def cosm (θ m : ℝ) := cos θ * radius θ m
-- So we can onto prove somethings!
-- actually, let us go and define a few more things

/- 005 -/
def tanm (θ m : ℝ) := sinm θ m / cosm θ m

theorem tanm_eq_tan (x m : ℝ) (n : ℤ) (f : radius x m ≠ 0): tanm x m = tan x :=
begin
unfold tanm,
unfold sinm,
unfold cosm,
have H : cos x * radius x m ≠ 0,
{simp only [ne.def, mul_eq_zero],
intros h,
cases h with m n,
swap,
{apply f, exact n,},
{ by_cases h : ∃ n, x = (2*n+1)/2 * pi,
{sorry},
{ rw not_exists at h,
apply h n,
-- bit stuck here, want to just 'cos' both sides
sorry
},
},
}
end


I have also proved this auxillary lemma but it doesn't seem to be much use:

lemma exists_cos_pi_half_eq_zero (x m : ℝ) (n : ℤ) : ∃ n, x = (2*n + 1) * pi / 2 → cos x = 0  :=
begin
use 0,
intros f,
rw [mul_zero, zero_add, one_mul] at f,
rw f,
simp,
end


#### Chris Hughes (Jul 15 2020 at 09:40):

There's the apply_fun tactic.

#### Johan Commelin (Jul 15 2020 at 09:40):

@James Arthur But sides of the goal, or both sides of a hypothesis?

#### Johan Commelin (Jul 15 2020 at 09:40):

(I didn't try your code yet.)

#### James Arthur (Jul 15 2020 at 09:41):

both sides of the goal

#### Chris Hughes (Jul 15 2020 at 09:41):

cosm needs to be injective for that right?

#### James Arthur (Jul 15 2020 at 09:41):

current state of the goal:

1 goal
x m: ℝ
n: ℤ
f: radius x m ≠ 0
m: cos x = 0
h: ∀ (x_1 : ℝ), ¬x = (2 * x_1 + 1) / 2 * pi
⊢ x = (2 * ↑n + 1) / 2 * pi


#### Chris Hughes (Jul 15 2020 at 09:42):

Is it injective on some interval and you know both sides of the goal are in that interval?

#### Sebastien Gouezel (Jul 15 2020 at 09:44):

Wait, your assumption h is wrong, right? (take $x_1 = (2 \pi x -1)/2$). From this, you can deduce anything you want!

#### James Arthur (Jul 15 2020 at 09:44):

I believe that $cos x$ isn't injective than on 0 to $\frac{\pi}{2}$ and I haven't actually looked at $cosm x$ but my intuition says no. I removed the problemed areas in this case, i.e. where cosm goes to infinity

#### James Arthur (Jul 15 2020 at 09:45):

Sebastien Gouezel said:

Wait, your assumption h is wrong, right? (take $x_1 = (2 \pi x -1)/2$). From this, you can deduce anything you want!

Oh... yeah. it needs to be an integer XD

#### Shing Tak Lam (Jul 15 2020 at 09:46):

This was what I was alluding to yesterday. I didn't see your code for very long and the \exists ... may not have been the correct idea.

theorem tanm_eq_tan (x m : ℝ) (f : radius x m ≠ 0): tanm x m = tan x :=
begin
unfold tanm sinm cosm,
rw tan_eq_sin_div_cos,
by_cases h : cos x = 0,
{ rw h, simp },
rw div_eq_div_iff,
ring,
exact mul_ne_zero h f,
exact h,
end


#### Shing Tak Lam (Jul 15 2020 at 09:46):

Since dividing by 0 in Lean gives you 0, so it's true whether cos x is 0 or not

#### Shing Tak Lam (Jul 15 2020 at 09:47):

Apologies for (maybe) leading you down a wrong path

#### James Arthur (Jul 15 2020 at 09:47):

It's ok. I was following your message. To be perfectly honest I had no idea where I was going

#### James Arthur (Jul 15 2020 at 10:09):

Also thankyou all!

Last updated: Aug 03 2023 at 10:10 UTC