Rotation ≠ Reflection

Stream: new members

[Shadman Sakib]

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]

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]

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]

Shadman Sakib has marked this topic as resolved.

[Notification Bot]

Shadman Sakib has marked this topic as unresolved.

[Eric Rodriguez]

  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]

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

[Eric Rodriguez]

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]

@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]

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