Re: [tlaplus] Defining State_I as the state at energy level \epsilon(I)

On Tuesday, April 30, 2024 at 4:33:51 AM UTC+12 marta zhango wrote:

N[i][g] ==

LET

numerator == Sum(k, N[i][k] * W[i][k] * C[j])

denominator == Sum(k, W[i][k] * C[j])

IN

numerator / denominator

On Tuesday, April 30, 2024 at 4:25:16 AM UTC+12 marta zhango wrote:
Specifically I compute the average number of particles at energy level i.

Here, Sum(k, ...) represents the summation over all possible values of k.
N[i][k] represents the number of particles at energy level i in macrostate k.
W[i][k] represents a weight associated with macrostate k at energy level i.
C[j] represents an arbitrary microstate j within macrostate k.

N[i][g] == LET numerator == Sum(k, N[i][k] * W[i][k] * C[j]) denominator == Sum(k, W[i][k] * C[j]) IN numerator / denominator

On Tuesday, April 30, 2024 at 4:10:48 AM UTC+12 marta zhango wrote:
I want to define the number of particles N at energy level E_i for a given microstate
p within macrostate k.

On Tuesday, April 30, 2024 at 2:58:34 AM UTC+12 Stephan Merz wrote:
It sounds like the macro- and microstates should also be parameters of the relevant operators (E and possibly epsilon). In formal mathematics, you cannot leave parameters implicit as it is sometimes done on a whiteboard or perhaps on paper: the machine is unforgiving and will not figure out what is implicit. This is not specific to TLA+ but also true of Coq, Isabelle or Lean.

I am not sure about the quantifiers, however: do you really mean E(i,s,…) to be the same value for all parameters? Of course, a definition is never wrong: it may simply not represent what you have in mind, and the good thing about formal mathematics is that you can play with your definitions and find out if they say what you mean.

Stephan

On 29 Apr 2024, at 15:58, marta zhango <marta...@xxxxxxxxx> wrote:

Correct, energy level i of some particular state. E_i(s)

Each state has n energy levels. There are also m macrostates at each
energy level i, and each macrostate can have p possible microstates.

How would I define them ?

On Monday, April 29, 2024 at 10:41:25 PM UTC+12 Stephan Merz wrote:
I presume that should be E_i(s)? But then, I don’t understand the quantifiers, and the bound variables k and j appear nowhere in your definition?

Stephan

On 29 Apr 2024, at 10:09, marta zhango <marta...@xxxxxxxxx> wrote:

Would that translate to something like

{ s \in S : \A i \in 1..n, k \in 1..m, j \in 1..p : E_i = \epsilon(i)} }

to mean the state s in S such that the energy of s is \epsilon(i)
for m macrostates and p microstates.

On Monday, April 29, 2024 at 5:41:46 PM UTC+12 Stephan Merz wrote:
TLA+ has bounded set comprehension:

{ x \in S : P(x) }

Unbounded comprehension is disallowed: this helps making the definition of Russell’s “set” illegal.

Stephan
--
Stephan Merz

On 29 Apr 2024, at 03:23, marta zhango <marta...@xxxxxxxxx> wrote:

How can I define State_I as the state at energy level \epsilon(I)} ?

State_I \in {energy_level : energy_level = \epsilon(I)}

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/643c7e96-552f-4ae5-ba67-84a2f2c390d3n%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/81197891-9342-4c88-867b-b47d47ad1068n%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4ba993d8-c1cc-4a65-9e9e-c2328bd9f138n%40googlegroups.com.