[Merged by Bors] - feat: norm estimates for various operators in linear algebra #12150
Conversation
sgouezel
added
awaiting-review
| /-- An auxiliary instance to be able to just state the fact that the norm of `smulRightL` makes | ||
| sense. This shouldn't be needed. TODO: fix typeclass inference. -/ | ||
| def seminormedAddCommGroup_aux_for_smulRightL : | ||
| SeminormedAddCommGroup ((E →L[𝕜] 𝕜) →L[𝕜] Fₗ →L[𝕜] E →L[𝕜] Fₗ) := |
There was a problem hiding this comment.
This isn't a max recursion depth issue for synthesis? (Not at a computer)
There was a problem hiding this comment.
My guess is it's like https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nested.20linear.20map.20norm.20failure/near/423226292 (synthPending issue)
There was a problem hiding this comment.
Sorry. Yes that was what I was thinking of. Can you just bump it locally?
There was a problem hiding this comment.
I don't know how to do that (there are no examples throughout mathlib, if I can tell correctly).
There was a problem hiding this comment.
If you mean set_option synthInstance.maxHeartbeats 0 in, it doesn't work here.
There was a problem hiding this comment.
There is a TODO in the core code which limits the number of pending instance problems when solving for another. It is set to a very small number but bumping it in core broke quite a bit.
I don't think we are getting any kind of help on this from core in the short term so we should just figure out here how we want to handle it.
The same problem pops up in Analysis.NormedSpace.OperatorNorm where some letI's helped things along.
Is there anyway to contain the new local instances to the declarations they are needed for?
There was a problem hiding this comment.
Instead of having a local instance, one can do as follows:
lemma norm_smulRightL_le :
letI := seminormedAddCommGroup_aux_for_smulRightL 𝕜 E Fₗ
‖smulRightL 𝕜 E Fₗ‖ ≤ 1 :=It's probably a better solution, let me switch to it.
|
I've created an issue in the core repo about this. Can you reference it in the comments? If it ever gets resolved, we can streamline here. |
|
I've referenced the issue in the comments. |
|
Thanks! bors delegate+ |
|
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
github-actions
bot
added
ready-to-merge
There is a technical issue: I need to register two local instances to be even able to state the norm estimates. The issue is typeclass inference getting stuck in complicated types of linear maps...
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
There is a technical issue: I need to register two local instances to be even able to state the norm estimates. The issue is typeclass inference getting stuck in complicated types of linear maps...
There is a technical issue: I need to register two local instances to be even able to state the norm estimates. The issue is typeclass inference getting stuck in complicated types of linear maps...
There is a technical issue: I need to register two local instances to be even able to state the norm estimates. The issue is typeclass inference getting stuck in complicated types of linear maps...
There is a technical issue: I need to register two local instances to be even able to state the norm estimates. The issue is typeclass inference getting stuck in complicated types of linear maps...