EVMPR theorem twoState_helmholtzFreeEnergy_eq - #1474
Conversation
…ified further if T \neq 0, but I left it as a general result
|
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 |
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Hi @korolrom This is a great first PR. I've added some comments (some of them are a bit pedantic). If you could have a go at addressing them, this would be great.
Let me know if you have any questions :).
| lemma twoState_helmholtzFreeEnergy_eq | ||
| (E₀ E₁ : ℝ) (T : Temperature) : |
There was a problem hiding this comment.
Could probably collapse this to one line.
| rw [helmholtzFreeEnergy, twoState_partitionFunction_apply] | ||
| rw [show (T.val : ℝ) = T.toReal by rfl] | ||
| rw [hE0, hE1] |
There was a problem hiding this comment.
May worth be putting this into a single large rw [...]
| rw [Real.log_exp,Temperature.β_toReal] | ||
| simp only [div_eq_mul_inv, one_mul, inv_inv] |
There was a problem hiding this comment.
Could you combine the things in the rw with the things in the simp so e.g.
simp only [Real.log_exp,Temperature.β_toReal, div_eq_mul_inv, one_mul, inv_inv]
(Will have to check if this actually works).
jstoobysmith
added
the
awaiting-author
|
Also doing the T \neq 0 case would be a great future PR! |
|
Thank you for the ultrafast review! @jstoobysmith I am happy to also add the T \neq 0 case. Would that be another lemma? Feels like not "big" enough to warrant its own lemma :) |
|
This looks much better - and looks almost there! Some of the linters are now failing though. Would you mind fixing these (some instructions to running them locally here, but can also just rely on github workflows. The ones I can see now are about line lengths. Regarding T \neq 0, if it is a large simplification then it probably does warrant its own lemma, but probably best to keep that to a separate Pull request (PR). |
|
Ok, I split the line and I tried to run the linter locally but there are a lot of errors and warnings from I ready to create another PR for the T\neq 0 result once this one is merged! |
2 participants
This is my first contribution to physlib.
The result can be simplified further under hypothesis T \neq 0, but I left it as a more general result including zero temperature.