question on is_R_or_C

Stream: new members

[Monica Omar]

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]

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]

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

[Eric Wieser]

Yes, that's docs#is_R_or_C.I_mul_I_ax

[Jireh Loreaux]

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]

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]

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

[Monica Omar]

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

[Eric Wieser]

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

[Kyle Miller]

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]

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]

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]

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]

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

[Jireh Loreaux]

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

[Monica Omar]

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

[Jireh Loreaux]

no need, don't worry about it.