[Merged by Bors] - feat(data/complex/is_R_or_C): add typeclass for real or complex

[dupuisf]

---

This PR defines the typeclass is_R_or_C intended to have only two instances:
ℝ and ℂ. It is meant for definitions and theorems which hold for both the
real and the complex case, such as inner products and Hilbert spaces. Its API
follows closely that of ℂ.

[fpvandoorn]

Nice!

I think (eventually) we want to move away from using complex.conj (and other operations), and use the conj that has as argument is_R_or_C. I think it works analogously to using has_mul.mul everywhere, and never using nat.mul. The fact that this class has only one interesting instance that uses conj doesn't really matter.

[cipher1024]

I'm fairly ignorant of the application here but I'm wondering, is there a reason to not define the class as:

class is_R_or_C (K : Type) := 
(from_R : R -> K)
(to_C : K -> C)
(to_C_from_R : \forall x : R, to_C (from_R x) = coe x)

and derive the rest from that? That could probably be generalized into an interval between types and applied to other situations like nat and int

[fpvandoorn]

@cipher1024 I don't think you can define/proof the current fields of is_R_or_C from your suggestion.

[dupuisf]

@cipher1024 Right -- more precisely, I don't see how to avoid being able to prove things like ∃ x, x^2 = -1 this way.

[dupuisf]

@fpvandoorn For conj, I think it might be a good idea to have a class like has_star or something, which would be used for complex conjugation, adjoints of linear operators, etc.

[jalex-stark]

Suggested change

	(@is_R_or_C.ext_iff K _ _ _ (conj (𝓚 r)) (𝓚 r)).mpr $ by simp
	by { rw ext_iff, simp only [of_real_im, conj_im, eq_self_iff_true, conj_re, and_self, neg_zero] }

squeezing this simp makes the file compile a bit faster. I don't have a profiler output, but the orange bar hangs around noticeably long with a raw simp and goes away immediately with this simp only

[jalex-stark]

Actually the proofs of conj_neg_I and conj_conj take a while, too. Maybe we've made a bad choice with our simp normal form?

[dupuisf]

I haven't been too careful with the simp lemmas, I basically left things the way they were in complex.lean.

[bryangingechen]

Should the file be named is_R_or_C.lean instead of R_or_C.lean too?

[dupuisf]

@fpvandoorn Thanks for the suggestions! Regarding norm_cast, it doesn't seem to work since the "coercions" used here aren't real coercions, they're just a regular function. In fact many of these lemmas were initially copy/pasted from complex.lean and I had to remove the norm_cast attribute since I was getting errors about the lhs not containing any coercions.

[sgouezel]

I am a little bit confused about the intended applications of this file. For instance, in the file analysis/normed_space/hahn_banach, we have Hahn-Banach theorem over the reals and over the complexes, and we introduce a specific typeclass to formulate the theorems for both (where the complex instance is deduced from the real instance and a trick). Do I understand correctly that the current typeclass is_R_or_C could not be used instead of this specific typeclass? In the same way, an important property of reals and complexes is that the mean value inequality holds (where the complex one is again deduced from the real one) -- could one use is_R_or_C to state this, or will we need to introduce yet another typeclass?

[dupuisf]

@sgouezel The main application I have in mind is defining the complex inner product, and other cases in which the real case follows directly from the complex case by replacing re by identity, im by zero, etc. For Hahn-Banach, I don't immediately see a reason why it wouldn't work, though one would have to port things like linear_map.extend_to_ℂ to linear_map.extend_to_ℝ_or_ℂ, etc. But in this case the benefits might be more limited, since one derives the complex case from the real one and not the other way around.

[sgouezel]

ok, thanks for the clarification. It might be a good idea to explain this in the file-level docstring, and to sketch an application there.

[dupuisf]

I've added some more details to the file-level docstring, and changed the normed_field requirement to nondiscrete_normed_field, since it looks like that will be needed in some applications.

[dupuisf]

I didn't go into too much detail regarding the applications, since I plan to PR inner products based on this fairly soon.

[fpvandoorn]

LGTM

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests