feat(temperature): PositiveTemperature refactor by ichxorya · Pull Request #976 · leanprover-community/physlib

ichxorya · 2026-03-05T11:55:37Z

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:

Temperature and PositiveTemperature definitions: type conversions, ext lemma, linear order and relevant order/comparison lemmas.
Beta and Inverse Beta (ofBeta) was moved from Temperature to PositiveTemperature, with additional lemmas in their antimonotonicity (T1 > T2 <=> Beta T1 < Beta T2, ect.)

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)

jstoobysmith · 2026-03-06T11:40:24Z

Hey, when you are ready for this to be reviewed, could you unmark it as a draft?

ichxorya · 2026-03-06T11:46:59Z

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.

jstoobysmith · 2026-03-09T05:24:31Z

Could we split the PositiveTemperature results into their own file?

jstoobysmith · 2026-03-09T05:25:42Z

Do you actually use the results in the PosReal file in this PR? If so this file should be moved to the mathematics folder, if not it could be removed from this PR.

ichxorya · 2026-03-09T06:06:56Z

Could we split the PositiveTemperature results into their own file?

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!

jstoobysmith · 2026-03-09T06:21:10Z

I guess we can, but since the beginning I though "Basic" was to store "base" data types. It would be done right away!

This is correct, it does in general store the basic data types, but I think where there becomes two main data types involved, Temperature and PositiveTemperature in this case, it becomes easier to split them up.

…table directories (with minor reformat)

ichxorya · 2026-03-09T06:39:34Z

I guess we can, but since the beginning I though "Basic" was to store "base" data types. It would be done right away!
This is correct, it does in general store the basic data types, but I think where there becomes two main data types involved, Temperature and PositiveTemperature in this case, it becomes easier to split them up.

Thank you, I have pushed the new code to my PR following my understanding of your suggestion.

PhysLean/Mathematics/PosReal.lean

PhysLean/Thermodynamics/Temperature/Basic.lean

PhysLean/Thermodynamics/Temperature/PositiveTemperature.lean

…jstoobysmith

…jstoobysmith review

ichxorya · 2026-03-10T05:59:50Z

PhysLean/Thermodynamics/Temperature/PositiveTemperature.lean

+/-- `⟨a, ha⟩ ≤ ⟨b, hb⟩` if and only if `a ≤ b` in `Temperature`. -/
+@[simp]
+lemma mk_le_mk {a b : Temperature} {ha : 0 < a.val} {hb : 0 < b.val} :
+    (⟨a, ha⟩ : PositiveTemperature) ≤ (⟨b, hb⟩ : PositiveTemperature) ↔ a ≤ b := Iff.rfl
+
+/-- `⟨a, ha⟩ < ⟨b, hb⟩` if and only if `a < b` in `Temperature`. -/
+@[simp]
+lemma mk_lt_mk {a b : Temperature} {ha : 0 < a.val} {hb : 0 < b.val} :
+    (⟨a, ha⟩ : PositiveTemperature) < (⟨b, hb⟩ : PositiveTemperature) ↔ a < b := Iff.rfl


Should we remove this and keep ofPosReal_le/lt only?

how about something like StrictMono ofPosReal and StrictMono val or similar

ichxorya · 2026-03-10T06:00:12Z

PhysLean/Thermodynamics/Temperature/Basic.lean

+/-- `⟨a⟩ ≤ ⟨b⟩` if and only if `a ≤ b` in `ℝ≥0`. -/
+@[simp]
+lemma mk_le_mk {a b : ℝ≥0} : Temperature.mk a ≤ Temperature.mk b ↔ a ≤ b := Iff.rfl

-/-- Build a `Temperature` directly from a nonnegative real. -/
-@[simp] def ofNNReal (t : ℝ≥0) : Temperature := ⟨t⟩
+/-- `⟨a⟩ < ⟨b⟩` if and only if `a < b` in `ℝ≥0`. -/
+@[simp]
+lemma mk_lt_mk {a b : ℝ≥0} : Temperature.mk a < Temperature.mk b ↔ a < b := Iff.rfl


Should we remove this and keep ofNNReal_le/lt only?

StrictMono ofNNReal and StrictMono Temperature.mk?

jstoobysmith · 2026-03-12T09:47:04Z

FYI you can now use comments to add and remove labels on PRs. When you are ready for the next review you can make the comment -awaiting-author to remove the awaiting-author tag.

feat: 20 of March PR to make the branch up-to-date

…as requested

ichxorya · 2026-03-20T04:17:05Z

-awaiting-author

Sorry for the wait, I was busy with my job search. Things might go back on track soon. @jstoobysmith can you review to see if I can implement the rest of the differentiations and limits, or should I further refine these existing definitions?

jstoobysmith · 2026-03-20T06:39:59Z

This current PR looks good to me.
If you can fix the linters I think we should merge this and leave the differentiations and limits to another PR.

jstoobysmith · 2026-03-20T06:40:10Z

awaiting-author

ichxorya · 2026-03-20T10:08:44Z

This current PR looks good to me.
If you can fix the linters I think we should merge this and leave the differentiations and limits to another PR.

Thank you. I'm on my way fixing the linter. But currently do we allows for unsuccessful build of the whole repository?

Since this is being used by Canonical Ensemble, and (1) we hadn't add all diff/limits theories for PositiveTemperatur, and (2) Canonical Ensemble is currently using those definitions (but was in the "removed" definitions in Temperature). Thus lake build will not completely build the repo and throw error at the Canonical Ensemble module.

jstoobysmith · 2026-03-20T10:39:18Z

awaiting-author

Ok, thanks for explaining. Yeah we require that lake build works for the whole project.

So let's add diff/limits for PositiveTemperature now, and I can review those.

In general when making a PR I think it is good to think about what the logically independent changes are, and how they can be separated into different PRs.

…culus and continuity proofs)

ichxorya · 2026-03-20T15:20:10Z

-awaiting-author

If this commit pass, I think we are ready to review how CanonicalEnsemble should depend on the new PositiveTemperature proofs and definitions.

…ce, and Regularity files

jstoobysmith

Some similar comments throughout.

PhysLean/Thermodynamics/Temperature/PositiveTemperature/Calculus.lean

PhysLean/Thermodynamics/Temperature/PositiveTemperature/Convergence.lean

ichxorya · 2026-03-22T14:58:45Z

Some similar comments throughout.

Thank you I will check them out later!

ichxorya · 2026-03-24T09:46:46Z

@jstoobysmith I have refactored these lengthy proofs following your suggestions.

-awaiting-author

If this commit pass, I think we are ready to review how CanonicalEnsemble should depend on the new PositiveTemperature proofs and definitions.

ichxorya · 2026-03-25T04:27:01Z

-awaiting-author

jstoobysmith · 2026-03-25T06:46:53Z

Ok, I think we can go onto the CanonicalEnsemble stuff, if that is what is blocking the building

…iveTemperature

…ll use Temperature, the Beta function is explicitly defined

ichxorya · 2026-03-25T16:00:48Z

There are 4 files in Canonical Ensemble to rework, but to be frank, my physics knowledge is not enough to figure out how to refactor (as Canonical Ensemble wasn't included in our general physics courses).

In this Basic file, (with suggestions from Claude LLM), I converted some T into PositiveTemperature, while some still kept as T (but still have to invoke Beta function; which is resolved by... calling 1/kb*T). I don't know if they should be kept as Temperature or should I convert them into PositiveTemperature.

@hungle0503 can you review this as well?

feat(temperature): introduce PosReal and PositiveTemperature types

f8af4ba

ichxorya marked this pull request as ready for review March 6, 2026 03:31

ichxorya marked this pull request as draft March 6, 2026 03:31

ichxorya marked this pull request as ready for review March 7, 2026 14:49

chore: add copyright and license information to PosReal.lean

294d01f

jstoobysmith added t-thermodynamics Thermodynamics awaiting-author A reviewer has asked the author a question or requested changes labels Mar 9, 2026

refactor(PosReal, Temperature): Migrate files and code content to sui…

3234c64

…table directories (with minor reformat)

jstoobysmith reviewed Mar 9, 2026

View reviewed changes

style(Temperature, PositiveTemperature): optimize the code following @…

25f7f99

…jstoobysmith review

ichxorya commented Mar 10, 2026

View reviewed changes

ichxorya added 4 commits March 20, 2026 00:21

Merge branch '0503-positivetemperature' into master

b189515

Merge pull request #1 from SEhumantics/master

38de3f7

feat: 20 of March PR to make the branch up-to-date

feat(temperature): add strict monotonicity lemmas for Temperature(s) …

a6c622c

…as requested

style(temperature): adjust import statements and use split_ifs

743ba60

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Mar 20, 2026

github-actions bot added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 20, 2026

ichxorya added 2 commits March 20, 2026 15:03

style(temperature): reorder imports and open namespaces

45745e7

feat(temperature): add PositiveTemperature module and components (cal…

4326622

…culus and continuity proofs)

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Mar 20, 2026

ichxorya added 2 commits March 20, 2026 15:22

style(temperature): clean up comments in Calculus and Convergence files

1b5337d

style(temperature): improve comment formatting in Calculus, Convergen…

1cfd925

…ce, and Regularity files

jstoobysmith reviewed Mar 22, 2026

View reviewed changes

ichxorya added 4 commits March 23, 2026 23:16

Merge branch 'leanprover-community:master' into 0503-positivetemperature

b71da0a

Merge branch 'leanprover-community:master' into 0503-positivetemperature

cfc76e2

refactor(Temperature): simplify Calculus lemmas

6f3b441

refactor(Convergence): simplify Convergence lemmas

350dee0

github-actions bot added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 24, 2026

refactor(Convergence): simplify Convergence lemmas

e024669

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Mar 25, 2026

ichxorya added 3 commits March 25, 2026 15:15

Merge branch 'leanprover-community:master' into 0503-positivetemperature

19cdd31

style(temperature): add module to Calculus and Convergence of Posit…

81cbd98

…iveTemperature

feat: refine the code to use PositiveTemperature; for those which sti…

871cf1e

…ll use Temperature, the Beta function is explicitly defined

Conversation

ichxorya commented Mar 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jstoobysmith commented Mar 6, 2026

Uh oh!

ichxorya commented Mar 6, 2026

Uh oh!

jstoobysmith commented Mar 9, 2026

Uh oh!

jstoobysmith commented Mar 9, 2026

Uh oh!

ichxorya commented Mar 9, 2026

Uh oh!

jstoobysmith commented Mar 9, 2026

Uh oh!

ichxorya commented Mar 9, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ichxorya Mar 10, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Mar 10, 2026

Choose a reason for hiding this comment

Uh oh!

ichxorya Mar 10, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Mar 10, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith commented Mar 12, 2026

Uh oh!

ichxorya commented Mar 20, 2026

Uh oh!

jstoobysmith commented Mar 20, 2026

Uh oh!

jstoobysmith commented Mar 20, 2026

Uh oh!

ichxorya commented Mar 20, 2026

Uh oh!

jstoobysmith commented Mar 20, 2026

Uh oh!

ichxorya commented Mar 20, 2026

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ichxorya commented Mar 22, 2026

Uh oh!

ichxorya commented Mar 24, 2026

Uh oh!

ichxorya commented Mar 25, 2026

Uh oh!

jstoobysmith commented Mar 25, 2026

Uh oh!

ichxorya commented Mar 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

ichxorya commented Mar 5, 2026 •

edited

Loading