!4#4280 Analysis.InnerProductSpace.Basic

Stream: mathlib4

[Jireh Loreaux]

In porting this file I ran across a "cannot find synthesization order" error on attribute [local instance] toNorm where the toNorm has type:

InnerProductSpace.Core.toNorm.{u_1, u_2} {𝕜 : Type u_1} {F : Type u_2} [inst✝ : IsROrC 𝕜] [inst✝¹ : AddCommGroup F]
  [inst✝² : Module 𝕜 F] [c : Core 𝕜 F] : Norm F

The error says:

cannot find synthesization order for instance @toNorm with type
  {𝕜 : Type u_1} →
    {F : Type u_2} → [inst : IsROrC 𝕜] → [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → [c : Core 𝕜 F] → Norm F
all remaining arguments have metavariables:
  IsROrC ?𝕜
  @Module ?𝕜 F DivisionSemiring.toSemiring AddCommGroup.toAddCommMonoid
  @Core ?𝕜 F ?inst✝ inst✝¹ ?inst✝¹

The problem is that 𝕜 is a metavariable, but since we're looking for as isROrC 𝕜 instance, so there are only two options and enumerating all of them is not the problem it usually is. What do I do here? Am I supposed to mark something as a SemiOutParam @Gabriel Ebner ?

[Gabriel Ebner]

Yes, since there are only the two instances IsROrC ℝ and IsROrC ℂ it's safe to mark it IsROrC (K : semiOutParam Type).

[Gabriel Ebner]

It would only be an issue if we had an instance like [ConditionallyCompleteLinearOrderedField K] : IsROrC K.

[Jireh Loreaux]

And I mark this on the declaration docs4#IsROrC itself right, not when setting up variables or in the declaration toNorm?

[Gabriel Ebner]

Yes, that should be on IsROrC directly.

[Eric Wieser]

I think this definition is only used internally anyway, so presumably it could just be set up locally somehow?

[Eric Wieser]

Which is to say, inner_product_space itself no longer relies on:

Gabriel Ebner said:

Yes, since there are only the two instances IsROrC ℝ and IsROrC ℂ it's safe to mark it IsROrC (K : semiOutParam Type).

[Jireh Loreaux]

ah shoot, I just realized I was supposed to wait for #19058 to start this. My bad. I'll just keep my edits locally as I'm about half way done. @Moritz Doll please let me know when that gets merged and then I'll pull in the new version from mathport.

[Jireh Loreaux]

Moritz said I should just continue with porting this file. I have just pushed changes and there are only a few errors left.

1. In one case I had to increase the synthInstance.maxHeartbeats to 80000 :grimacing:
2. toSesqForm is broken and I don't really understand why, but it seems to be something to do with applying LinearIsometryEquiv.toContinuousLinearEquiv to (ContinuousLinearMap.flipₗᵢ' E E' 𝕜 (starRingEnd 𝕜) (RingHom.id 𝕜))
3. I haven't yet edited names or anything, I've only dealt with errors.

Help welcome unless I say otherwise. I'll be asleep for 8 hours or so.

[Jireh Loreaux]

I'm locking this file again to work on it.

[Jireh Loreaux]

This is green, but there are two places where I had to increase maxHeartbeats by a lot. We should probably deal with these, but I need help because I couldn't figure it out.