attempt at the ideal gas law

PhysLean/KineticTheory/Basic.lean

@@ -0,0 +1,56 @@
+import Mathlib
+import PhysLean.Meta.TODO.Basic
+import PhysLean.Meta.Informal.SemiFormal
+import PhysLean.Meta.Informal.Basic
+
+namespace KineticTheory
+open Real
+
+
+/-- An Ideal gas
+ -/
+structure IdealGas where
+  /-- The Pressure of an Ideal Gas. -/
+  P : ℝ
+  /-- The Volume of the Ideal Gas. -/
+  V : ℝ
+  /-- The number of molecules in the Ideal Gas. -/
+  N : ℝ
+  /-- The Temperature of the Ideal Gas. -/
+  T : ℝ
+
+  P_pos : 0 < P
+  V_pos : 0 < V
+  N_pos : 0 < N
+  T_pos : 0 < T
+
+namespace IdealGas
+
+/--The Boltzmann constant--/
+def k_B : ℝ := 1.38064852 * 0.1^(23)
+
+variable (I : IdealGas)
+
+@[simp]
+lemma P_neq_zero : I.P ≠ 0 := Ne.symm (ne_of_lt I.P_pos)
+
+@[simp]
+lemma V_neq_zero : I.V ≠ 0 := Ne.symm (ne_of_lt I.V_pos)
+
+@[simp]
+lemma N_neq_zero : I.N ≠ 0 := Ne.symm (ne_of_lt I.N_pos)
+
+@[simp]
+lemma T_neq_zero : I.T ≠ 0 := Ne.symm (ne_of_lt I.T_pos)
+
+/-- The internal Energy of an Ideal Gas -/
+noncomputable def internalEnergy :=  3/2 * I.N * k_B * I.T
+
+
+/-- TODO "Prove the equation of state later kinetic theory" --/ 
+lemma eqn_of_state : I.P * I.V = I.N * k_B * I.T  := by sorry
+
+
+end IdealGas 
+end KineticTheory 
+