feat: Refactor downstream use away from FieldStrengthMatrix#1288
Conversation
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
|
@NicolaBernini I think this now has a merge conflict with your other PR |
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Hi @jstoobysmith should be fixed now |
| -/ | ||
|
|
||
| /-- The field-strength component obtained by evaluating both tensor indices. -/ | ||
| noncomputable abbrev fieldStrengthComponent {d} (A : ElectromagneticPotential d) (x : SpaceTime d) |
There was a problem hiding this comment.
This I'm not so sure about as it seems to be just a rewriting of fieldStrengthMatrix. I think what is needed here is to write the results in terms of toField {toFieldStrength A [mu] [nu]} (not quite the right syntax but hopefully obvious what I mean).
I think the idea is to base everything more concretely on toFieldStrength A rather than introducing a new version of it.
jstoobysmith
added
the
awaiting-author
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
| /-- The horizontal position `x₁` of the support mass. -/ | ||
| supportPosition : ℝ | ||
| /-- The angle `φ` that the string makes with the vertical. -/ | ||
| angle : ℝ |
There was a problem hiding this comment.
I think I would make this [Real.Angle](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.html#Real.Angle) rather then Real.
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
|
(Think we should remove the sliding pendulum changes from this PR) |
2 participants
Overview
feat: Refactor downstream use away from FieldStrengthMatrix