Zulip Chat Archive

Stream: new members

Topic: question on is_R_or_C


Monica Omar (Feb 06 2023 at 09:32):

When dealing with is_R_or_C 𝕜, is there a way to "separate" it in the proof? Like proving it in the case of 𝕜 = ℝ and in the case of 𝕜 = ℂ?

Yaël Dillies (Feb 06 2023 at 09:56):

Not really, no. That's the entire point of is_R_or_C in the first place : avoid proving every real and complex result separately.

Ruben Van de Velde (Feb 06 2023 at 10:08):

You might be able to case on I = 0; not sure if that would help

Eric Wieser (Feb 06 2023 at 12:48):

Yes, that's docs#is_R_or_C.I_mul_I_ax

Jireh Loreaux (Feb 06 2023 at 16:25):

I think a key question is: why do you want to separate it? I'm not saying there are no possible reasons, but often it's the case that there is a better way to work with is_R_or_C.

Monica Omar (Feb 07 2023 at 12:14):

For example, if I want to show that any self-adjoint linear map T has the property: (∀ x, ⟪x, T x⟫ = 0) ↔ T = 0, then I wanted to see if I can use inner_map_self_eq_zero for the complex case, instead of copying the proof.

Eric Wieser (Feb 07 2023 at 12:48):

Arguably docs#inner_map_self_eq_zero should be stated for is_R_or_C in the first place

Monica Omar (Feb 07 2023 at 13:56):

you need the self-adjoint property for it to work over the reals though

Eric Wieser (Feb 07 2023 at 14:17):

Can you give the full statement of what you want to prove?

Kyle Miller (Feb 07 2023 at 14:32):

Eric Wieser said:

Arguably docs#inner_map_self_eq_zero should be stated for is_R_or_C in the first place

Isn't that false over R? For example, have V be R^2 and T be rotation by a quarter turn.

Monica Omar (Feb 07 2023 at 14:49):

Eric Wieser said:

Can you give the full statement of what you want to prove?

Here ya go

import analysis.inner_product_space.symmetric

variables {𝕜 E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]

local notation `⟪`x`,`y`⟫` := @inner 𝕜 _ _ x y

example (T : E →ₗ[𝕜] E) (hT : T.is_symmetric) :
  (∀ x, ⟪x, T x⟫ = 0) ↔ T = 0 :=
sorry

Jireh Loreaux (Feb 07 2023 at 16:04):

You could prove something like this that works over is_R_or_C.

import analysis.inner_product_space.symmetric

variables {𝕜 V : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 V]
open is_R_or_C

local notation `⟪` x `, ` y `⟫` := @inner 𝕜 _ _ x y

lemma linear_map.is_symmetric.inner_map_polarization {T : V →ₗ[𝕜] V} (hT : T.is_symmetric)
  (x y : V) :
  ⟪ T x, y ⟫ = (⟪T (x + y) , x + y⟫ - ⟪T (x - y) , x - y⟫ -
    I * ⟪T (x + (I : 𝕜) • y) , x + (I : 𝕜) • y⟫ +
    I * ⟪T (x - (I : 𝕜) • y), x - (I : 𝕜) • y ⟫) / 4 :=
begin
  rcases @I_mul_I_ax 𝕜 _ with (h | h),
  { simp only [h, map_add, map_sub, add_zero, zero_mul, sub_zero],
    simp only [inner_add_left, inner_add_right, inner_sub_left, inner_sub_right],
    rw [hT y x, ←inner_conj_sym y (T x), eq_conj_iff_re.mpr _],
    { ring, },
    { nth_rewrite 1 ←re_add_im (⟪T x, y⟫),
      rw [h, mul_zero, add_zero] } },
  { simp only [map_add, map_sub, inner_add_left, inner_add_right, linear_map.map_smul,
             inner_smul_left, inner_smul_right, is_R_or_C.conj_I, ←pow_two, sq, h,
             inner_sub_left, inner_sub_right, mul_add, ←mul_assoc, mul_neg, neg_neg,
             sub_neg_eq_add, one_mul, neg_one_mul, mul_sub, sub_sub],
    ring, }
end

example {T : V →ₗ[𝕜] V} (hT : T.is_symmetric) :
  (∀ x, ⟪T x, x⟫ = 0) ↔ T = 0 :=
begin
  refine ⟨λ h, _, λ h, by simp only [h, linear_map.zero_apply, inner_zero_left, forall_const]⟩,
  ext x,
  rw [linear_map.zero_apply, ←inner_self_eq_zero, hT.inner_map_polarization],
  simp only [h _],
  ring,
end

Monica Omar (Feb 07 2023 at 16:05):

Jireh Loreaux said:

You could prove something like this that works over is_R_or_C.

import analysis.inner_product_space.symmetric

variables (𝕜 V : Type*) [is_R_or_C 𝕜] [inner_product_space 𝕜 V]
open is_R_or_C

local notation `⟪` x `, ` y `⟫` := @inner 𝕜 _ _ x y

lemma is_symmetric.inner_map_polarization (T : V →ₗ[𝕜] V) (x y : V) (hT : T.is_symmetric):
  ⟪ T x, y ⟫ = (⟪T (x + y) , x + y⟫ - ⟪T (x - y) , x - y⟫ -
    I * ⟪T (x + (I : 𝕜) • y) , x + (I : 𝕜) • y⟫ +
    I * ⟪T (x - (I : 𝕜) • y), x - (I : 𝕜) • y ⟫) / 4 :=
begin
  rcases @I_mul_I_ax 𝕜 _ with (h | h),
  { simp only [h, map_add, map_sub, add_zero, zero_mul, sub_zero],
    simp only [inner_add_left, inner_add_right, inner_sub_left, inner_sub_right],
    rw [hT y x, ←inner_conj_sym y (T x), eq_conj_iff_re.mpr _],
    { ring, },
    { nth_rewrite 1 ←re_add_im (⟪T x, y⟫),
      rw [h, mul_zero, add_zero] } },
  { simp only [map_add, map_sub, inner_add_left, inner_add_right, linear_map.map_smul,
             inner_smul_left, inner_smul_right, is_R_or_C.conj_I, ←pow_two, sq, h,
             inner_sub_left, inner_sub_right, mul_add, ←mul_assoc, mul_neg, neg_neg,
             sub_neg_eq_add, one_mul, neg_one_mul, mul_sub, sub_sub],
    ring, }
end

yo! I was legit in the process of doing this - haha!

Jireh Loreaux (Feb 07 2023 at 16:26):

(edited the code above with a proof of your result)

Jireh Loreaux (Feb 07 2023 at 16:33):

Actually, if you want to PR the results above, that would be nice.

Monica Omar (Feb 07 2023 at 16:35):

yeah! sounds good. i'll do that just now. i'll have to give your code the credit tho lol

Jireh Loreaux (Feb 07 2023 at 16:48):

no need, don't worry about it.


Last updated: Dec 20 2023 at 11:08 UTC