diff --git a/src/analysis/special_functions/complex/log.lean b/src/analysis/special_functions/complex/log.lean index 66f89c176c6ce..34f328cd867f0 100644 --- a/src/analysis/special_functions/complex/log.lean +++ b/src/analysis/special_functions/complex/log.lean @@ -5,6 +5,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin -/ import analysis.special_functions.complex.arg import analysis.special_functions.log +import analysis.special_functions.trigonometric.inverse_deriv /-! # The complex `log` function diff --git a/src/analysis/special_functions/trigonometric/inverse.lean b/src/analysis/special_functions/trigonometric/inverse.lean index 2059d48a65c76..aa798af6f6c2b 100644 --- a/src/analysis/special_functions/trigonometric/inverse.lean +++ b/src/analysis/special_functions/trigonometric/inverse.lean @@ -3,7 +3,9 @@ Copyright (c) 2018 Chris Hughes. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson -/ -import analysis.special_functions.trigonometric.deriv +import analysis.special_functions.trigonometric.basic +import topology.algebra.ordered.proj_Icc + /-! # Inverse trigonometric functions. @@ -11,7 +13,7 @@ import analysis.special_functions.trigonometric.deriv See also `analysis.special_functions.trigonometric.arctan` for the inverse tan function. (This is delayed as it is easier to set up after developing complex trigonometric functions.) -Basic inequalities and derivatives. +Basic inequalities on trigonometric functions. -/ noncomputable theory @@ -227,112 +229,6 @@ begin rw [this, sin_arcsin hx₁ hx₂], end -lemma deriv_arcsin_aux {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : - has_strict_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x ∧ times_cont_diff_at ℝ ⊤ arcsin x := -begin - cases h₁.lt_or_lt with h₁ h₁, - { have : 1 - x ^ 2 < 0, by nlinarith [h₁], - rw [sqrt_eq_zero'.2 this.le, div_zero], - have : arcsin =ᶠ[𝓝 x] λ _, -(π / 2) := - (gt_mem_nhds h₁).mono (λ y hy, arcsin_of_le_neg_one hy.le), - exact ⟨(has_strict_deriv_at_const _ _).congr_of_eventually_eq this.symm, - times_cont_diff_at_const.congr_of_eventually_eq this⟩ }, - cases h₂.lt_or_lt with h₂ h₂, - { have : 0 < sqrt (1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂]), - simp only [← cos_arcsin h₁.le h₂.le, one_div] at this ⊢, - exact ⟨sin_local_homeomorph.has_strict_deriv_at_symm ⟨h₁, h₂⟩ this.ne' - (has_strict_deriv_at_sin _), - sin_local_homeomorph.times_cont_diff_at_symm_deriv this.ne' ⟨h₁, h₂⟩ - (has_deriv_at_sin _) times_cont_diff_sin.times_cont_diff_at⟩ }, - { have : 1 - x ^ 2 < 0, by nlinarith [h₂], - rw [sqrt_eq_zero'.2 this.le, div_zero], - have : arcsin =ᶠ[𝓝 x] λ _, π / 2 := (lt_mem_nhds h₂).mono (λ y hy, arcsin_of_one_le hy.le), - exact ⟨(has_strict_deriv_at_const _ _).congr_of_eventually_eq this.symm, - times_cont_diff_at_const.congr_of_eventually_eq this⟩ } -end - -lemma has_strict_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : - has_strict_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x := -(deriv_arcsin_aux h₁ h₂).1 - -lemma has_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : - has_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x := -(has_strict_deriv_at_arcsin h₁ h₂).has_deriv_at - -lemma times_cont_diff_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} : - times_cont_diff_at ℝ n arcsin x := -(deriv_arcsin_aux h₁ h₂).2.of_le le_top - -lemma has_deriv_within_at_arcsin_Ici {x : ℝ} (h : x ≠ -1) : - has_deriv_within_at arcsin (1 / sqrt (1 - x ^ 2)) (Ici x) x := -begin - rcases em (x = 1) with (rfl|h'), - { convert (has_deriv_within_at_const _ _ (π / 2)).congr _ _; - simp [arcsin_of_one_le] { contextual := tt } }, - { exact (has_deriv_at_arcsin h h').has_deriv_within_at } -end - -lemma has_deriv_within_at_arcsin_Iic {x : ℝ} (h : x ≠ 1) : - has_deriv_within_at arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x := -begin - rcases em (x = -1) with (rfl|h'), - { convert (has_deriv_within_at_const _ _ (-(π / 2))).congr _ _; - simp [arcsin_of_le_neg_one] { contextual := tt } }, - { exact (has_deriv_at_arcsin h' h).has_deriv_within_at } -end - -lemma differentiable_within_at_arcsin_Ici {x : ℝ} : - differentiable_within_at ℝ arcsin (Ici x) x ↔ x ≠ -1 := -begin - refine ⟨_, λ h, (has_deriv_within_at_arcsin_Ici h).differentiable_within_at⟩, - rintro h rfl, - have : sin ∘ arcsin =ᶠ[𝓝[Ici (-1:ℝ)] (-1)] id, - { filter_upwards [Icc_mem_nhds_within_Ici ⟨le_rfl, neg_lt_self (@zero_lt_one ℝ _ _)⟩], - exact λ x, sin_arcsin' }, - have := h.has_deriv_within_at.sin.congr_of_eventually_eq this.symm (by simp), - simpa using (unique_diff_on_Ici _ _ left_mem_Ici).eq_deriv _ this (has_deriv_within_at_id _ _) -end - -lemma differentiable_within_at_arcsin_Iic {x : ℝ} : - differentiable_within_at ℝ arcsin (Iic x) x ↔ x ≠ 1 := -begin - refine ⟨λ h, _, λ h, (has_deriv_within_at_arcsin_Iic h).differentiable_within_at⟩, - rw [← neg_neg x, ← image_neg_Ici] at h, - have := (h.comp (-x) differentiable_within_at_id.neg (maps_to_image _ _)).neg, - simpa [(∘), differentiable_within_at_arcsin_Ici] using this -end - -lemma differentiable_at_arcsin {x : ℝ} : - differentiable_at ℝ arcsin x ↔ x ≠ -1 ∧ x ≠ 1 := -⟨λ h, ⟨differentiable_within_at_arcsin_Ici.1 h.differentiable_within_at, - differentiable_within_at_arcsin_Iic.1 h.differentiable_within_at⟩, - λ h, (has_deriv_at_arcsin h.1 h.2).differentiable_at⟩ - -@[simp] lemma deriv_arcsin : deriv arcsin = λ x, 1 / sqrt (1 - x ^ 2) := -begin - funext x, - by_cases h : x ≠ -1 ∧ x ≠ 1, - { exact (has_deriv_at_arcsin h.1 h.2).deriv }, - { rw [deriv_zero_of_not_differentiable_at (mt differentiable_at_arcsin.1 h)], - simp only [not_and_distrib, ne.def, not_not] at h, - rcases h with (rfl|rfl); simp } -end - -lemma differentiable_on_arcsin : differentiable_on ℝ arcsin {-1, 1}ᶜ := -λ x hx, (differentiable_at_arcsin.2 - ⟨λ h, hx (or.inl h), λ h, hx (or.inr h)⟩).differentiable_within_at - -lemma times_cont_diff_on_arcsin {n : with_top ℕ} : - times_cont_diff_on ℝ n arcsin {-1, 1}ᶜ := -λ x hx, (times_cont_diff_at_arcsin (mt or.inl hx) (mt or.inr hx)).times_cont_diff_within_at - -lemma times_cont_diff_at_arcsin_iff {x : ℝ} {n : with_top ℕ} : - times_cont_diff_at ℝ n arcsin x ↔ n = 0 ∨ (x ≠ -1 ∧ x ≠ 1) := -⟨λ h, or_iff_not_imp_left.2 $ λ hn, differentiable_at_arcsin.1 $ h.differentiable_at $ - with_top.one_le_iff_pos.2 (pos_iff_ne_zero.2 hn), - λ h, h.elim (λ hn, hn.symm ▸ (times_cont_diff_zero.2 continuous_arcsin).times_cont_diff_at) $ - λ hx, times_cont_diff_at_arcsin hx.1 hx.2⟩ - /-- Inverse of the `cos` function, returns values in the range `0 ≤ arccos x` and `arccos x ≤ π`. If the argument is not between `-1` and `1` it defaults to `π / 2` -/ @[pp_nodot] noncomputable def arccos (x : ℝ) : ℝ := @@ -388,51 +284,4 @@ by rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin hx₁ hx @[continuity] lemma continuous_arccos : continuous arccos := continuous_const.sub continuous_arcsin -lemma has_strict_deriv_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : - has_strict_deriv_at arccos (-(1 / sqrt (1 - x ^ 2))) x := -(has_strict_deriv_at_arcsin h₁ h₂).const_sub (π / 2) - -lemma has_deriv_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : - has_deriv_at arccos (-(1 / sqrt (1 - x ^ 2))) x := -(has_deriv_at_arcsin h₁ h₂).const_sub (π / 2) - -lemma times_cont_diff_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} : - times_cont_diff_at ℝ n arccos x := -times_cont_diff_at_const.sub (times_cont_diff_at_arcsin h₁ h₂) - -lemma has_deriv_within_at_arccos_Ici {x : ℝ} (h : x ≠ -1) : - has_deriv_within_at arccos (-(1 / sqrt (1 - x ^ 2))) (Ici x) x := -(has_deriv_within_at_arcsin_Ici h).const_sub _ - -lemma has_deriv_within_at_arccos_Iic {x : ℝ} (h : x ≠ 1) : - has_deriv_within_at arccos (-(1 / sqrt (1 - x ^ 2))) (Iic x) x := -(has_deriv_within_at_arcsin_Iic h).const_sub _ - -lemma differentiable_within_at_arccos_Ici {x : ℝ} : - differentiable_within_at ℝ arccos (Ici x) x ↔ x ≠ -1 := -(differentiable_within_at_const_sub_iff _).trans differentiable_within_at_arcsin_Ici - -lemma differentiable_within_at_arccos_Iic {x : ℝ} : - differentiable_within_at ℝ arccos (Iic x) x ↔ x ≠ 1 := -(differentiable_within_at_const_sub_iff _).trans differentiable_within_at_arcsin_Iic - -lemma differentiable_at_arccos {x : ℝ} : - differentiable_at ℝ arccos x ↔ x ≠ -1 ∧ x ≠ 1 := -(differentiable_at_const_sub_iff _).trans differentiable_at_arcsin - -@[simp] lemma deriv_arccos : deriv arccos = λ x, -(1 / sqrt (1 - x ^ 2)) := -funext $ λ x, (deriv_const_sub _).trans $ by simp only [deriv_arcsin] - -lemma differentiable_on_arccos : differentiable_on ℝ arccos {-1, 1}ᶜ := -differentiable_on_arcsin.const_sub _ - -lemma times_cont_diff_on_arccos {n : with_top ℕ} : - times_cont_diff_on ℝ n arccos {-1, 1}ᶜ := -times_cont_diff_on_const.sub times_cont_diff_on_arcsin - -lemma times_cont_diff_at_arccos_iff {x : ℝ} {n : with_top ℕ} : - times_cont_diff_at ℝ n arccos x ↔ n = 0 ∨ (x ≠ -1 ∧ x ≠ 1) := -by refine iff.trans ⟨λ h, _, λ h, _⟩ times_cont_diff_at_arcsin_iff; - simpa [arccos] using (@times_cont_diff_at_const _ _ _ _ _ _ _ _ _ _ (π / 2)).sub h - end real diff --git a/src/analysis/special_functions/trigonometric/inverse_deriv.lean b/src/analysis/special_functions/trigonometric/inverse_deriv.lean new file mode 100644 index 0000000000000..16edc46c73c9e --- /dev/null +++ b/src/analysis/special_functions/trigonometric/inverse_deriv.lean @@ -0,0 +1,184 @@ +/- +Copyright (c) 2018 Chris Hughes. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson +-/ +import analysis.special_functions.trigonometric.inverse +import analysis.special_functions.trigonometric.deriv + +/-! +# derivatives of the inverse trigonometric functions + +Derivatives of `arcsin` and `arccos`. +-/ + +noncomputable theory +open_locale classical topological_space filter +open set filter + +open_locale real + +namespace real + +section arcsin + +lemma deriv_arcsin_aux {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : + has_strict_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x ∧ times_cont_diff_at ℝ ⊤ arcsin x := +begin + cases h₁.lt_or_lt with h₁ h₁, + { have : 1 - x ^ 2 < 0, by nlinarith [h₁], + rw [sqrt_eq_zero'.2 this.le, div_zero], + have : arcsin =ᶠ[𝓝 x] λ _, -(π / 2) := + (gt_mem_nhds h₁).mono (λ y hy, arcsin_of_le_neg_one hy.le), + exact ⟨(has_strict_deriv_at_const _ _).congr_of_eventually_eq this.symm, + times_cont_diff_at_const.congr_of_eventually_eq this⟩ }, + cases h₂.lt_or_lt with h₂ h₂, + { have : 0 < sqrt (1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂]), + simp only [← cos_arcsin h₁.le h₂.le, one_div] at this ⊢, + exact ⟨sin_local_homeomorph.has_strict_deriv_at_symm ⟨h₁, h₂⟩ this.ne' + (has_strict_deriv_at_sin _), + sin_local_homeomorph.times_cont_diff_at_symm_deriv this.ne' ⟨h₁, h₂⟩ + (has_deriv_at_sin _) times_cont_diff_sin.times_cont_diff_at⟩ }, + { have : 1 - x ^ 2 < 0, by nlinarith [h₂], + rw [sqrt_eq_zero'.2 this.le, div_zero], + have : arcsin =ᶠ[𝓝 x] λ _, π / 2 := (lt_mem_nhds h₂).mono (λ y hy, arcsin_of_one_le hy.le), + exact ⟨(has_strict_deriv_at_const _ _).congr_of_eventually_eq this.symm, + times_cont_diff_at_const.congr_of_eventually_eq this⟩ } +end + +lemma has_strict_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : + has_strict_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x := +(deriv_arcsin_aux h₁ h₂).1 + +lemma has_deriv_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : + has_deriv_at arcsin (1 / sqrt (1 - x ^ 2)) x := +(has_strict_deriv_at_arcsin h₁ h₂).has_deriv_at + +lemma times_cont_diff_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} : + times_cont_diff_at ℝ n arcsin x := +(deriv_arcsin_aux h₁ h₂).2.of_le le_top + +lemma has_deriv_within_at_arcsin_Ici {x : ℝ} (h : x ≠ -1) : + has_deriv_within_at arcsin (1 / sqrt (1 - x ^ 2)) (Ici x) x := +begin + rcases em (x = 1) with (rfl|h'), + { convert (has_deriv_within_at_const _ _ (π / 2)).congr _ _; + simp [arcsin_of_one_le] { contextual := tt } }, + { exact (has_deriv_at_arcsin h h').has_deriv_within_at } +end + +lemma has_deriv_within_at_arcsin_Iic {x : ℝ} (h : x ≠ 1) : + has_deriv_within_at arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x := +begin + rcases em (x = -1) with (rfl|h'), + { convert (has_deriv_within_at_const _ _ (-(π / 2))).congr _ _; + simp [arcsin_of_le_neg_one] { contextual := tt } }, + { exact (has_deriv_at_arcsin h' h).has_deriv_within_at } +end + +lemma differentiable_within_at_arcsin_Ici {x : ℝ} : + differentiable_within_at ℝ arcsin (Ici x) x ↔ x ≠ -1 := +begin + refine ⟨_, λ h, (has_deriv_within_at_arcsin_Ici h).differentiable_within_at⟩, + rintro h rfl, + have : sin ∘ arcsin =ᶠ[𝓝[Ici (-1:ℝ)] (-1)] id, + { filter_upwards [Icc_mem_nhds_within_Ici ⟨le_rfl, neg_lt_self (@zero_lt_one ℝ _ _)⟩], + exact λ x, sin_arcsin' }, + have := h.has_deriv_within_at.sin.congr_of_eventually_eq this.symm (by simp), + simpa using (unique_diff_on_Ici _ _ left_mem_Ici).eq_deriv _ this (has_deriv_within_at_id _ _) +end + +lemma differentiable_within_at_arcsin_Iic {x : ℝ} : + differentiable_within_at ℝ arcsin (Iic x) x ↔ x ≠ 1 := +begin + refine ⟨λ h, _, λ h, (has_deriv_within_at_arcsin_Iic h).differentiable_within_at⟩, + rw [← neg_neg x, ← image_neg_Ici] at h, + have := (h.comp (-x) differentiable_within_at_id.neg (maps_to_image _ _)).neg, + simpa [(∘), differentiable_within_at_arcsin_Ici] using this +end + +lemma differentiable_at_arcsin {x : ℝ} : + differentiable_at ℝ arcsin x ↔ x ≠ -1 ∧ x ≠ 1 := +⟨λ h, ⟨differentiable_within_at_arcsin_Ici.1 h.differentiable_within_at, + differentiable_within_at_arcsin_Iic.1 h.differentiable_within_at⟩, + λ h, (has_deriv_at_arcsin h.1 h.2).differentiable_at⟩ + +@[simp] lemma deriv_arcsin : deriv arcsin = λ x, 1 / sqrt (1 - x ^ 2) := +begin + funext x, + by_cases h : x ≠ -1 ∧ x ≠ 1, + { exact (has_deriv_at_arcsin h.1 h.2).deriv }, + { rw [deriv_zero_of_not_differentiable_at (mt differentiable_at_arcsin.1 h)], + simp only [not_and_distrib, ne.def, not_not] at h, + rcases h with (rfl|rfl); simp } +end + +lemma differentiable_on_arcsin : differentiable_on ℝ arcsin {-1, 1}ᶜ := +λ x hx, (differentiable_at_arcsin.2 + ⟨λ h, hx (or.inl h), λ h, hx (or.inr h)⟩).differentiable_within_at + +lemma times_cont_diff_on_arcsin {n : with_top ℕ} : + times_cont_diff_on ℝ n arcsin {-1, 1}ᶜ := +λ x hx, (times_cont_diff_at_arcsin (mt or.inl hx) (mt or.inr hx)).times_cont_diff_within_at + +lemma times_cont_diff_at_arcsin_iff {x : ℝ} {n : with_top ℕ} : + times_cont_diff_at ℝ n arcsin x ↔ n = 0 ∨ (x ≠ -1 ∧ x ≠ 1) := +⟨λ h, or_iff_not_imp_left.2 $ λ hn, differentiable_at_arcsin.1 $ h.differentiable_at $ + with_top.one_le_iff_pos.2 (pos_iff_ne_zero.2 hn), + λ h, h.elim (λ hn, hn.symm ▸ (times_cont_diff_zero.2 continuous_arcsin).times_cont_diff_at) $ + λ hx, times_cont_diff_at_arcsin hx.1 hx.2⟩ + +end arcsin + +section arccos + +lemma has_strict_deriv_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : + has_strict_deriv_at arccos (-(1 / sqrt (1 - x ^ 2))) x := +(has_strict_deriv_at_arcsin h₁ h₂).const_sub (π / 2) + +lemma has_deriv_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : + has_deriv_at arccos (-(1 / sqrt (1 - x ^ 2))) x := +(has_deriv_at_arcsin h₁ h₂).const_sub (π / 2) + +lemma times_cont_diff_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} : + times_cont_diff_at ℝ n arccos x := +times_cont_diff_at_const.sub (times_cont_diff_at_arcsin h₁ h₂) + +lemma has_deriv_within_at_arccos_Ici {x : ℝ} (h : x ≠ -1) : + has_deriv_within_at arccos (-(1 / sqrt (1 - x ^ 2))) (Ici x) x := +(has_deriv_within_at_arcsin_Ici h).const_sub _ + +lemma has_deriv_within_at_arccos_Iic {x : ℝ} (h : x ≠ 1) : + has_deriv_within_at arccos (-(1 / sqrt (1 - x ^ 2))) (Iic x) x := +(has_deriv_within_at_arcsin_Iic h).const_sub _ + +lemma differentiable_within_at_arccos_Ici {x : ℝ} : + differentiable_within_at ℝ arccos (Ici x) x ↔ x ≠ -1 := +(differentiable_within_at_const_sub_iff _).trans differentiable_within_at_arcsin_Ici + +lemma differentiable_within_at_arccos_Iic {x : ℝ} : + differentiable_within_at ℝ arccos (Iic x) x ↔ x ≠ 1 := +(differentiable_within_at_const_sub_iff _).trans differentiable_within_at_arcsin_Iic + +lemma differentiable_at_arccos {x : ℝ} : + differentiable_at ℝ arccos x ↔ x ≠ -1 ∧ x ≠ 1 := +(differentiable_at_const_sub_iff _).trans differentiable_at_arcsin + +@[simp] lemma deriv_arccos : deriv arccos = λ x, -(1 / sqrt (1 - x ^ 2)) := +funext $ λ x, (deriv_const_sub _).trans $ by simp only [deriv_arcsin] + +lemma differentiable_on_arccos : differentiable_on ℝ arccos {-1, 1}ᶜ := +differentiable_on_arcsin.const_sub _ + +lemma times_cont_diff_on_arccos {n : with_top ℕ} : + times_cont_diff_on ℝ n arccos {-1, 1}ᶜ := +times_cont_diff_on_const.sub times_cont_diff_on_arcsin + +lemma times_cont_diff_at_arccos_iff {x : ℝ} {n : with_top ℕ} : + times_cont_diff_at ℝ n arccos x ↔ n = 0 ∨ (x ≠ -1 ∧ x ≠ 1) := +by refine iff.trans ⟨λ h, _, λ h, _⟩ times_cont_diff_at_arcsin_iff; + simpa [arccos] using (@times_cont_diff_at_const _ _ _ _ _ _ _ _ _ _ (π / 2)).sub h + +end arccos + +end real diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean index 0a319b84f1913..30c96f9ea5424 100644 --- a/src/data/complex/basic.lean +++ b/src/data/complex/basic.lean @@ -198,12 +198,12 @@ instance : star_ring ℂ := @[simp] lemma conj_re (z : ℂ) : (conj z).re = z.re := rfl @[simp] lemma conj_im (z : ℂ) : (conj z).im = -z.im := rfl -@[simp] lemma conj_of_real (r : ℝ) : conj (r : ℂ) = r := ext_iff.2 $ by simp [conj] +lemma conj_of_real (r : ℝ) : conj (r : ℂ) = r := ext_iff.2 $ by simp [conj] @[simp] lemma conj_I : conj I = -I := ext_iff.2 $ by simp -@[simp] lemma conj_bit0 (z : ℂ) : conj (bit0 z) = bit0 (conj z) := ext_iff.2 $ by simp [bit0] -@[simp] lemma conj_bit1 (z : ℂ) : conj (bit1 z) = bit1 (conj z) := ext_iff.2 $ by simp [bit0] +lemma conj_bit0 (z : ℂ) : conj (bit0 z) = bit0 (conj z) := ext_iff.2 $ by simp [bit0] +lemma conj_bit1 (z : ℂ) : conj (bit1 z) = bit1 (conj z) := ext_iff.2 $ by simp [bit0] @[simp] lemma conj_neg_I : conj (-I) = I := ext_iff.2 $ by simp diff --git a/src/geometry/euclidean/basic.lean b/src/geometry/euclidean/basic.lean index 3edd5bc4fbb77..17e595e16e518 100644 --- a/src/geometry/euclidean/basic.lean +++ b/src/geometry/euclidean/basic.lean @@ -7,6 +7,7 @@ import analysis.inner_product_space.projection import analysis.special_functions.trigonometric.inverse import algebra.quadratic_discriminant import linear_algebra.affine_space.finite_dimensional +import analysis.calculus.conformal.normed_space /-! # Euclidean spaces