Zulip Chat Archive

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 eiθzzˉ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,
  rw  exp_add,
  rw mul_add,
  rw  add_assoc,
  have : θ * I + I * -(θ/2) = I * (θ/2),
  { ring, },
  rw this,
  simp,
  rw add_comm,
  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 nZn \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,
    rw [conj_I, add_left_inj I, neg_add_self],
    nth_rewrite 1 one_mul I,
    rw [right_distrib, mul_eq_zero],
    simp only [I_ne_zero, or_false],
    rw add_left_inj (-1 : ),
    simp only [add_neg_cancel_right, zero_add],
    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