Mathlib/Analysis/RCLike/Basic.lean

Mathlib · fixed commit 360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56

Fixed original declaration · Raw UTF-8 source · Back to the referring Card

1/-2Copyright (c) 2020 Frédéric Dupuis. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Frédéric Dupuis5-/6module78public import Mathlib.Algebra.Algebra.IsSimpleRing9public import Mathlib.Algebra.BigOperators.Balance10public import Mathlib.Algebra.Order.BigOperators.Expect11public import Mathlib.Algebra.Order.Star.Basic12public import Mathlib.Analysis.CStarAlgebra.Basic13public import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap14public import Mathlib.Analysis.Normed.Ring.Finite15public import Mathlib.Analysis.Real.Sqrt16public import Mathlib.Tactic.LinearCombination1718/-!19# `RCLike`: a typeclass for ℝ or ℂ2021This file defines the typeclass `RCLike` intended to have only two instances:22ℝ and ℂ. It is meant for definitions and theorems which hold for both the real and the complex case,23and in particular when the real case follows directly from the complex case by setting `re` to `id`,24`im` to zero and so on. Its API follows closely that of ℂ.2526Applications include defining inner products and Hilbert spaces for both the real and27complex case. One typically produces the definitions and proof for an arbitrary field of this28typeclass, which basically amounts to doing the complex case, and the two cases then fall out29immediately from the two instances of the class.3031The instance for `ℝ` is registered in this file.32The instance for `ℂ` is declared in `Mathlib/Analysis/Complex/Basic.lean`.3334## Implementation notes3536The coercion from reals into an `RCLike` field is done by registering `RCLike.ofReal` as37a `CoeTC`. For this to work, we must proceed carefully to avoid problems involving circular38coercions in the case `K=ℝ`; in particular, we cannot use the plain `Coe` and must set39priorities carefully. This problem was already solved for `ℕ`, and we copy the solution detailed40in `Mathlib/Data/Nat/Cast/Defs.lean`. See also Note [coercion into rings] for more details.4142In addition, several lemmas need to be set at priority 900 to make sure that they do not override43their counterparts in `Mathlib/Analysis/Complex/Basic.lean` (which causes linter errors).4445A few lemmas requiring heavier imports are in `Mathlib/Analysis/RCLike/Lemmas.lean`.46-/4748@[expose] public section4950open Fintype51open scoped BigOperators ComplexConjugate5253section5455local notation "𝓚" => algebraMap ℝ _5657/--58This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ.59-/60class RCLike (K : semiOutParam Type*) extends DenselyNormedField K, StarRing K,61    NormedAlgebra ℝ K, CompleteSpace K where62  /-- The real part as an additive monoid homomorphism -/63  re : K →+ ℝ64  /-- The imaginary part as an additive monoid homomorphism -/65  im : K →+ ℝ66  /-- Imaginary unit in `K`. Meant to be set to `0` for `K = ℝ`. -/67  I : K68  I_re_ax : re I = 069  I_mul_I_ax : I = 0 ∨ I * I = -170  re_add_im_ax : ∀ z : K, 𝓚 (re z) + 𝓚 (im z) * I = z71  ofReal_re_ax : ∀ r : ℝ, re (𝓚 r) = r72  ofReal_im_ax : ∀ r : ℝ, im (𝓚 r) = 073  mul_re_ax : ∀ z w : K, re (z * w) = re z * re w - im z * im w74  mul_im_ax : ∀ z w : K, im (z * w) = re z * im w + im z * re w75  conj_re_ax : ∀ z : K, re (conj z) = re z76  conj_im_ax : ∀ z : K, im (conj z) = -im z77  conj_I_ax : conj I = -I78  norm_sq_eq_def_ax : ∀ z : K, ‖z‖ ^ 2 = re z * re z + im z * im z79  mul_im_I_ax : ∀ z : K, im z * im I = im z80  /-- only an instance in the `ComplexOrder` scope -/81  [toPartialOrder : PartialOrder K]82  le_iff_re_im {z w : K} : z ≤ w ↔ re z ≤ re w ∧ im z = im w83  -- note we cannot put this in the `extends` clause84  [toDecidableEq : DecidableEq K]8586attribute [instance_reducible] RCLike.toPartialOrder RCLike.toDecidableEq87scoped[ComplexOrder] attribute [instance 100] RCLike.toPartialOrder88attribute [instance 100] RCLike.toDecidableEq8990end9192variable {K E : Type*} [RCLike K]9394namespace RCLike9596/-- Coercion from `ℝ` to an `RCLike` field. -/97@[coe] abbrev ofReal : ℝ → K := Algebra.cast9899/-- The priority must be set at 900 to ensure that coercions are tried in the right order.100See Note [coercion into rings], or `Mathlib/Data/Nat/Cast/Basic.lean` for more details. -/101noncomputable instance (priority := 900) algebraMapCoe : CoeTC ℝ K :=102  ⟨ofReal⟩103104theorem ofReal_alg (x : ℝ) : (x : K) = x • (1 : K) :=105  Algebra.algebraMap_eq_smul_one x106107theorem real_smul_eq_coe_mul (r : ℝ) (z : K) : r • z = (r : K) * z :=108  Algebra.smul_def r z109110theorem real_smul_eq_coe_smul [AddCommGroup E] [Module K E] [Module ℝ E] [IsScalarTower ℝ K E]111    (r : ℝ) (x : E) : r • x = (r : K) • x := by rw [RCLike.ofReal_alg, smul_one_smul]112113theorem algebraMap_eq_ofReal : ⇑(algebraMap ℝ K) = ofReal :=114  rfl115116@[simp, rclike_simps]117theorem re_add_im (z : K) : (re z : K) + im z * I = z :=118  RCLike.re_add_im_ax z119120@[simp, norm_cast, rclike_simps]121theorem ofReal_re : ∀ r : ℝ, re (r : K) = r :=122  RCLike.ofReal_re_ax123124@[simp, norm_cast, rclike_simps]125theorem ofReal_im : ∀ r : ℝ, im (r : K) = 0 :=126  RCLike.ofReal_im_ax127128@[simp, rclike_simps]129theorem mul_re : ∀ z w : K, re (z * w) = re z * re w - im z * im w :=130  RCLike.mul_re_ax131132@[simp, rclike_simps]133theorem mul_im : ∀ z w : K, im (z * w) = re z * im w + im z * re w :=134  RCLike.mul_im_ax135136theorem ext_iff {z w : K} : z = w ↔ re z = re w ∧ im z = im w :=137  ⟨fun h => h ▸ ⟨rfl, rfl⟩, fun ⟨h₁, h₂⟩ => re_add_im z ▸ re_add_im w ▸ h₁ ▸ h₂ ▸ rfl⟩138139theorem ext {z w : K} (hre : re z = re w) (him : im z = im w) : z = w :=140  ext_iff.2 ⟨hre, him⟩141142@[norm_cast]143theorem ofReal_zero : ((0 : ℝ) : K) = 0 :=144  algebraMap.coe_zero145146@[rclike_simps]147theorem zero_re : re (0 : K) = (0 : ℝ) :=148  map_zero re149150@[rclike_simps]151theorem zero_im : im (0 : K) = (0 : ℝ) :=152  map_zero im153154@[norm_cast]155theorem ofReal_one : ((1 : ℝ) : K) = 1 :=156  map_one (algebraMap ℝ K)157158@[simp, rclike_simps]159theorem one_re : re (1 : K) = 1 := by rw [← ofReal_one, ofReal_re]160161@[simp, rclike_simps]162theorem one_im : im (1 : K) = 0 := by rw [← ofReal_one, ofReal_im]163164theorem ofReal_injective : Function.Injective ((↑) : ℝ → K) :=165  (algebraMap ℝ K).injective166167@[norm_cast]168theorem ofReal_inj {z w : ℝ} : (z : K) = (w : K) ↔ z = w :=169  algebraMap.coe_inj _ _170171theorem ofReal_eq_zero {x : ℝ} : (x : K) = 0 ↔ x = 0 :=172  algebraMap.coe_eq_zero_iff _ _ _173174theorem ofReal_ne_zero {x : ℝ} : (x : K) ≠ 0 ↔ x ≠ 0 :=175  ofReal_eq_zero.not176177@[rclike_simps, norm_cast]178theorem ofReal_add (r s : ℝ) : ((r + s : ℝ) : K) = r + s :=179  algebraMap.coe_add _ _180181@[rclike_simps, norm_cast]182theorem ofReal_neg (r : ℝ) : ((-r : ℝ) : K) = -r :=183  algebraMap.coe_neg r184185@[rclike_simps, norm_cast]186theorem ofReal_sub (r s : ℝ) : ((r - s : ℝ) : K) = r - s :=187  map_sub (algebraMap ℝ K) r s188189@[rclike_simps, norm_cast]190theorem ofReal_sum {α : Type*} (s : Finset α) (f : α → ℝ) :191    ((∑ i ∈ s, f i : ℝ) : K) = ∑ i ∈ s, (f i : K) :=192  map_sum (algebraMap ℝ K) _ _193194@[simp, rclike_simps, norm_cast]195theorem ofReal_finsupp_sum {α M : Type*} [Zero M] (f : α →₀ M) (g : α → M → ℝ) :196    ((f.sum fun a b => g a b : ℝ) : K) = f.sum fun a b => (g a b : K) :=197  map_finsuppSum (algebraMap ℝ K) f g198199@[rclike_simps, norm_cast]200theorem ofReal_mul (r s : ℝ) : ((r * s : ℝ) : K) = r * s :=201  algebraMap.coe_mul _ _202203@[rclike_simps, norm_cast]204theorem ofReal_pow (r : ℝ) (n : ℕ) : ((r ^ n : ℝ) : K) = (r : K) ^ n :=205  map_pow (algebraMap ℝ K) r n206207@[rclike_simps, norm_cast]208theorem ofReal_prod {α : Type*} (s : Finset α) (f : α → ℝ) :209    ((∏ i ∈ s, f i : ℝ) : K) = ∏ i ∈ s, (f i : K) :=210  map_prod (algebraMap ℝ K) _ _211212@[simp, rclike_simps, norm_cast]213theorem ofReal_finsuppProd {α M : Type*} [Zero M] (f : α →₀ M) (g : α → M → ℝ) :214    ((f.prod fun a b => g a b : ℝ) : K) = f.prod fun a b => (g a b : K) :=215  map_finsuppProd _ f g216217@[simp, norm_cast, rclike_simps]218theorem real_smul_ofReal (r x : ℝ) : r • (x : K) = (r : K) * (x : K) :=219  real_smul_eq_coe_mul _ _220221@[rclike_simps]222theorem re_ofReal_mul (r : ℝ) (z : K) : re (↑r * z) = r * re z := by223  simp only [mul_re, ofReal_im, zero_mul, ofReal_re, sub_zero]224225@[rclike_simps]226theorem re_mul_ofReal (z : K) (r : ℝ) : re (z * ↑r) = re z * r := by227  rw [mul_comm, re_ofReal_mul, mul_comm]228229@[rclike_simps]230theorem im_ofReal_mul (r : ℝ) (z : K) : im (↑r * z) = r * im z := by231  simp only [add_zero, ofReal_im, zero_mul, ofReal_re, mul_im]232233@[rclike_simps]234theorem im_mul_ofReal (z : K) (r : ℝ) : im (z * ↑r) = im z * r := by235  rw [mul_comm, im_ofReal_mul, mul_comm]236237@[rclike_simps]238theorem smul_re (r : ℝ) (z : K) : re (r • z) = r * re z := by239  rw [real_smul_eq_coe_mul, re_ofReal_mul]240241@[rclike_simps]242theorem smul_im (r : ℝ) (z : K) : im (r • z) = r * im z := by243  rw [real_smul_eq_coe_mul, im_ofReal_mul]244245@[rclike_simps, norm_cast]246theorem norm_ofReal (r : ℝ) : ‖(r : K)‖ = |r| :=247  norm_algebraMap' K r248249@[simp]250theorem re_ofReal_pow (a : ℝ) (n : ℕ) : re ((a : K) ^ n) = a ^ n := by251  rw [← ofReal_pow, @ofReal_re]252253@[simp]254theorem im_ofReal_pow (a : ℝ) (n : ℕ) : im ((a : K) ^ n) = 0 := by255  rw [← @ofReal_pow, @ofReal_im_ax]256257/-! ### Characteristic zero -/258259-- see Note [lower instance priority]260/-- ℝ and ℂ are both of characteristic zero. -/261instance (priority := 100) charZero_rclike : CharZero K :=262  (RingHom.charZero_iff (algebraMap ℝ K).injective).1 inferInstance263264@[rclike_simps, norm_cast]265lemma ofReal_expect {α : Type*} (s : Finset α) (f : α → ℝ) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : K) :=266  map_expect (algebraMap ..) ..267268@[norm_cast]269lemma ofReal_balance {ι : Type*} [Fintype ι] (f : ι → ℝ) (i : ι) :270    ((balance f i : ℝ) : K) = balance ((↑) ∘ f) i := map_balance (algebraMap ..) ..271272@[simp] lemma ofReal_comp_balance {ι : Type*} [Fintype ι] (f : ι → ℝ) :273    ofReal ∘ balance f = balance (ofReal ∘ f : ι → K) := funext <| ofReal_balance _274275/-! ### The imaginary unit, `I` -/276277/-- The imaginary unit. -/278@[simp, rclike_simps]279theorem I_re : re (I : K) = 0 :=280  I_re_ax281282@[simp, rclike_simps]283theorem I_im (z : K) : im z * im (I : K) = im z :=284  mul_im_I_ax z285286@[simp, rclike_simps]287theorem I_im' (z : K) : im (I : K) * im z = im z := by rw [mul_comm, I_im]288289-- Not `@[simp]` since `simp` can prove this.290@[rclike_simps]291theorem I_mul_re (z : K) : re (I * z) = -im z := by292  simp only [I_re, zero_sub, I_im', zero_mul, mul_re]293294theorem I_mul_I : (I : K) = 0 ∨ (I : K) * I = -1 :=295  I_mul_I_ax296297variable (𝕜) in298lemma I_eq_zero_or_im_I_eq_one : (I : K) = 0 ∨ im (I : K) = 1 :=299  I_mul_I (K := K) |>.imp_right fun h ↦ by simpa [h] using (I_mul_re (I : K)).symm300301@[simp, rclike_simps]302theorem conj_re (z : K) : re (conj z) = re z :=303  RCLike.conj_re_ax z304305@[simp, rclike_simps]306theorem conj_im (z : K) : im (conj z) = -im z :=307  RCLike.conj_im_ax z308309@[simp, rclike_simps]310theorem conj_I : conj (I : K) = -I :=311  RCLike.conj_I_ax312313@[simp, rclike_simps]314theorem conj_ofReal (r : ℝ) : conj (r : K) = (r : K) := by315  rw [ext_iff]316  simp only [ofReal_im, conj_im, conj_re, and_self_iff, neg_zero]317318theorem conj_nat_cast (n : ℕ) : conj (n : K) = n := map_natCast _ _319320theorem conj_ofNat (n : ℕ) [n.AtLeastTwo] : conj (ofNat(n) : K) = ofNat(n) :=321  map_ofNat _ _322323@[rclike_simps, simp]324theorem conj_neg_I : conj (-I) = (I : K) := by rw [map_neg, conj_I, neg_neg]325326theorem conj_eq_re_sub_im (z : K) : conj z = re z - im z * I :=327  (congr_arg conj (re_add_im z).symm).trans <| by328    rw [map_add, map_mul, conj_I, conj_ofReal, conj_ofReal, mul_neg, sub_eq_add_neg]329330theorem sub_conj (z : K) : z - conj z = 2 * im z * I :=331  calc332    z - conj z = re z + im z * I - (re z - im z * I) := by rw [re_add_im, ← conj_eq_re_sub_im]333    _ = 2 * im z * I := by rw [add_sub_sub_cancel, ← two_mul, mul_assoc]334335@[rclike_simps]336theorem conj_smul (r : ℝ) (z : K) : conj (r • z) = r • conj z := by337  rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,338    real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]339340theorem add_conj (z : K) : z + conj z = 2 * re z :=341  calc342    z + conj z = re z + im z * I + (re z - im z * I) := by rw [re_add_im, conj_eq_re_sub_im]343    _ = 2 * re z := by rw [add_add_sub_cancel, two_mul]344345theorem re_eq_add_conj (z : K) : ↑(re z) = (z + conj z) / 2 := by346  rw [add_conj, mul_div_cancel_left₀ (re z : K) two_ne_zero]347348theorem im_eq_conj_sub (z : K) : ↑(im z) = I * (conj z - z) / 2 := by349  rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,350    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]351352open List in353/-- There are several equivalent ways to say that a number `z` is in fact a real number. -/354theorem is_real_TFAE (z : K) :355    TFAE [conj z = z, ∃ r : ℝ, (r : K) = z, ↑(re z) = z, im z = 0, IsSelfAdjoint z] := by356  tfae_have 1 → 4357  | h => by358    rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,359      ofReal_zero]360  tfae_have 4 → 3361  | h => by362    conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]363  tfae_have 3 → 2 := fun h => ⟨_, h⟩364  tfae_have 2 → 1 := fun ⟨r, hr⟩ => hr ▸ conj_ofReal _365  tfae_have 1 → 5 := fun _ => by rwa [isSelfAdjoint_iff]366  tfae_have 5 → 1 := fun hz => by rwa [isSelfAdjoint_iff] at hz367  tfae_finish368369set_option linter.style.whitespace false in -- manual alignment is not recognised370theorem conj_eq_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) :=371  calc372    _ ↔ ∃ r : ℝ, (r : K) = z := (is_real_TFAE z).out 0 1373    _ ↔ _                    := by simp only [eq_comm]374375theorem conj_eq_iff_re {z : K} : conj z = z ↔ (re z : K) = z :=376  (is_real_TFAE z).out 0 2377378theorem conj_eq_iff_im {z : K} : conj z = z ↔ im z = 0 :=379  (is_real_TFAE z).out 0 3380381@[simp]382theorem star_def : (Star.star : K → K) = conj :=383  rfl384385lemma im_eq_zero_iff_isSelfAdjoint {x : K} : im x = 0 ↔ IsSelfAdjoint x :=386  is_real_TFAE x |>.out 3 4387388lemma re_eq_ofReal_of_isSelfAdjoint {x : K} {y : ℝ} (hx : IsSelfAdjoint x) :389    re x = y ↔ x = y := by390  simp [RCLike.ext_iff (K := K), hx, im_eq_zero_iff_isSelfAdjoint]391392lemma ofReal_eq_re_of_isSelfAdjoint {x : K} {y : ℝ} (hx : IsSelfAdjoint x) :393    y = re x ↔ y = x := by394  simpa [eq_comm] using re_eq_ofReal_of_isSelfAdjoint hx395396variable (K)397398/-- Conjugation as a ring equivalence. This is used to convert the inner product into a399sesquilinear product. -/400abbrev conjToRingEquiv : K ≃+* Kᵐᵒᵖ :=401  starRingEquiv402403variable {K} {z : K}404405/-- The norm squared function. -/406def normSq : K →*₀ ℝ where407  toFun z := re z * re z + im z * im z408  map_zero' := by simp only [add_zero, mul_zero, map_zero]409  map_one' := by simp only [one_im, add_zero, mul_one, one_re, mul_zero]410  map_mul' z w := by411    simp only [mul_im, mul_re]412    ring413414theorem normSq_apply (z : K) : normSq z = re z * re z + im z * im z :=415  rfl416417theorem norm_sq_eq_def {z : K} : ‖z‖ ^ 2 = re z * re z + im z * im z :=418  norm_sq_eq_def_ax z419420theorem normSq_eq_def' (z : K) : normSq z = ‖z‖ ^ 2 :=421  norm_sq_eq_def.symm422423@[rclike_simps]424theorem normSq_zero : normSq (0 : K) = 0 :=425  normSq.map_zero426427@[rclike_simps]428theorem normSq_one : normSq (1 : K) = 1 :=429  normSq.map_one430431theorem normSq_nonneg (z : K) : 0 ≤ normSq z :=432  add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)433434-- Not `@[simp]` since `simp` can prove this.435@[rclike_simps]436theorem normSq_eq_zero {z : K} : normSq z = 0 ↔ z = 0 :=437  map_eq_zero _438439@[simp, rclike_simps]440theorem normSq_pos {z : K} : 0 < normSq z ↔ z ≠ 0 := by441  rw [lt_iff_le_and_ne, Ne, eq_comm]; simp [normSq_nonneg]442443@[simp, rclike_simps]444theorem normSq_neg (z : K) : normSq (-z) = normSq z := by simp only [normSq_eq_def', norm_neg]445446@[simp, rclike_simps]447theorem normSq_conj (z : K) : normSq (conj z) = normSq z := by448  simp only [normSq_apply, neg_mul, mul_neg, neg_neg, rclike_simps]449450-- Not `@[simp]` since `simp` can prove this.451@[rclike_simps]452theorem normSq_mul (z w : K) : normSq (z * w) = normSq z * normSq w :=453  map_mul _ z w454455theorem normSq_add (z w : K) : normSq (z + w) = normSq z + normSq w + 2 * re (z * conj w) := by456  simp only [normSq_apply, map_add, rclike_simps]457  ring458459theorem re_sq_le_normSq (z : K) : re z * re z ≤ normSq z :=460  le_add_of_nonneg_right (mul_self_nonneg _)461462theorem im_sq_le_normSq (z : K) : im z * im z ≤ normSq z :=463  le_add_of_nonneg_left (mul_self_nonneg _)464465theorem mul_conj (z : K) : z * conj z = ‖z‖ ^ 2 := by466  apply ext <;> simp [← ofReal_pow, norm_sq_eq_def, mul_comm]467468theorem conj_mul (z : K) : conj z * z = ‖z‖ ^ 2 := by rw [mul_comm, mul_conj]469470lemma inv_eq_conj (hz : ‖z‖ = 1) : z⁻¹ = conj z :=471  inv_eq_of_mul_eq_one_left <| by simp_rw [conj_mul, hz, algebraMap.coe_one, one_pow]472473theorem normSq_sub (z w : K) : normSq (z - w) = normSq z + normSq w - 2 * re (z * conj w) := by474  simp only [normSq_add, sub_eq_add_neg, map_neg, mul_neg, normSq_neg, map_neg]475476theorem sqrt_normSq_eq_norm {z : K} : √(normSq z) = ‖z‖ := by477  rw [normSq_eq_def', Real.sqrt_sq (norm_nonneg _)]478479/-! ### Inversion -/480481@[rclike_simps, norm_cast]482theorem ofReal_inv (r : ℝ) : ((r⁻¹ : ℝ) : K) = (r : K)⁻¹ :=483  map_inv₀ _ r484485theorem inv_def (z : K) : z⁻¹ = conj z * ((‖z‖ ^ 2)⁻¹ : ℝ) := by486  rcases eq_or_ne z 0 with (rfl | h₀)487  · simp488  · apply inv_eq_of_mul_eq_one_right489    rw [← mul_assoc, mul_conj, ofReal_inv, ofReal_pow, mul_inv_cancel₀]490    simpa491492@[simp, rclike_simps]493theorem inv_re (z : K) : re z⁻¹ = re z / normSq z := by494  rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]495496@[simp, rclike_simps]497theorem inv_im (z : K) : im z⁻¹ = -im z / normSq z := by498  rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]499500theorem div_re (z w : K) : re (z / w) = re z * re w / normSq w + im z * im w / normSq w := by501  simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, neg_mul, mul_neg, neg_neg,502    rclike_simps]503504theorem div_im (z w : K) : im (z / w) = im z * re w / normSq w - re z * im w / normSq w := by505  simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm, neg_mul, mul_neg,506    rclike_simps]507508-- Not `@[simp]` since `simp` can prove this509@[rclike_simps]510theorem conj_inv (x : K) : conj x⁻¹ = (conj x)⁻¹ :=511  star_inv₀ _512513lemma conj_div (x y : K) : conj (x / y) = conj x / conj y := map_div' conj conj_inv _ _514515--TODO: Do we rather want the map as an explicit definition?516lemma exists_norm_eq_mul_self (x : K) : ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x := by517  obtain rfl | hx := eq_or_ne x 0518  · exact ⟨1, by simp⟩519  · exact ⟨‖x‖ / x, by simp [norm_ne_zero_iff.2, hx]⟩520521lemma exists_norm_mul_eq_self (x : K) : ∃ c, ‖c‖ = 1 ∧ c * ‖x‖ = x := by522  obtain rfl | hx := eq_or_ne x 0523  · exact ⟨1, by simp⟩524  · exact ⟨x / ‖x‖, by simp [norm_ne_zero_iff.2, hx]⟩525526@[rclike_simps, norm_cast]527theorem ofReal_div (r s : ℝ) : ((r / s : ℝ) : K) = r / s :=528  map_div₀ (algebraMap ℝ K) r s529530theorem div_re_ofReal {z : K} {r : ℝ} : re (z / r) = re z / r := by531  rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, re_ofReal_mul]532533@[rclike_simps, norm_cast]534theorem ofReal_zpow (r : ℝ) (n : ℤ) : ((r ^ n : ℝ) : K) = (r : K) ^ n :=535  map_zpow₀ (algebraMap ℝ K) r n536537theorem I_mul_I_of_nonzero : (I : K) ≠ 0 → (I : K) * I = -1 :=538  I_mul_I_ax.resolve_left539540@[simp, rclike_simps]541theorem inv_I : (I : K)⁻¹ = -I := by542  by_cases h : (I : K) = 0543  · simp [h]544  · field_simp545    linear_combination I_mul_I_of_nonzero h546547@[simp, rclike_simps]548theorem div_I (z : K) : z / I = -(z * I) := by rw [div_eq_mul_inv, inv_I, mul_neg]549550-- Not `@[simp]` since `simp` can prove this.551@[rclike_simps]552theorem normSq_inv (z : K) : normSq z⁻¹ = (normSq z)⁻¹ :=553  map_inv₀ normSq z554555-- Not `@[simp]` since `simp` can prove this.556@[rclike_simps]557theorem normSq_div (z w : K) : normSq (z / w) = normSq z / normSq w :=558  map_div₀ normSq z w559560@[simp 1100, rclike_simps]561theorem norm_conj (z : K) : ‖conj z‖ = ‖z‖ := by simp only [← sqrt_normSq_eq_norm, normSq_conj]562563@[simp 1100, rclike_simps] lemma nnnorm_conj (z : K) : ‖conj z‖₊ = ‖z‖₊ := by simp [nnnorm]564565@[simp 1100, rclike_simps] lemma enorm_conj (z : K) : ‖conj z‖ₑ = ‖z‖ₑ := by simp [enorm]566567instance (priority := 100) : CStarRing K where568  norm_mul_self_le x := le_of_eq <| ((norm_mul _ _).trans <| congr_arg (· * ‖x‖) (norm_conj _)).symm569570instance : StarModule ℝ K where571  star_smul r a := by572    apply RCLike.ext <;> simp [RCLike.smul_re, RCLike.smul_im]573574/-! ### Cast lemmas -/575576@[rclike_simps, norm_cast]577theorem ofReal_natCast (n : ℕ) : ((n : ℝ) : K) = n :=578  map_natCast (algebraMap ℝ K) n579580@[simp, rclike_simps]581theorem natCast_re (n : ℕ) : re (n : K) = n := by rw [← ofReal_natCast, ofReal_re]582583@[simp, rclike_simps, norm_cast]584theorem natCast_im (n : ℕ) : im (n : K) = 0 := by rw [← ofReal_natCast, ofReal_im]585@[simp, rclike_simps]586theorem ofNat_re (n : ℕ) [n.AtLeastTwo] : re (ofNat(n) : K) = ofNat(n) :=587  natCast_re n588@[simp, rclike_simps]589theorem ofNat_im (n : ℕ) [n.AtLeastTwo] : im (ofNat(n) : K) = 0 :=590  natCast_im n591592@[rclike_simps, norm_cast]593theorem ofReal_ofNat (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℝ) : K) = ofNat(n) :=594  ofReal_natCast n595596theorem ofNat_mul_re (n : ℕ) [n.AtLeastTwo] (z : K) :597    re (ofNat(n) * z) = ofNat(n) * re z := by598  rw [← ofReal_ofNat, re_ofReal_mul]599600theorem ofNat_mul_im (n : ℕ) [n.AtLeastTwo] (z : K) :601    im (ofNat(n) * z) = ofNat(n) * im z := by602  rw [← ofReal_ofNat, im_ofReal_mul]603604@[rclike_simps, norm_cast]605theorem ofReal_intCast (n : ℤ) : ((n : ℝ) : K) = n :=606  map_intCast _ n607608@[simp, rclike_simps]609theorem intCast_re (n : ℤ) : re (n : K) = n := by rw [← ofReal_intCast, ofReal_re]610611@[simp, rclike_simps, norm_cast]612theorem intCast_im (n : ℤ) : im (n : K) = 0 := by rw [← ofReal_intCast, ofReal_im]613614@[rclike_simps, norm_cast]615theorem ofReal_nnratCast (n : ℚ≥0) : ((n : ℝ) : K) = n :=616  map_nnratCast _ n617618@[simp, rclike_simps]619theorem nnratCast_re (q : ℚ≥0) : re (q : K) = q := by rw [← ofReal_nnratCast, ofReal_re]620621@[simp, rclike_simps, norm_cast]622theorem nnratCast_im (q : ℚ≥0) : im (q : K) = 0 := by rw [← ofReal_nnratCast, ofReal_im]623624@[rclike_simps, norm_cast]625theorem ofReal_ratCast (n : ℚ) : ((n : ℝ) : K) = n :=626  map_ratCast _ n627628@[simp, rclike_simps]629theorem ratCast_re (q : ℚ) : re (q : K) = q := by rw [← ofReal_ratCast, ofReal_re]630631@[simp, rclike_simps, norm_cast]632theorem ratCast_im (q : ℚ) : im (q : K) = 0 := by rw [← ofReal_ratCast, ofReal_im]633634open OfScientific (ofScientific)635636@[rclike_simps, norm_cast]637theorem ofReal_ofScientific (m : ℕ) (s : Bool) (e : ℕ) :638    ((ofScientific m s e : ℝ) : K) = ofScientific m s e := ofReal_nnratCast _639640@[simp, rclike_simps]641theorem ofScientific_re (m : ℕ) (s : Bool) (e : ℕ) :642    re (ofScientific m s e : K) = ofScientific m s e := by rw [← ofReal_ofScientific, ofReal_re]643644@[simp, rclike_simps, norm_cast]645theorem ofScientific_im (m : ℕ) (s : Bool) (e : ℕ) :646    im (ofScientific m s e : K) = 0 := by rw [← ofReal_ofScientific, ofReal_im]647648/-! ### Norm -/649650theorem norm_of_nonneg {r : ℝ} (h : 0 ≤ r) : ‖(r : K)‖ = r :=651  (norm_ofReal _).trans (abs_of_nonneg h)652653@[simp 1100, rclike_simps, norm_cast]654theorem norm_natCast (n : ℕ) : ‖(n : K)‖ = n := by655  rw [← ofReal_natCast]656  exact norm_of_nonneg (Nat.cast_nonneg n)657658@[simp, rclike_simps, norm_cast] lemma nnnorm_natCast (n : ℕ) : ‖(n : K)‖₊ = n := by simp [nnnorm]659660@[simp, rclike_simps]661theorem norm_ofNat (n : ℕ) [n.AtLeastTwo] : ‖(ofNat(n) : K)‖ = ofNat(n) :=662  norm_natCast n663664@[simp, rclike_simps]665lemma nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] : ‖(ofNat(n) : K)‖₊ = ofNat(n) :=666  nnnorm_natCast n667668lemma norm_two : ‖(2 : K)‖ = 2 := norm_ofNat 2669lemma nnnorm_two : ‖(2 : K)‖₊ = 2 := nnnorm_ofNat 2670671@[simp, rclike_simps, norm_cast]672lemma norm_nnratCast (q : ℚ≥0) : ‖(q : K)‖ = q := by673  rw [← ofReal_nnratCast]; exact norm_of_nonneg q.cast_nonneg674675@[simp, rclike_simps, norm_cast]676lemma nnnorm_nnratCast (q : ℚ≥0) : ‖(q : K)‖₊ = q := by simp [nnnorm]; rfl677678variable (K) in679lemma norm_nsmul [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) : ‖n • x‖ = n • ‖x‖ := by680  simpa [Nat.cast_smul_eq_nsmul] using norm_smul (n : K) x681682variable (K) in683lemma nnnorm_nsmul [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) :684    ‖n • x‖₊ = n • ‖x‖₊ := by simpa [Nat.cast_smul_eq_nsmul] using nnnorm_smul (n : K) x685686theorem mul_self_norm (z : K) : ‖z‖ * ‖z‖ = normSq z := by rw [normSq_eq_def', sq]687688attribute [rclike_simps] norm_zero norm_one norm_eq_zero abs_norm norm_inv norm_div689690theorem abs_re_le_norm (z : K) : |re z| ≤ ‖z‖ := by691  rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]692  apply re_sq_le_normSq693694theorem abs_im_le_norm (z : K) : |im z| ≤ ‖z‖ := by695  rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]696  apply im_sq_le_normSq697698theorem norm_re_le_norm (z : K) : ‖re z‖ ≤ ‖z‖ :=699  abs_re_le_norm z700701theorem norm_im_le_norm (z : K) : ‖im z‖ ≤ ‖z‖ :=702  abs_im_le_norm z703704theorem re_le_norm (z : K) : re z ≤ ‖z‖ :=705  (abs_le.1 (abs_re_le_norm z)).2706707theorem im_le_norm (z : K) : im z ≤ ‖z‖ :=708  (abs_le.1 (abs_im_le_norm _)).2709710theorem im_eq_zero_of_le {a : K} (h : ‖a‖ ≤ re a) : im a = 0 := by711  simpa only [mul_self_norm a, normSq_apply, left_eq_add, mul_self_eq_zero]712    using congr_arg (fun z => z * z) ((re_le_norm a).antisymm h)713714theorem re_eq_self_of_le {a : K} (h : ‖a‖ ≤ re a) : (re a : K) = a := by715  rw [← conj_eq_iff_re, conj_eq_iff_im, im_eq_zero_of_le h]716717open IsAbsoluteValue718719theorem abs_re_div_norm_le_one (z : K) : |re z / ‖z‖| ≤ 1 := by720  rw [abs_div, abs_norm]721  exact div_le_one_of_le₀ (abs_re_le_norm _) (norm_nonneg _)722723theorem abs_im_div_norm_le_one (z : K) : |im z / ‖z‖| ≤ 1 := by724  rw [abs_div, abs_norm]725  exact div_le_one_of_le₀ (abs_im_le_norm _) (norm_nonneg _)726727theorem norm_I_of_ne_zero (hI : (I : K) ≠ 0) : ‖(I : K)‖ = 1 := by728  rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,729    I_mul_I_of_nonzero hI, norm_neg, norm_one]730731theorem re_eq_norm_of_mul_conj (x : K) : re (x * conj x) = ‖x * conj x‖ := by732  rw [mul_conj, ← ofReal_pow]; simp [-map_pow]733734theorem norm_sq_re_add_conj (x : K) : ‖x + conj x‖ ^ 2 = re (x + conj x) ^ 2 := by735  rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]736737theorem norm_sq_re_conj_add (x : K) : ‖conj x + x‖ ^ 2 = re (conj x + x) ^ 2 := by738  rw [add_comm, norm_sq_re_add_conj]739740instance : NormSMulClass ℤ K where741  norm_smul r x := by742    rw [zsmul_eq_mul, norm_mul, ← ofReal_intCast, norm_ofReal, Int.norm_eq_abs]743744/-! ### Cauchy sequences -/745746theorem isCauSeq_re (f : CauSeq K norm) : IsCauSeq abs fun n => re (f n) := fun _ ε0 =>747  (f.cauchy ε0).imp fun i H j ij =>748    lt_of_le_of_lt (by simpa only [map_sub] using abs_re_le_norm (f j - f i)) (H _ ij)749750theorem isCauSeq_im (f : CauSeq K norm) : IsCauSeq abs fun n => im (f n) := fun _ ε0 =>751  (f.cauchy ε0).imp fun i H j ij =>752    lt_of_le_of_lt (by simpa only [map_sub] using abs_im_le_norm (f j - f i)) (H _ ij)753754/-- The real part of a K Cauchy sequence, as a real Cauchy sequence. -/755noncomputable def cauSeqRe (f : CauSeq K norm) : CauSeq ℝ abs :=756  ⟨_, isCauSeq_re f⟩757758/-- The imaginary part of a K Cauchy sequence, as a real Cauchy sequence. -/759noncomputable def cauSeqIm (f : CauSeq K norm) : CauSeq ℝ abs :=760  ⟨_, isCauSeq_im f⟩761762theorem isCauSeq_norm {f : ℕ → K} (hf : IsCauSeq norm f) : IsCauSeq abs (norm ∘ f) := fun ε ε0 =>763  let ⟨i, hi⟩ := hf ε ε0764  ⟨i, fun j hj => lt_of_le_of_lt (abs_norm_sub_norm_le _ _) (hi j hj)⟩765766lemma I_mem_skewAdjoint : I ∈ skewAdjoint K := by simp [skewAdjoint.mem_iff]767768end RCLike769770section771variable {A : Type*} [AddCommGroup A] [StarAddMonoid A] [Module K A] [StarModule K A] {a : A}772773open RCLike774775lemma IsSelfAdjoint.I_smul_mem_skewAdjoint (h : IsSelfAdjoint a) :776    (I : K) • a ∈ skewAdjoint A := h.smul_mem_skewAdjoint I_mem_skewAdjoint777778lemma IsSelfAdjoint.I_smul_of_mem_skewAdjoint (h : a ∈ skewAdjoint A) :779    IsSelfAdjoint ((I : K) • a) := isSelfAdjoint_smul_of_mem_skewAdjoint I_mem_skewAdjoint h780781end782783section Instances784785noncomputable instance Real.instRCLike : RCLike ℝ where786  re := AddMonoidHom.id ℝ787  im := 0788  I := 0789  I_re_ax := by simp only [map_zero]790  I_mul_I_ax := Or.intro_left _ rfl791  re_add_im_ax z := by792    simp only [add_zero, mul_zero, Algebra.algebraMap_self, RingHom.id_apply, AddMonoidHom.id_apply]793  ofReal_re_ax _ := rfl794  ofReal_im_ax _ := rfl795  mul_re_ax z w := by simp only [sub_zero, mul_zero, AddMonoidHom.zero_apply, AddMonoidHom.id_apply]796  mul_im_ax z w := by simp only [add_zero, zero_mul, mul_zero, AddMonoidHom.zero_apply]797  conj_re_ax z := by simp only [starRingEnd_apply, star_id_of_comm]798  conj_im_ax _ := by simp only [neg_zero, AddMonoidHom.zero_apply]799  conj_I_ax := by simp only [map_zero, neg_zero]800  norm_sq_eq_def_ax z := by simp only [sq, Real.norm_eq_abs, ← abs_mul, abs_mul_self z, add_zero,801    mul_zero, AddMonoidHom.zero_apply, AddMonoidHom.id_apply]802  mul_im_I_ax _ := by simp only [mul_zero, AddMonoidHom.zero_apply]803  le_iff_re_im := (and_iff_left rfl).symm804805end Instances806807namespace RCLike808809section NormedField810variable [NormedField E] [CharZero E] [NormedSpace K E]811include K812813variable (K) in814lemma norm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖ = q • ‖x‖ := by815  simpa [NNRat.cast_smul_eq_nnqsmul] using! norm_smul (q : K) x816817variable (K) in818lemma nnnorm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖₊ = q • ‖x‖₊ := by819  simpa [NNRat.cast_smul_eq_nnqsmul] using! nnnorm_smul (q : K) x820821@[bound]822lemma norm_expect_le {ι : Type*} {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=823  Finset.le_expect_of_subadditive norm_zero norm_add_le fun _ _ ↦ by rw [norm_nnqsmul K]824825end NormedField826827section Order828829open scoped ComplexOrder830variable {z w : K}831832theorem lt_iff_re_im : z < w ↔ re z < re w ∧ im z = im w := by833  simp_rw [lt_iff_le_and_ne, @RCLike.le_iff_re_im K]834  constructor835  · rintro ⟨⟨hr, hi⟩, heq⟩836    exact ⟨⟨hr, mt (fun hreq => ext hreq hi) heq⟩, hi⟩837  · rintro ⟨⟨hr, hrn⟩, hi⟩838    exact ⟨⟨hr, hi⟩, ne_of_apply_ne _ hrn⟩839840theorem nonneg_iff : 0 ≤ z ↔ 0 ≤ re z ∧ im z = 0 := by841  simpa only [map_zero, eq_comm] using le_iff_re_im (z := 0) (w := z)842843theorem pos_iff : 0 < z ↔ 0 < re z ∧ im z = 0 := by844  simpa only [map_zero, eq_comm] using lt_iff_re_im (z := 0) (w := z)845846theorem nonpos_iff : z ≤ 0 ↔ re z ≤ 0 ∧ im z = 0 := by847  simpa only [map_zero] using le_iff_re_im (z := z) (w := 0)848849theorem neg_iff : z < 0 ↔ re z < 0 ∧ im z = 0 := by850  simpa only [map_zero] using lt_iff_re_im (z := z) (w := 0)851852lemma nonneg_iff_exists_ofReal : 0 ≤ z ↔ ∃ x ≥ (0 : ℝ), x = z := by853  simp_rw [nonneg_iff (K := K), ext_iff (K := K)]; aesop854855lemma pos_iff_exists_ofReal : 0 < z ↔ ∃ x > (0 : ℝ), x = z := by856  simp_rw [pos_iff (K := K), ext_iff (K := K)]; aesop857858lemma nonpos_iff_exists_ofReal : z ≤ 0 ↔ ∃ x ≤ (0 : ℝ), x = z := by859  simp_rw [nonpos_iff (K := K), ext_iff (K := K)]; aesop860861lemma neg_iff_exists_ofReal : z < 0 ↔ ∃ x < (0 : ℝ), x = z := by862  simp_rw [neg_iff (K := K), ext_iff (K := K)]; aesop863864@[simp, norm_cast]865lemma ofReal_le_ofReal {x y : ℝ} : (x : K) ≤ (y : K) ↔ x ≤ y := by866  rw [le_iff_re_im]867  simp868869@[simp, norm_cast]870lemma ofReal_lt_ofReal {x y : ℝ} : (x : K) < (y : K) ↔ x < y := by871  rw [lt_iff_re_im]872  simp873874@[simp, norm_cast]875lemma ofReal_nonneg {x : ℝ} : 0 ≤ (x : K) ↔ 0 ≤ x := by876  rw [← ofReal_zero, ofReal_le_ofReal]877878@[simp, norm_cast]879lemma ofReal_nonpos {x : ℝ} : (x : K) ≤ 0 ↔ x ≤ 0 := by880  rw [← ofReal_zero, ofReal_le_ofReal]881882@[simp, norm_cast]883lemma ofReal_pos {x : ℝ} : 0 < (x : K) ↔ 0 < x := by884  rw [← ofReal_zero, ofReal_lt_ofReal]885886@[simp, norm_cast]887lemma ofReal_lt_zero {x : ℝ} : (x : K) < 0 ↔ x < 0 := by888  rw [← ofReal_zero, ofReal_lt_ofReal]889890lemma norm_le_re_iff_eq_norm {z : K} :891    ‖z‖ ≤ re z ↔ z = ‖z‖ := by892  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩893  · have h' : ‖z‖ = re z := (le_antisymm (re_le_norm z) h).symm894    rw [h', re_eq_self_of_le h]895  · rw [h]896    simp897898lemma re_le_neg_norm_iff_eq_neg_norm {z : K} :899    re z ≤ -‖z‖ ↔ z = -‖z‖ := by900  simpa [neg_eq_iff_eq_neg, le_neg] using norm_le_re_iff_eq_norm (z := -z)901902lemma norm_of_nonneg' {x : K} (hx : 0 ≤ x) : ‖x‖ = x := by903  rw [eq_comm, ← norm_le_re_iff_eq_norm, ← sqrt_normSq_eq_norm, normSq_apply]904  simp [nonneg_iff.mp hx]905906lemma re_nonneg_of_nonneg {x : K} (hx : IsSelfAdjoint x) : 0 ≤ re x ↔ 0 ≤ x := by907  simp [nonneg_iff (K := K), conj_eq_iff_im.mp hx]908909@[gcongr]910lemma re_le_re {x y : K} (h : x ≤ y) : re x ≤ re y := by911  rw [RCLike.le_iff_re_im] at h912  exact h.1913914lemma re_monotone : Monotone (re : K → ℝ) :=915  fun _ _ => re_le_re916917protected lemma inv_pos_of_pos (hz : 0 < z) : 0 < z⁻¹ := by918  rw [pos_iff_exists_ofReal] at hz919  obtain ⟨x, hx, hx'⟩ := hz920  rw [← hx', ← ofReal_inv, ofReal_pos]921  exact inv_pos_of_pos hx922923protected lemma inv_pos : 0 < z⁻¹ ↔ 0 < z := by924  refine ⟨fun h => ?_, fun h => RCLike.inv_pos_of_pos h⟩925  rw [← inv_inv z]926  exact RCLike.inv_pos_of_pos h927928/-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℝ` and `ℂ` are star ordered rings.929(That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)930931Note this is only an instance with `open scoped ComplexOrder`. -/932lemma toStarOrderedRing : StarOrderedRing K :=933  StarOrderedRing.of_nonneg_iff'934    (h_add := fun {x y} hxy z => by935      rw [RCLike.le_iff_re_im] at *936      simpa [map_add, add_le_add_iff_left, add_right_inj] using hxy)937    (h_nonneg_iff := fun x => by938      rw [nonneg_iff]939      refine ⟨fun h ↦ ⟨√(re x), by simp [ext_iff (K := K), h.1, h.2]⟩, ?_⟩940      rintro ⟨s, rfl⟩941      simp [mul_comm, mul_self_nonneg, add_nonneg])942943scoped[ComplexOrder] attribute [instance] RCLike.toStarOrderedRing944945lemma toZeroLEOneClass : ZeroLEOneClass K where946  zero_le_one := by simp [@RCLike.le_iff_re_im K]947948scoped[ComplexOrder] attribute [instance] RCLike.toZeroLEOneClass949950lemma toIsOrderedAddMonoid : IsOrderedAddMonoid K where951  add_le_add_left _ _ := add_le_add_left952953scoped[ComplexOrder] attribute [instance] RCLike.toIsOrderedAddMonoid954955/-- With `z ≤ w` iff `w - z` is real and nonnegative, `ℝ` and `ℂ` are strictly ordered rings.956957Note this is only an instance with `open scoped ComplexOrder`. -/958lemma toIsStrictOrderedRing : IsStrictOrderedRing K :=959  .of_mul_pos fun z w hz hw ↦ by960    rw [lt_iff_re_im, map_zero] at hz hw ⊢961    simp [mul_re, mul_im, ← hz.2, ← hw.2, mul_pos hz.1 hw.1]962963scoped[ComplexOrder] attribute [instance] RCLike.toIsStrictOrderedRing964965lemma toPosMulReflectLT : PosMulReflectLT K where966  elim := by967    rintro ⟨x, hx⟩ y z hyz968    dsimp at *969    rw [RCLike.le_iff_re_im, map_zero, map_zero, eq_comm] at hx970    obtain ⟨r, rfl⟩ := ((is_real_TFAE x).out 3 1).1 hx.2971    simp only [RCLike.lt_iff_re_im (K := K), mul_re, ofReal_re, ofReal_im, zero_mul, sub_zero,972      mul_im, add_zero, mul_eq_mul_left_iff] at hyz ⊢973    refine ⟨lt_of_mul_lt_mul_of_nonneg_left hyz.1 <| by simpa using hx, hyz.2.resolve_right ?_⟩974    rintro rfl975    simp at hyz976977scoped[ComplexOrder] attribute [instance] RCLike.toPosMulReflectLT978979theorem toIsStrictOrderedModule : IsStrictOrderedModule ℝ K where980  smul_lt_smul_of_pos_left r hr a b hab := by981    simpa [RCLike.lt_iff_re_im (K := K), smul_re, smul_im, hr, hr.ne'] using hab982  smul_lt_smul_of_pos_right a ha r₁ r₂ hr := by983    obtain ⟨hare, haim⟩ := RCLike.lt_iff_re_im.1 ha984    simp_all [RCLike.lt_iff_re_im (K := K), smul_re, smul_im]985986scoped[ComplexOrder] attribute [instance] RCLike.toIsStrictOrderedModule987988theorem ofReal_mul_pos_iff (x : ℝ) (z : K) :989    0 < x * z ↔ (x < 0 ∧ z < 0) ∨ (0 < x ∧ 0 < z) := by990  simp only [pos_iff (K := K), neg_iff (K := K), re_ofReal_mul, im_ofReal_mul]991  obtain hx | hx | hx := lt_trichotomy x 0992  · simp only [mul_pos_iff, not_lt_of_gt hx, false_and, hx, true_and, false_or, mul_eq_zero, hx.ne,993      or_false]994  · simp only [hx, zero_mul, lt_self_iff_false, false_and, false_or]995  · simp only [mul_pos_iff, hx, true_and, not_lt_of_gt hx, false_and, or_false, mul_eq_zero,996      hx.ne', false_or]997998theorem ofReal_mul_neg_iff (x : ℝ) (z : K) :999    x * z < 0 ↔ (x < 0 ∧ 0 < z) ∨ (0 < x ∧ z < 0) := by1000  simpa only [mul_neg, neg_pos, neg_neg_iff_pos] using ofReal_mul_pos_iff x (-z)10011002lemma instPosMulReflectLE : PosMulReflectLE K where1003  elim a b c h := by1004    obtain ⟨a', ha1, ha2⟩ := pos_iff_exists_ofReal.mp a.21005    rw [← sub_nonneg]1006    #adaptation_note /-- 2025-03-29 need beta reduce for https://github.com/leanprover/lean4/issues/7717 -/1007    beta_reduce at h1008    rw [← ha2, ← sub_nonneg, ← mul_sub, le_iff_lt_or_eq] at h1009    rcases h with h | h1010    · rw [ofReal_mul_pos_iff] at h1011      exact le_of_lt <| h.rec (False.elim <| not_lt_of_gt ·.1 ha1) (·.2)1012    · exact ((mul_eq_zero_iff_left <| ofReal_ne_zero.mpr ha1.ne').mp h.symm).ge10131014scoped[ComplexOrder] attribute [instance] RCLike.instPosMulReflectLE10151016lemma instMulPosReflectLE : MulPosReflectLE K := PosMulReflectLE.toMulPosReflectLE10171018scoped[ComplexOrder] attribute [instance] RCLike.instMulPosReflectLE10191020end Order10211022section CleanupLemmas10231024local notation "reR" => @RCLike.re ℝ _1025local notation "imR" => @RCLike.im ℝ _1026local notation "IR" => @RCLike.I ℝ _1027local notation "normSqR" => @RCLike.normSq ℝ _10281029@[simp, rclike_simps]1030theorem re_to_real {x : ℝ} : reR x = x :=1031  rfl10321033@[simp, rclike_simps]1034theorem im_to_real {x : ℝ} : imR x = 0 :=1035  rfl10361037@[rclike_simps]1038theorem conj_to_real {x : ℝ} : conj x = x :=1039  rfl10401041@[simp, rclike_simps]1042theorem I_to_real : IR = 0 :=1043  rfl10441045@[simp, rclike_simps]1046theorem normSq_to_real {x : ℝ} : normSq x = x * x := by simp [RCLike.normSq]10471048@[simp]1049theorem ofReal_real_eq_id : @ofReal ℝ _ = id :=1050  rfl10511052end CleanupLemmas10531054section LinearMaps10551056/-- The real part in an `RCLike` field, as a linear map. -/1057noncomputable def reLm : K →ₗ[ℝ] ℝ :=1058  { re with map_smul' := smul_re }10591060@[simp, rclike_simps]1061theorem reLm_coe : (reLm : K → ℝ) = re :=1062  rfl10631064/-- The real part in an `RCLike` field, as a continuous linear map. -/1065noncomputable def reCLM : StrongDual ℝ K :=1066  reLm.mkContinuous 1 fun x => by1067    rw [one_mul]1068    exact abs_re_le_norm x10691070@[simp, rclike_simps, norm_cast]1071theorem reCLM_coe : ((reCLM : StrongDual ℝ K) : K →ₗ[ℝ] ℝ) = reLm :=1072  rfl10731074@[simp, rclike_simps]1075theorem reCLM_apply : ((reCLM : StrongDual ℝ K) : K → ℝ) = re :=1076  rfl10771078@[continuity, fun_prop]1079theorem continuous_re : Continuous (re : K → ℝ) :=1080  reCLM.continuous10811082/-- The imaginary part in an `RCLike` field, as a linear map. -/1083noncomputable def imLm : K →ₗ[ℝ] ℝ :=1084  { im with map_smul' := smul_im }10851086@[simp, rclike_simps]1087theorem imLm_coe : (imLm : K → ℝ) = im :=1088  rfl10891090/-- The imaginary part in an `RCLike` field, as a continuous linear map. -/1091noncomputable def imCLM : StrongDual ℝ K :=1092  imLm.mkContinuous 1 fun x => by1093    rw [one_mul]1094    exact abs_im_le_norm x10951096@[simp, rclike_simps, norm_cast]1097theorem imCLM_coe : ((imCLM : StrongDual ℝ K) : K →ₗ[ℝ] ℝ) = imLm :=1098  rfl10991100@[simp, rclike_simps]1101theorem imCLM_apply : ((imCLM : StrongDual ℝ K) : K → ℝ) = im :=1102  rfl11031104@[continuity, fun_prop]1105theorem continuous_im : Continuous (im : K → ℝ) :=1106  imCLM.continuous11071108/-- Conjugate as an `ℝ`-algebra equivalence -/1109def conjAe : K ≃ₐ[ℝ] K :=1110  { conj with1111    invFun := conj1112    left_inv := conj_conj1113    right_inv := conj_conj1114    commutes' := conj_ofReal }11151116@[simp, rclike_simps]1117theorem conjAe_coe : (conjAe : K → K) = conj :=1118  rfl11191120/-- Conjugate as a linear isometry -/1121noncomputable def conjLIE : K ≃ₗᵢ[ℝ] K :=1122  ⟨conjAe.toLinearEquiv, norm_conj⟩11231124@[simp, rclike_simps]1125theorem conjLIE_apply : (conjLIE : K → K) = conj :=1126  rfl11271128/-- Conjugate as a continuous linear equivalence -/1129noncomputable def conjCLE : K ≃L[ℝ] K :=1130  @conjLIE K _11311132@[simp, rclike_simps]1133theorem conjCLE_coe : (@conjCLE K _).toLinearEquiv = conjAe.toLinearEquiv :=1134  rfl11351136@[simp, rclike_simps]1137theorem conjCLE_apply : (conjCLE : K → K) = conj :=1138  rfl11391140instance (priority := 100) : ContinuousStar K :=1141  ⟨conjLIE.continuous⟩11421143@[continuity]1144theorem continuous_conj : Continuous (conj : K → K) :=1145  continuous_star11461147/-- The `ℝ → K` coercion, as an algebra map. -/1148noncomputable def ofRealAm : ℝ →ₐ[ℝ] K :=1149  Algebra.ofId ℝ K11501151@[simp, rclike_simps]1152theorem ofRealAm_coe : (ofRealAm : ℝ → K) = ofReal :=1153  rfl11541155variable (K) in1156/-- The `ℝ → K` coercion, as a ⋆-algebra map. -/1157noncomputable def ofRealStarAlgHom : ℝ →⋆ₐ[ℝ] K := .ofId ℝ K11581159@[simp] theorem coe_ofRealStarAlgHom : (ofRealStarAlgHom K : ℝ → K) = ofReal := rfl1160@[simp] lemma toAlgHom_ofRealStarAlgHom : (ofRealStarAlgHom K).toAlgHom = ofRealAm := rfl11611162/-- The ℝ → K coercion, as a linear isometry -/1163noncomputable def ofRealLI : ℝ →ₗᵢ[ℝ] K where1164  toLinearMap := ofRealAm.toLinearMap1165  norm_map' := norm_ofReal11661167@[simp, rclike_simps]1168theorem ofRealLI_apply : (ofRealLI : ℝ → K) = ofReal :=1169  rfl11701171/-- The `ℝ → K` coercion, as a continuous linear map -/1172noncomputable def ofRealCLM : ℝ →L[ℝ] K :=1173  ofRealLI.toContinuousLinearMap11741175@[simp, rclike_simps]1176theorem ofRealCLM_coe : (@ofRealCLM K _ : ℝ →ₗ[ℝ] K) = ofRealAm.toLinearMap :=1177  rfl11781179@[simp, rclike_simps]1180theorem ofRealCLM_apply : (ofRealCLM : ℝ → K) = ofReal :=1181  rfl11821183@[continuity, fun_prop]1184theorem continuous_ofReal : Continuous (ofReal : ℝ → K) :=1185  ofRealLI.continuous11861187@[continuity]1188theorem continuous_normSq : Continuous (normSq : K → ℝ) :=1189  (continuous_re.mul continuous_re).add (continuous_im.mul continuous_im)11901191theorem lipschitzWith_ofReal : LipschitzWith 1 (ofReal : ℝ → K) :=1192  ofRealLI.lipschitz11931194lemma lipschitzWith_re : LipschitzWith 1 (re (K := K)) := by1195  intro x y1196  simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]1197  calc ‖re x - re y‖ₑ1198  _ = ‖re (x - y)‖ₑ := by rw [map_sub re x y]1199  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_re_le_norm (x - y)12001201lemma lipschitzWith_im : LipschitzWith 1 (im (K := K)) := by1202  intro x y1203  simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]1204  calc ‖im x - im y‖ₑ1205  _ = ‖im (x - y)‖ₑ := by rw [map_sub im x y]1206  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_im_le_norm (x - y)12071208/-- The canonical map between `RCLike` types. It maps `x : 𝕜` to `re x + im x * I`. -/1209@[simps] def map (𝕜 𝕜' : Type*) [RCLike 𝕜] [RCLike 𝕜'] : 𝕜 →L[ℝ] 𝕜' where1210  toFun x := re x + im x * (I : 𝕜')1211  map_add' _ _ := by simp only [map_add, add_mul]; ring1212  map_smul' _ _ := by simp [real_smul_eq_coe_mul, mul_assoc]12131214@[simp] theorem map_same_eq_id : map K K = .id ℝ K := by ext; simp12151216@[simp] theorem map_to_real : map K ℝ = reCLM := by1217  ext; simp only [map_apply, I, mul_zero, add_zero]; rfl12181219@[simp] theorem map_from_real : map ℝ K = ofRealCLM := by ext; simp12201221open scoped ComplexOrder in1222lemma instOrderClosedTopology : OrderClosedTopology K where1223  isClosed_le' := by1224    conv in _ ≤ _ => rw [RCLike.le_iff_re_im]1225    simp_rw [Set.setOf_and]1226    refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_) <;> fun_prop12271228scoped[ComplexOrder] attribute [instance] RCLike.instOrderClosedTopology12291230end LinearMaps12311232/-!1233### ℝ-dependent results12341235Here we gather results that depend on whether `K` is `ℝ`.1236-/1237section CaseSpecific12381239lemma im_eq_zero (h : I = (0 : K)) (z : K) : im z = 0 := by1240  rw [← re_add_im z, h]1241  simp12421243/-- The natural isomorphism between `𝕜` satisfying `RCLike 𝕜` and `ℝ` when `RCLike.I = 0`. -/1244@[simps]1245def realRingEquiv (h : I = (0 : K)) : K ≃+* ℝ where1246  toFun := re1247  invFun := (↑)1248  left_inv x := by nth_rw 2 [← re_add_im x]; simp [h]1249  right_inv := ofReal_re1250  map_add' := map_add re1251  map_mul' := by simp [im_eq_zero h]12521253/-- The natural `ℝ`-linear isometry equivalence between `𝕜` satisfying `RCLike 𝕜` and `ℝ` when1254`RCLike.I = 0`. -/1255@[simps]1256noncomputable def realLinearIsometryEquiv (h : I = (0 : K)) : K ≃ₗᵢ[ℝ] ℝ where1257  map_smul' := smul_re1258  norm_map' z := by rw [← re_add_im z]; simp [-re_add_im, h]1259  __ := realRingEquiv h12601261end CaseSpecific12621263lemma norm_le_im_iff_eq_I_mul_norm {z : K} :1264    ‖z‖ ≤ im z ↔ z = I * ‖z‖ := by1265  obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := K)1266  · simp [h, im_eq_zero]1267  · have : (I : K) ≠ 0 := fun _ ↦ by simp_all1268    rw [← mul_right_inj' (neg_ne_zero.mpr this)]1269    convert! norm_le_re_iff_eq_norm (z := -I * z) using 21270    all_goals simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]12711272lemma im_le_neg_norm_iff_eq_neg_I_mul_norm {z : K} :1273    im z ≤ -‖z‖ ↔ z = -(I * ‖z‖) := by1274  simpa [neg_eq_iff_eq_neg, le_neg] using norm_le_im_iff_eq_I_mul_norm (z := -z)12751276end RCLike12771278namespace AddChar1279variable {G : Type*} [Finite G]12801281lemma inv_apply_eq_conj [AddLeftCancelMonoid G] (ψ : AddChar G K) (x : G) : (ψ x)⁻¹ = conj (ψ x) :=1282  RCLike.inv_eq_conj <| norm_apply _ _12831284lemma map_neg_eq_conj [AddCommGroup G] (ψ : AddChar G K) (x : G) : ψ (-x) = conj (ψ x) := by1285  rw [map_neg_eq_inv, inv_apply_eq_conj]12861287end AddChar12881289section12901291/-- A mixin over a normed field, saying that the norm field structure is the same as `ℝ` or `ℂ`.1292To endow such a field with a compatible `RCLike` structure in a proof, use1293`letI := IsRCLikeNormedField.rclike 𝕜`. -/1294class IsRCLikeNormedField (𝕜 : Type*) [hk : NormedField 𝕜] : Prop where1295  out : ∃ h : RCLike 𝕜, hk = h.toNormedField12961297instance (priority := 100) (𝕜 : Type*) [h : RCLike 𝕜] : IsRCLikeNormedField 𝕜 := ⟨⟨h, rfl⟩⟩12981299/-- A copy of an `RCLike` field in which the `NormedField` field is adjusted to be become defeq1300to a propeq one. -/1301@[implicit_reducible]1302noncomputable def RCLike.copy_of_normedField {𝕜 : Type*} (h : RCLike 𝕜) (hk : NormedField 𝕜)1303    (h'' : hk = h.toNormedField) : RCLike 𝕜 where1304  __ := hk1305  toPartialOrder := h.toPartialOrder1306  toDecidableEq := h.toDecidableEq1307  complete := by subst h''; exact h.complete1308  lt_norm_lt := by subst h''; exact h.lt_norm_lt1309  -- star fields1310  star := (@StarMul.toInvolutiveStar _ (_) (@StarRing.toStarMul _ (_) h.toStarRing)).star1311  star_involutive := by subst h''; exact h.star_involutive1312  star_mul := by subst h''; exact h.star_mul1313  star_add := by subst h''; exact h.star_add1314  -- algebra fields1315  smul := (@Algebra.toSMul _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra)).smul1316  algebraMap :=1317  { toFun := @Algebra.algebraMap _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra)1318    map_one' := by subst h''; exact h.algebraMap.map_one'1319    map_mul' := by subst h''; exact h.algebraMap.map_mul'1320    map_zero' := by subst h''; exact h.algebraMap.map_zero'1321    map_add' := by subst h''; exact h.algebraMap.map_add' }1322  commutes' := by subst h''; exact h.commutes'1323  smul_def' := by subst h''; exact h.smul_def'1324  norm_smul_le := by subst h''; exact h.norm_smul_le1325  -- RCLike fields1326  re := by subst h''; exact h.re1327  im := by subst h''; exact h.im1328  I := h.I1329  I_re_ax := by subst h''; exact h.I_re_ax1330  I_mul_I_ax := by subst h''; exact h.I_mul_I_ax1331  re_add_im_ax := by subst h''; exact h.re_add_im_ax1332  ofReal_re_ax := by subst h''; exact h.ofReal_re_ax1333  ofReal_im_ax := by subst h''; exact h.ofReal_im_ax1334  mul_re_ax := by subst h''; exact h.mul_re_ax1335  mul_im_ax := by subst h''; exact h.mul_im_ax1336  conj_re_ax := by subst h''; exact h.conj_re_ax1337  conj_im_ax := by subst h''; exact h.conj_im_ax1338  conj_I_ax := by subst h''; exact h.conj_I_ax1339  norm_sq_eq_def_ax := by subst h''; exact h.norm_sq_eq_def_ax1340  mul_im_I_ax := by subst h''; exact h.mul_im_I_ax1341  le_iff_re_im := by subst h''; exact h.le_iff_re_im13421343/-- Given a normed field `𝕜` satisfying `IsRCLikeNormedField 𝕜`, build an associated `RCLike 𝕜`1344structure on `𝕜` which is definitionally compatible with the given normed field structure. -/1345@[implicit_reducible]1346noncomputable def IsRCLikeNormedField.rclike (𝕜 : Type*)1347    [hk : NormedField 𝕜] [h : IsRCLikeNormedField 𝕜] : RCLike 𝕜 := by1348  choose p hp using h.out1349  exact p.copy_of_normedField hk hp13501351end13521353namespace LinearIsometryEquiv1354variable {𝕜 V W G : Type*} [RCLike 𝕜] [SeminormedAddCommGroup V] [Module 𝕜 V]1355  [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G]13561357/-- Left scalar multiplication of a unit with norm one and a linear isometric equivalence,1358as a linear isometric equivalence. -/1359instance : SMul (unitary 𝕜) (V ≃ₗᵢ[𝕜] W) where smul α e :=1360  { __ := Unitary.toUnits α • e.toLinearEquiv1361    norm_map' _ := by simp [norm_smul] }13621363@[simp] theorem smul_apply (e : V ≃ₗᵢ[𝕜] W) (α : unitary 𝕜) (x : V) :1364    (α • e) x = (α : 𝕜) • e x := rfl13651366theorem symm_smul_apply (e : V ≃ₗᵢ[𝕜] W) (α : unitary 𝕜) (x : W) :1367    (α • e).symm x = (↑α⁻¹ : 𝕜) • e.symm x := rfl13681369@[simp] theorem symm_units_smul (e : G ≃ₗᵢ[𝕜] W) (α : unitary 𝕜) :1370    (α • e).symm = α⁻¹ • e.symm := by ext; simp [symm_smul_apply]13711372@[simp] theorem toLinearEquiv_smul (e : V ≃ₗᵢ[𝕜] W) (α : unitary 𝕜) :1373    (α • e).toLinearEquiv = Unitary.toUnits α • e.toLinearEquiv := rfl13741375@[simp] theorem toContinuousLinearEquiv_smul (e : G ≃ₗᵢ[𝕜] W) (α : unitary 𝕜) :1376    (α • e).toContinuousLinearEquiv = Unitary.toUnits α • e.toContinuousLinearEquiv := rfl13771378theorem smul_trans (α : unitary 𝕜) (e : V ≃ₗᵢ[𝕜] G) (f : G ≃ₗᵢ[𝕜] W) :1379    (α • e).trans f = α • (e.trans f) := by ext; simp13801381theorem trans_smul (α : unitary 𝕜) (e : V ≃ₗᵢ[𝕜] G) (f : G ≃ₗᵢ[𝕜] W) :1382    e.trans (α • f) = α • (e.trans f) := by ext; simp13831384end LinearIsometryEquiv