feat(temperature): PositiveTemperature refactor#976
feat(temperature): PositiveTemperature refactor#976ichxorya wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
|
Hey, when you are ready for this to be reviewed, could you unmark it as a draft? |
Yes I think it is ready, but I marked as draft since it's not ready to be merge. Can you please review this section first? I'd like to add the rest of the original Basic.lean but it would be too lengthy for now. |
|
Could we split the |
jstoobysmith
added
t-thermodynamics
|
Do you actually use the results in the PosReal file in this PR? If so this file should be moved to the |
I guess we can, but since the beginning I though "Basic" was to store "base" data types. It would be done right away! Also, the PosReal type is defined for easier notation of R>0. I would move it to Math folder if it suits the project better! |
This is correct, it does in general store the |
…table directories (with minor reformat)
Thank you, I have pushed the new code to my PR following my understanding of your suggestion. |
| @@ -0,0 +1,16 @@ | |||
| /- | |||
There was a problem hiding this comment.
This should be in the Mathematics file
There was a problem hiding this comment.
I have received the comments and will work on them right away. But first, isnt this is the mathematics directory that i need my file to be moved to?
There was a problem hiding this comment.
Sorry this was an old message. Thanks - yep you have already done this.
| It wraps a nonnegative real number, which is the `val` field of the structure. | ||
| -/ | ||
| structure Temperature where | ||
| /-- The nonnegative real value of the temperature. -/ |
There was a problem hiding this comment.
Will need this doc-string for the linters
| /-! | ||
| ## Extensionality for `Temperature` | ||
| -/ | ||
| namespace Temperature |
There was a problem hiding this comment.
no need to end and restart namespace here
| /-! | ||
| ## Extensionality for `PositiveTemperature` | ||
| -/ | ||
| namespace PositiveTemperature |
There was a problem hiding this comment.
Again no need to to end and restart namespaces
| noncomputable def ofβ (β : ℝ>0) : PositiveTemperature := | ||
| ⟨ | ||
| ⟨1 / (kB * β), by | ||
| apply div_nonneg |
There was a problem hiding this comment.
will the tactic positivity work here?
| exact h_T₁_le_T₂ | ||
|
|
||
| /-- The thermodynamic beta strictly reverses strict inequalities. -/ | ||
| lemma β_strictAnti {T₁ T₂ : PositiveTemperature} : T₁ < T₂ ↔ β T₂ < β T₁ := by |
There was a problem hiding this comment.
use [StrictAnti](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Monotone/Defs.html#StrictAnti) directly here, and similar for the above?
2 participants
At this first commit, I would follow the suggestion of @jstoobysmith to break the PR down into pieces. Hopefully this could be reviewed as a passing commit 😄
However, note that at this point, the Basic.lean file only contain:
For the rest (derivatives, limits, ect.), I have also proved them following the PositiveTemperature refactor here (https://github.com/SEhumantics/PhysLean/tree/feat/nghiabt/postemp/PhysLean/Thermodynamics/Temperature). However, I can only commit more until further acceptance from maintainer revisions!
Referred issues: #861 #860 - #892 (directly dependent on the Beta and Inverse Beta functions)