## Stream: new members

### Topic: Rotation ≠ Reflection

#### Shadman Sakib (Jul 16 2021 at 22:19):

I'm working on a lemma that shows a rotation by $\theta$ is never the same as a reflection about the x-axis. Simplified to an equation, I am trying to prove $e^{i\theta}*z ≠ \bar{z}$. I found an example of z for which this equation is not true, but I am having trouble finishing the proof.

#### Shadman Sakib (Jul 16 2021 at 22:20):

import analysis.complex.isometry
import analysis.special_functions.trigonometric

noncomputable theory

open complex

local notation π := real.pi

lemma reflection_rotation : ∀ θ, ∃ z, rotation (exp_map_circle θ) z ≠ conj_lie z :=
begin
intro θ,
simp,
use exp(I * (- (θ/2) + 2)),
rw ← exp_conj,
rw conj.map_mul,
simp,
rw conj.map_div,
simp,
have : ↑θ * I + I * -(↑θ/2) = I * (θ/2),
{ ring, },
rw this,
simp,
rw exp_eq_exp_iff_exists_int,
sorry,
end


#### Shadman Sakib (Jul 16 2021 at 22:21):

How can I show that there is, in fact, not an $n \in \Z$ that satisfies the equation or that the equation before I rewrite exp_eq_exp_iff_exists_int is, in fact, false?

#### Notification Bot (Jul 16 2021 at 22:45):

Shadman Sakib has marked this topic as resolved.

#### Notification Bot (Jul 16 2021 at 22:46):

Shadman Sakib has marked this topic as unresolved.

#### Eric Rodriguez (Jul 16 2021 at 23:23):

  push_neg,
ring,
intros n h,
replace h := add_left_cancel (mul_right_cancel' I_ne_zero h),


will get you closer to your goal. a word of advice, though, usingsimp every line is slow + bad style (what if someone adds a new simp lemma? then it could break your whole proof). try use squeeze_simp if simp doesn't finish your goal and replace the simp with the simp only it suggests

#### Eric Rodriguez (Jul 16 2021 at 23:24):

you can also group rws using the syntax rw [add_comm, exp_eq_exp_iff_exists_int] (for example)

#### Eric Rodriguez (Jul 16 2021 at 23:25):

it'd be interesting, but not sure if possible in mathlib, to prove this via complex diffability; the lhs is complex diffable whilst the rhs isn't

#### Kyle Miller (Jul 16 2021 at 23:37):

@Shadman Sakib Sometimes it pays to generalize a lemma to prove a more specialized one:

import analysis.complex.isometry

noncomputable theory

open complex

lemma reflection_rotation' (w : ℂ) : ∃ z, ¬ w * z = conj z :=
begin
by_cases hu : w.re = -1,
{ use 1,
simp only [mul_one, ring_hom.map_one],
rintro rfl,
rw one_re at hu,
linarith, },
{ use I,
nth_rewrite 1 ←one_mul I,
rw [←right_distrib, mul_eq_zero],
simp only [I_ne_zero, or_false],
rw ←add_left_inj (-1 : ℂ),
rintro rfl,
simpa using hu, }
end

lemma reflection_rotation (θ : ℝ) : ∃ z, rotation (exp_map_circle θ) z ≠ conj_lie z :=
begin
simp only [rotation_apply, ne.def, conj_lie_apply],
exact reflection_rotation' (exp_map_circle θ),
end


#### Kyle Miller (Jul 16 2021 at 23:39):

(I'm sure those with more facility than me with complex numbers and algebraic expressions could simplify the proof of the supporting lemma.)

Last updated: Dec 20 2023 at 11:08 UTC