diff --git a/content/http..mathhub.info/MitM/Models/poisson/$Displacement$Law.omdoc b/content/http..mathhub.info/MitM/Models/poisson/$Displacement$Law.omdoc
index 1ff8b452d220290fb8b079ace9e014071f0b1a58..321919a705660585d67bc400a99c648b0b75b15b 100644
--- a/content/http..mathhub.info/MitM/Models/poisson/$Displacement$Law.omdoc
+++ b/content/http..mathhub.info/MitM/Models/poisson/$Displacement$Law.omdoc
@@ -1,6 +1,6 @@
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="DisplacementLaw" base="http://mathhub.info/MitM/Models/poisson" meta="http://mathhub.info/MitM/Models?Base"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1171.29.0:1469.38.1"/></metadata><import from="http://mathhub.info/MitM/Models/densities?ElectrostaticPotential"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1209.30.1:1250.30.42"/></metadata></import><import from="http://mathhub.info/MitM/Models/poisson?PoissonParameters"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1253.31.1:1280.31.28"/></metadata></import><import from="http://mathhub.info/MitM/Models/poisson?Displacement"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1283.32.1:1305.32.23"/></metadata></import><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1310.34.1:1386.34.77"/></metadata>Expression for electric displacement denoted by <unparsed>None</unparsed> = <unparsed>None</unparsed> d/dx <unparsed>None</unparsed></opaque><constant name="electric_displacement">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/mmt/poisson.mmt#1390.36.1:1467.37.30"/></metadata>
- <type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[Ω → displacement_dim]]></om:text></om:OMSF></om:OMOBJ></type>
+ <type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[Ω ⟶ displacement_dim]]></om:text></om:OMSF></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[[x] -ε_s ⋅ (ψ ' x)]]></om:text></om:OMSF></om:OMOBJ></definition>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="D"> <scope languages="" priority="0"/> </notation></notations>
</constant></theory></omdoc>
\ No newline at end of file
diff --git a/content/http..mathhub.info/MitM/Models/thermistor/$Spatial$Reference$Electrical$Field.omdoc b/content/http..mathhub.info/MitM/Models/thermistor/$Spatial$Reference$Electrical$Field.omdoc
index 78cd8532cbf05803b1700d15acaac4b6854bba9a..5ad6858730657c0f80ded642a6af081892433b3a 100644
--- a/content/http..mathhub.info/MitM/Models/thermistor/$Spatial$Reference$Electrical$Field.omdoc
+++ b/content/http..mathhub.info/MitM/Models/thermistor/$Spatial$Reference$Electrical$Field.omdoc
@@ -1,6 +1,6 @@
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="SpatialReferenceElectricalField" base="http://mathhub.info/MitM/Models/thermistor" meta="http://mathhub.info/MitM/Models?Base"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/thermistor/quantities.mmt#2155.71.0:2342.75.-1"/></metadata><import from="http://mathhub.info/MitM/Models/thermistor?DeviceGeometry"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/thermistor/quantities.mmt#2210.72.2:2234.72.26"/></metadata></import><import from="http://mathhub.info/MitM/Models/thermistor?ElectricalFieldStrength"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/thermistor/quantities.mmt#2238.73.2:2271.73.35"/></metadata></import><constant name="referebceelectricfield">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/Models/thermistor/quantities.mmt#2275.74.2:2341.74.68"/></metadata>
- <type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[Ω → (electricfieldstrength_dim)]]></om:text></om:OMSF></om:OMOBJ></type>
+ <type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unparsed"><![CDATA[Ω ⟶ (electricfieldstrength_dim)]]></om:text></om:OMSF></om:OMOBJ></type>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="Eref"> <scope languages="" priority="0"/> </notation></notations>
</constant></theory></omdoc>
\ No newline at end of file
diff --git a/source/mmt/Quantities.mmt b/source/mmt/Quantities.mmt
index 77ac92d51a6d36a5c314354b748d70fc9e878a18..c04af89e3cbb9eee0920b2de4904e3aa76ba3c8d 100644
--- a/source/mmt/Quantities.mmt
+++ b/source/mmt/Quantities.mmt
@@ -1,70 +1,70 @@
-namespace http://mathhub.info/MitM/Models
-import qe http://mathhub.info/MitM/Foundation/Units
+namespace http://mathhub.info/MitM/Models âš
+import qe http://mathhub.info/MitM/Foundation/Units âš
-/T This is a theory containing the electric displacement.
+/T This is a theory containing the electric displacement. âš
theory Displacement : qe:?SIUnits =
- // meta modeltype physical_quantity
- // displacement_dim : type = QE (ElectricCharge /' (Length *' Length))
- displacement : QE( ElectricDisplacement ) # D
-
+ // meta modeltype physical_quantity â™
+ // displacement_dim : type ☠= QE (ElectricCharge /' (Length *' Length)) â™
+ displacement : QE( ElectricDisplacement ) ☠# D â™
+âš
theory Permittivity : qe:?SIUnits =
- // meta modeltype physical_quantity
- // permittivity_dim : type = QE (ElectricCharge /' (ElectricPotential *' Length))
- permittivity : QE( ElectricalPermittivity ) # εs
-
+ // meta modeltype physical_quantity â™
+ // permittivity_dim : type ☠= QE (ElectricCharge /' (ElectricPotential *' Length)) â™
+ permittivity : QE( ElectricalPermittivity ) ☠# εs â™
+âš
theory Density : qe:?SIUnits =
- // meta modeltype physical_quantity
- // density_dim : dimension = (DimNone /' (Length *' Length *' Length))
- density : QE( VolumeDensity )
-
+ // meta modeltype physical_quantity â™
+ // density_dim : dimension ☠= (DimNone /' (Length *' Length *' Length)) â™
+ density : QE( VolumeDensity ) â™
+âš
theory CurrentDensity : qe:?SIUnits =
- // meta modeltype physical_quantity
- // currentdensity_dim : dimension = (Current /' Area)
- currentdensity : QE ( CurrentDensity )
-
+ // meta modeltype physical_quantity â™
+ // currentdensity_dim : dimension ☠= (Current /' Area) â™
+ currentdensity : QE ( CurrentDensity ) â™
+âš
theory RecombinationRate : qe:?QEBase =
- include Models/device?DeviceGeometry
- // meta modeltype physical_quantity
- // recombinationrate_dim : dimension = DimNone /' (Volume *' Time)
- recombinationrate : Ω → QE RecombinationRate # R
-
+ include Models/device?DeviceGeometry â™
+ // meta modeltype physical_quantity â™
+ // recombinationrate_dim : dimension ☠= DimNone /' (Volume *' Time) â™
+ recombinationrate : Ω ⟶ QE RecombinationRate ☠# R â™
+âš
theory RecombinationCoefficient : top:?Base =
- include ?Density
- recombination_coefficient : QE( VolumeDensity )→ QE( VolumeDensity ) → QE (Volume /' Time) # r 1 2
+ include ?Density â™
+ recombination_coefficient : QE( VolumeDensity )⟶ QE( VolumeDensity ) ⟶ QE (Volume /' Time) ☠# r 1 2 â™
-
+âš
theory Energy : qe:?QEBase =
- energy : QE Energy
-
+ energy : QE Energy â™
+âš
theory SpatialDensity : qe:?QEBase =
- include Models/device?DeviceGeometry
- include ?Density
- spatialdensity : Ω → QE( VolumeDensity ) # n 1
-
+ include Models/device?DeviceGeometry â™
+ include ?Density â™
+ spatialdensity : Ω ⟶ QE( VolumeDensity ) ☠# n 1â™
+âš
theory SpatialPotential : top:?Base =
- include Models/device?DeviceGeometry
+ include Models/device?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- potential : Ω → QE ( ElectricPotential ) # φ 1
-
+ usually denoted by $φ$. â™
+ potential : Ω ⟶ QE ( ElectricPotential ) ☠# φ 1â™
+âš
theory SpatialChargeDensity : top:?Base =
- include Models/device?DeviceGeometry
- include ?Density
- charge : Ω → QE ( ElectricChargeDensity ) # Q 1
-
+ include Models/device?DeviceGeometry â™
+ include ?Density â™
+ charge : Ω ⟶ QE ( ElectricChargeDensity ) ☠# Q 1 â™
+âš
theory SpatialCurrentDensity : top:?Base =
- include Models/device?DeviceGeometry
- include ?CurrentDensity
- spatialcurrentdensity : Ω → QE( CurrentDensity ) # j 1
-
\ No newline at end of file
+ include Models/device?DeviceGeometry â™
+ include ?CurrentDensity â™
+ spatialcurrentdensity : Ω ⟶ QE( CurrentDensity ) ☠# j 1 â™
+âš
\ No newline at end of file
diff --git a/source/mmt/VanRoosbroeck.mmt b/source/mmt/VanRoosbroeck.mmt
index a583d83ac97bb7694672439c44a0df7f543f6525..272b43d80ff1cb6dfc14a1d5d47d2a285d48c5d5 100644
--- a/source/mmt/VanRoosbroeck.mmt
+++ b/source/mmt/VanRoosbroeck.mmt
@@ -1,5 +1,5 @@
-namespace http://mathhub.info/MitM/Models/VanRoosbroeck
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/VanRoosbroeck âš
+import top http://mathhub.info/MitM/Models âš
/T This is a theory containing the stationary van Roosbroeck system
describung the charge transport of electrons and holes
@@ -11,13 +11,13 @@ import top http://mathhub.info/MitM/Models
density of states, mobilties are assumed to be
homogenous (spatially constant). Also a homogenous device
temperature is assumed.
-
+ âš
theory VanRoosbroeck : top:?Base =
- include poissonElectrostatics?PoissonEquation
- include poisson?PoissonBoundaryConditions
- include continuity?ContinuityEquationElectrons
- include continuity?ContinuityEquationHoles
- include continuity?ContinuityBoundaryConditionsElectrons
- include continuity?ContinuityBoundaryConditionsHoles
- include recombination?SpontaneousRecombination
-
\ No newline at end of file
+ include poissonElectrostatics?PoissonEquation â™
+ include poisson?PoissonBoundaryConditions â™
+ include continuity?ContinuityEquationElectrons â™
+ include continuity?ContinuityEquationHoles â™
+ include continuity?ContinuityBoundaryConditionsElectrons â™
+ include continuity?ContinuityBoundaryConditionsHoles â™
+ include recombination?SpontaneousRecombination â™
+âš
\ No newline at end of file
diff --git a/source/mmt/band.mmt b/source/mmt/band.mmt
index 2a40dde1690cc71c14872a4b418c69838d8aea26..05c0fd03f4e35900630bfc87ec9356006840ee1f 100644
--- a/source/mmt/band.mmt
+++ b/source/mmt/band.mmt
@@ -1,24 +1,24 @@
-namespace http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models âš
/T This is a theory containing the bandstructure parameters of
- the semiconductor.
-/T Parameter
+ the semiconductor. âš
+/T Parameter âš
theory BandstructureParameters : top:?Base =
structure effective_density : top:?Density =
- density @ effective_density_of_states # N
-
+ density @ effective_density_of_states ☠# N â™
+ âš
/T The effective density of states for the conduction bands
- usually denoted by $N$.
- /T The conduction band edge usually denoted by $E$.
- band_edge : QE Energy # E
- /T Charge number (for electrons -1, for holes 1)
- charge_number : ℤ # z
- mobility : QE (Area /' (ElectricPotential *' Time)) # μ
-
+ usually denoted by $N$. â™
+ /T The conduction band edge usually denoted by $E$. â™
+ band_edge : QE Energy ☠# E â™
+ /T Charge number (for electrons -1, for holes 1) â™
+ charge_number : ℤ ☠# z â™
+ mobility : QE (Area /' (ElectricPotential *' Time)) ☠# μ â™
+âš
theory Band : top:?Base =
- include ?BandstructureParameters
+ include ?BandstructureParameters â™
structure fermi : top:?SpatialPotential =
- potential # φ 1
-
-
\ No newline at end of file
+ potential # φ 1 â™
+ âš
+âš
\ No newline at end of file
diff --git a/source/mmt/constants.mmt b/source/mmt/constants.mmt
index 7001b498cee349f9d789153d3f901ebb805bb9a0..162392412786e02a618aeff74338db32fac52ee8 100644
--- a/source/mmt/constants.mmt
+++ b/source/mmt/constants.mmt
@@ -1,31 +1,31 @@
-namespace http://mathhub.info/MitM/Models
-import mitm http://mathhub.info/MitM
-import lfx http://gl.mathhub.info/MMT/LFX
+namespace http://mathhub.info/MitM/Models âš
+import mitm http://mathhub.info/MitM âš
+import lfx http://gl.mathhub.info/MMT/LFX âš
-/T This is a theory containing general physical constants
+/T This is a theory containing general physical constants âš
theory PhysicalConstants : mitm:/Foundation/Units?SIUnits =
- include ?Permittivity
- include mitm:/smglom/arithmetics?realarith
- /T The vaccuum dielectric permitivity constant (usually denoted by $ε_0$)
- vacuum_dielectric_permitivity : permittivity_dim # ε_0
- /T The elementary charge (denoted by $q$)
- elementary_charge : QE ElectricCharge # q
- /T The Boltzmann constant (usually denoted by $k_B$)
- Boltzmann_constant : QE (Energy /' Temperature) # k_B
-
+ include ?Permittivity â™
+ include mitm:/smglom/arithmetics?realarith â™
+ /T The vaccuum dielectric permitivity constant (usually denoted by $ε_0$) â™
+ vacuum_dielectric_permitivity : permittivity_dim ☠# ε_0 â™
+ /T The elementary charge (denoted by $q$) â™
+ elementary_charge : QE ElectricCharge ☠# q â™
+ /T The Boltzmann constant (usually denoted by $k_B$) â™
+ Boltzmann_constant : QE (Energy /' Temperature) ☠# k_B â™
+âš
theory Base : mitm:/smglom/arithmetics?realarith =
- include ?PhysicalConstants
- include http://mathhub.info/MitM/smglom/calculus?derivative
- // TODO anständige ableitung (Einheiten!!)
- unit_pred : {D : dimension, P : ℠→ bool} type
- = [D,P] ⟨ QE D | [x] ⊦ P (scalar x) ⟩ # dpred 1 2
- inof : {D : dimension, u : unit D, P : ℠→ bool, r : pred P}dpred D P # 4 inof 2 // TODO
- scalarp : {D : dimension, P : ℠→ bool} dpred D P → pred P # scalarp 3
+ include ?PhysicalConstants â™
+ include http://mathhub.info/MitM/smglom/calculus?derivative â™
+ // TODO anständige ableitung (Einheiten!!) â™
+ unit_pred : {D : dimension, P : ℠⟶ bool} type â˜
+ = [D,P] ⟨ QE D | [x] ⊦ P (scalar x) ⟩ ☠# dpred 1 2 â™
+ inof : {D : dimension, u : unit D, P : ℠⟶ bool, r : pred P}dpred D P ☠# 4 inof 2 â™ // TODO â™
+ scalarp : {D : dimension, P : ℠⟶ bool} dpred D P ⟶ pred P ☠# scalarp 3 â™
- // TODO
- // unit_derivative : {P : ℠→ bool, Da : dimension, Db : dimension, u : unit Da, f : (dpred Da P) → QE Db, p : ⊦ diff [x : pred P] scalar (f (x inof u))} dpred Da P → QE Db
- = [P,Da,Db,u,f,p] ([y] ([x : pred P] (scalar (f (x inof u)))' (scalarp y)) of (unitof y) )
+ // TODO â™
+ // unit_derivative : {P : ℠⟶ bool, Da : dimension, Db : dimension, u : unit Da, f : (dpred Da P) ⟶ QE Db, p : ⊦ diff [x : pred P] scalar (f (x inof u))} dpred Da P ⟶ QE Db â˜
+ = [P,Da,Db,u,f,p] ([y] ([x : pred P] (scalar (f (x inof u)))' (scalarp y)) of (unitof y) ) â™
- // Ω = kompakte, einfach zusammenhängende teilmenge des â„^n für n â€âˆˆ 4
-
+ // Ω = kompakte, einfach zusammenhängende teilmenge des â„^n für n â€âˆˆ 4 â™
+âš
diff --git a/source/mmt/continuity.mmt b/source/mmt/continuity.mmt
index 6ae3c84b92b67e2a61a3d9e0825f9b2b795f0053..c77c77a50f400a67dbe758848c25641a4027e614 100644
--- a/source/mmt/continuity.mmt
+++ b/source/mmt/continuity.mmt
@@ -1,60 +1,60 @@
-namespace http://mathhub.info/MitM/Models/continuity
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/continuity âš
+import top http://mathhub.info/MitM/Models âš
/T This is a theory containing the mobilitiy parameters of
- the semiconductor.
+ the semiconductor. âš
theory Mobility : top:?Base =
- /T The mobility parameter usually denoted by $μ$.
-
+ /T The mobility parameter usually denoted by $μ$. â™
+âš
-/T This is a theory containing the expression for the hole current.
+/T This is a theory containing the expression for the hole current. âš
theory CurrentLaw : top:?Base =
- include top:?Band
- include top:?BandstructureParameters
- include top:?SpatialCurrentDensity
+ include top:?Band â™
+ include top:?BandstructureParameters â™
+ include top:?SpatialCurrentDensity â™
/T Defintion of the hole current in gradient form.
The driving force of the current are the negative gradient of
- the quasi-Fermi potential, here denoted by j_p.
- // TODO: change to more natural formulation later, e.g. f-> xψ, g-> xφ_p?
+ the quasi-Fermi potential, here denoted by j_p. â™
+ // TODO: change to more natural formulation later, e.g. f-> xψ, g-> xφ_p? â™
- current_law : {x : Ω} ⊦ j x ≠-q ⋅ μ ⋅ (n x) ⋅ ((φ ') x)
-
+ current_law : {x : Ω} ⊦ j x ≠-q â‹… μ â‹… (n x) â‹… ((φ ') x) â™
+âš
-/T This is a theory containing the continuity equation for the electrons.
+/T This is a theory containing the continuity equation for the electrons. âš
theory ContinuityEquation : top:?Base =
- include top:/Species?Species
- include top:?RecombinationRate
+ include top:/Species?Species â™
+ include top:?RecombinationRate â™
- /T Formulation of the continuity equation for electrons in divergence form.
+ /T Formulation of the continuity equation for electrons in divergence form. â™
continuity_equation :
- {x : Ω} ⊦ (j ') x ≠-z (R x)
-
+ {x : Ω} ⊦ (j ') x ≠-z (R x) â™
+âš
/T This is a theory containing the boundary conditions for the
- electron continuity equation modeling Ohmic contacts.
+ electron continuity equation modeling Ohmic contacts. âš
theory ContinuityBoundaryConditionsElectrons : top:?Base =
- include device?DeviceOperationState
- /T Boundary condition for the top contact.
- potential_top : QE ElectricPotential = U_1 # φ_n_1
- /T Boundary condition for the bottom contact.
- potential_bottom : QE ElectricPotential = U_2 # φ_n_2
-
+ include device?DeviceOperationState â™
+ /T Boundary condition for the top contact. â™
+ potential_top : QE ElectricPotential ☠= U_1 ☠# φ_n_1 â™
+ /T Boundary condition for the bottom contact. â™
+ potential_bottom : QE ElectricPotential ☠= U_2 ☠# φ_n_2 â™
+âš
/T This is a theory containing the boundary conditions for the
- holes continuity equation modeling Ohmic contacts.
+ holes continuity equation modeling Ohmic contacts. âš
theory ContinuityBoundaryConditionsHoles : top:?Base =
- include device?DeviceOperationState
- /T Boundary condition for the top contact.
- potential_top : QE ElectricPotential = U_1 # φ_p_1
- /T Boundary condition for the bottom contact.
- potential_bottom : QE ElectricPotential = U_2 # φ_p_2
-
\ No newline at end of file
+ include device?DeviceOperationState â™
+ /T Boundary condition for the top contact. â™
+ potential_top : QE ElectricPotential ☠= U_1 ☠# φ_p_1 â™
+ /T Boundary condition for the bottom contact. â™
+ potential_bottom : QE ElectricPotential ☠= U_2 ☠# φ_p_2 â™
+âš
\ No newline at end of file
diff --git a/source/mmt/densities.mmt b/source/mmt/densities.mmt
index af435b1460b458be5d88aaf341020c9a5eff1394..bcc101e795b61f589048764ddb4ec5daf63f4584 100644
--- a/source/mmt/densities.mmt
+++ b/source/mmt/densities.mmt
@@ -1,22 +1,22 @@
-namespace http://mathhub.info/MitM/Models/densities
-import top http://mathhub.info/MitM/Models
-import arith http://mathhub.info/MitM/smglom/arithmetics
+namespace http://mathhub.info/MitM/Models/densities âš
+import top http://mathhub.info/MitM/Models âš
+import arith http://mathhub.info/MitM/smglom/arithmetics âš
/T This is a theory containing state equation for the
- density for the Boltzmann approximation (exp).
-/T Solution
+ density for the Boltzmann approximation (exp). âš
+/T Solution âš
theory DensityLaw : top:?Base =
-// meta model_type physical_law
- include device?DeviceOperationState
- include top:?PhysicalConstants
- include top:?Density
- include top:?SpatialDensity
+// meta model_type physical_law â™
+ include device?DeviceOperationState â™
+ include top:?PhysicalConstants â™
+ include top:?Density â™
+ include top:?SpatialDensity â™
structure electrostatic : top:?SpatialPotential =
- domain = `top:/device?DeviceGeometry?domain
- potential # ψ
- // should be an include, but...
- structure band : top:?Band =
- /T Formula for the electron density for the Boltzmann approximation.
- density_law : {x : Ω} ⊦ n x ≠N ⋅ `arith:?realarith?exponentiation (scalar (((- q) ⋅ z ⋅ ((ψ x) - (φ x)) - E) / k_B ⋅ T))
-
\ No newline at end of file
+ domain = `top:/device?DeviceGeometry?domain â™
+ potential # ψ â™
+ âš // should be an include, but... â™
+ structure band : top:?Band = âš
+ /T Formula for the electron density for the Boltzmann approximation. â™
+ density_law : {x : Ω} ⊦ n x ≠N â‹… `arith:?realarith?exponentiation (scalar (((- q) â‹… z â‹… ((ψ x) - (φ x)) - E) / k_B â‹… T)) â™
+âš
\ No newline at end of file
diff --git a/source/mmt/device.mmt b/source/mmt/device.mmt
index 89c551c550550d9652de0342eb1f7f02f64e0021..4e3b9b0e9af6d8bfbcc7c80ed89ed9f3f87e5c5a 100644
--- a/source/mmt/device.mmt
+++ b/source/mmt/device.mmt
@@ -1,63 +1,63 @@
-namespace http://mathhub.info/MitM/Models/device
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/device âš
+import top http://mathhub.info/MitM/Models âš
-/T This theory intentionally left empty. It has a narrative in sTeX
-/T Background
-theory Device =
+/T This theory intentionally left empty. It has a narrative in sTeX âš
+/T Background âš
+theory Device = âš
-/T This is a theory containing description of device geometry.
-/T Parameter
+/T This is a theory containing description of device geometry. âš
+/T Parameter âš
theory DeviceGeometry : top:?Base =
- include ?Device
- // domain_prop : â„3 → bool
- domain_prop : ℠→ bool
- /T The one-dimensional spatial domain of the device (denoted by $Ω$).
- // domain : type = pred3 domain_prop # Ω
- domain : type = pred domain_prop # Ω
-
+ include ?Device â™
+ // domain_prop : â„3 ⟶ bool â™
+ domain_prop : ℠⟶ bool â™
+ /T The one-dimensional spatial domain of the device (denoted by $Ω$). â™
+ // domain : type ☠= pred3 domain_prop ☠# Ω â™
+ domain : type ☠= pred domain_prop ☠# Ω â™
+âš
// theory OneDimDeviceGeometry : top:?Base =
- bottom : â„
- top : â„
- Interval_pred : ℠→ bool = [r] bottom ≤ r ∧ r ≤ top
- Omega_Interval : type = pred Interval_pred # I
+ bottom : â„ â™
+ top : â„ â™
+ Interval_pred : ℠⟶ bool ☠= [r] bottom ≤ r ∧ r ≤ top â™
+ Omega_Interval : type ☠= pred Interval_pred ☠# I â™
structure Geometry : ?DeviceGeometry =
- domain_prop = t1↑ Interval_pred
-
-//
+ domain_prop = t1↑ Interval_pred â™
+ âš
+// âš
// theory TwoDimDeviceGeometry : top:?Base =
- Plane_pred : â„2 → bool
- Omega_Plane : type = pred2 Plane_pred # G
+ Plane_pred : â„2 ⟶ bool â™
+ Omega_Plane : type ☠= pred2 Plane_pred ☠# G â™
structure Geometry : ?DeviceGeometry =
- domain_prop = t2↑ Plane_pred
-
-//
+ domain_prop = t2↑ Plane_pred â™
+ âš
+// âš
-/T This is a theory containing description of the doping profile.
-/T Parameter
+/T This is a theory containing description of the doping profile. âš
+/T Parameter âš
theory DopingProfile : top:?Base =
- include ?DeviceGeometry
- include top:?Density
- /T The doping profile, denoted by $C$.
- doping_profile : Ω → QE density_dim # C
-
+ include ?DeviceGeometry â™
+ include top:?Density â™
+ /T The doping profile, denoted by $C$. â™
+ doping_profile : Ω ⟶ QE density_dim ☠# C â™
+âš
/T This is a theory containing a description the the operating state,
- that means applied voltages and device temperature.
-/T Parameter
+ that means applied voltages and device temperature. âš
+/T Parameter âš
theory DeviceOperationState : top:?Base =
- include ?DeviceGeometry
- /T The global temperature of the device denoted by $T$.
- // temperature : Ω → ℠# T
- temperature : QE Temperature # T
- /T The applied voltage at the bottom contact denoted by $U_1$.
- voltage_bottom : QE ElectricPotential # U_1
- /T The applied voltage at the top contact denoted by $U_2$.
- voltage_top : QE ElectricPotential # U_2
+ include ?DeviceGeometry â™
+ /T The global temperature of the device denoted by $T$. â™
+ // temperature : Ω ⟶ ℠☠# T â™
+ temperature : QE Temperature ☠# T â™
+ /T The applied voltage at the bottom contact denoted by $U_1$. â™
+ voltage_bottom : QE ElectricPotential ☠# U_1 â™
+ /T The applied voltage at the top contact denoted by $U_2$. â™
+ voltage_top : QE ElectricPotential ☠# U_2 â™
- // prf : ⊦ k_B ⋅ T ≠0 . Energy
-
\ No newline at end of file
+ // prf : ⊦ k_B â‹… T ≠0 . Energy â™
+âš
\ No newline at end of file
diff --git a/source/mmt/poisson.mmt b/source/mmt/poisson.mmt
index 1f08384000780effa77c875f4cb457d224315406..1d4f2d08e22e12e9162bf636d9c5d53199f44640 100644
--- a/source/mmt/poisson.mmt
+++ b/source/mmt/poisson.mmt
@@ -1,38 +1,38 @@
-namespace http://mathhub.info/MitM/Models/poisson
-import mitm http://mathhub.info/MitM
-import top http://mathhub.info/MitM/Models
-import qe http://mathhub.info/MMT/physics-units
+namespace http://mathhub.info/MitM/Models/poisson âš
+import mitm http://mathhub.info/MitM âš
+import top http://mathhub.info/MitM/Models âš
+import qe http://mathhub.info/MMT/physics-units âš
/T This is a theory containing a general formulation of
- the Poisson equation.
+ the Poisson equation. âš
-// TODO as a view on elliptic pdes?
+// TODO as a view on elliptic pdes? â™
theory PoissonEquation : top:?Base =
- include mitm:/smglom/arithmetics?realarith
+ include mitm:/smglom/arithmetics?realarith â™
- // TODO f, k and t as functions that are defined on Ω and return values of arbitrary QE on Ω
- f : Ω → QE // needs to be 2 times derivable in Ω but is usually determined to be that was
- u : Ω → QE // additionally needs to be integrable => metricspaces?
+ // TODO f, k and t as functions that are defined on Ω and return values of arbitrary QE on Ω â™
+ f : Ω ⟶ QE // needs to be 2 times derivable in Ω but is usually determined to be that wasâ™
+ u : Ω ⟶ QE // additionally needs to be integrable => metricspaces?â™
- // the dimensions in which we derive (dx) as (subspace of) space where omega lies => probably implicitly by definition of f
+ // the dimensions in which we derive (dx) as (subspace of) space where omega lies => probably implicitly by definition of fâ™
- // general form of PE: usually f is unknown and needs to be solved for
- poisson_equation : {} = <prop | [p] ⊦ ∃f ∃t p= ( d( k*(df/dx))/dx = t) >
+ // general form of PE: usually f is unknown and needs to be solved for â™
+ poisson_equation : {} ☠= <prop | [p] ⊦ ∃f ∃t p= ( d( k*(df/dx))/dx = t) >â™
-
+âš
-/T This is a theory containing the boundary values for the Poisson eqauation.
+/T This is a theory containing the boundary values for the Poisson eqauation. âš
-// TODO probably in a more general setting
+// TODO probably in a more general setting â™
// theory PoissonBoundaryConditions : top:?Base =
- include ?ThermodynamicEquilibrium
+ include ?ThermodynamicEquilibrium â™
/T Boundary value for electrostatic potential at top contact
- for an applied voltage $U_1$.
- potential_top : QE ElectricPotential = ψ_0_1 + U_1 # ψ_1
+ for an applied voltage $U_1$. â™
+ potential_top : QE ElectricPotential ☠= ψ_0_1 + U_1 ☠# ψ_1 â™
/T Boundary value for electrostatic potential at bottom contact
for an applied voltage $U_2$.
- N.B.: the applied bias voltage is U_bias = $U_2-U_1$
- potential_bottom : QE ElectricPotential = ψ_0_2 + U_2 # ψ_2
-
\ No newline at end of file
+ N.B.: the applied bias voltage is U_bias = $U_2-U_1$ â™
+ potential_bottom : QE ElectricPotential ☠= ψ_0_2 + U_2 ☠# ψ_2 â™
+âš
\ No newline at end of file
diff --git a/source/mmt/poissonElectrostatics.mmt b/source/mmt/poissonElectrostatics.mmt
index 07af5a1efee4f33363c22056dd603e385e96917b..00bf6ba4e84ee312fc2f7ac548562ca5e4c16213 100644
--- a/source/mmt/poissonElectrostatics.mmt
+++ b/source/mmt/poissonElectrostatics.mmt
@@ -1,82 +1,82 @@
-namespace http://mathhub.info/MitM/Models/poissonElectrostatics
-import top http://mathhub.info/MitM/Models
-import qe http://mathhub.info/MMT/physics-units
+namespace http://mathhub.info/MitM/Models/poissonElectrostatics âš
+import top http://mathhub.info/MitM/Models âš
+import qe http://mathhub.info/MMT/physics-units âš
/T This is a theory containing the static dielectric permitivity constant
- of the semiconductor.
+ of the semiconductor. âš
theory PoissonParameters : top:?Base =
- /T The relative dielelectric permitivity constant denoted by $ε_r$.
- relative_dielectric_permittivity : real_lit # ε_r
- /T The static dielelectric permittivity constant denoted by $ε_s$.
- dielectric_permittivity : {ε_r : QE ( DimNone ), ε_0 : QE ( ElectricalPermittivity )} QE( DimNone ) → QE ( ElectricalPermittivity ) → QE ( ElectricalPermittivity ) // = ε_r ⋅ ε_0 // TODO implement QE arithmetics (?) # ε_s
-
+ /T The relative dielelectric permitivity constant denoted by $ε_r$. â™
+ relative_dielectric_permittivity : real_lit ☠# ε_r â™
+ /T The static dielelectric permittivity constant denoted by $ε_s$. â™
+ dielectric_permittivity : {ε_r : QE ( DimNone ), ε_0 : QE ( ElectricalPermittivity )} QE( DimNone ) ⟶ QE ( ElectricalPermittivity ) ⟶ QE ( ElectricalPermittivity ) â˜// = ε_r â‹… ε_0 // TODO implement QE arithmetics (?) ☠# ε_s â™
+âš
/T This is a theory containing the total charge entering
- the right side of Poisson's equation.
+ the right side of Poisson's equation. âš
theory ChargeLaw : top:?Base =
- include device?DeviceGeometry
- include device?DopingProfile
- include ?PoissonParameters
- include top:/Species?ElectronsAndHoles
- include top:?SpatialChargeDensity
+ include device?DeviceGeometry â™
+ include device?DopingProfile â™
+ include ?PoissonParameters â™
+ include top:/Species?ElectronsAndHoles â™
+ include top:?SpatialChargeDensity â™
/T The total charge denoted by $Q$ composed of doping profile $C$ and
electron and hole densities $n$ and $p$, defined by
- $Q$ = $q$($C$+$p$ - $n$).
- total_charge_density : {x : Ω} ⊦ Q x ≠-q ⋅ ((C x) + (holes/z ⋅ (holes/density x)) + (electrons/z ⋅ (electrons/density x)))
-
+ $Q$ = $q$($C$+$p$ - $n$). â™
+ total_charge_density : {x : Ω} ⊦ Q x ≠-q â‹… ((C x) + (holes/z â‹… (holes/density x)) + (electrons/z â‹… (electrons/density x))) â™
+âš
// theory DisplacementLaw : top:?Base =
- include densities?ElectrostaticPotential
- include ?PoissonParameters
- include ?Displacement
+ include densities?ElectrostaticPotential â™
+ include ?PoissonParameters â™
+ include ?Displacement â™
- /T Expression for electric displacement denoted by $D$ = $- ε_s$ d/dx $ψ$
+ /T Expression for electric displacement denoted by $D$ = $- ε_s$ d/dx $ψ$ â™
- electric_displacement : Ω → displacement_dim
- = [x] -ε_s ⋅ (ψ ' x) # D
-
+ electric_displacement : Ω ⟶ displacement_dim â˜
+ = [x] -ε_s â‹… (ψ ' x) ☠# D â™
+âš
-/T This is a theory containing Poissons equation.
+/T This is a theory containing Poissons equation. âš
// theory PoissonEquation : top:?Base =
- include ?Charge
- include ?Displacement
+ include ?Charge â™
+ include ?Displacement â™
/T Defintion of the Poisson equation with total charge
- as right hand side.
- poisson_equation : ⊦ D ' ≠Q
+ as right hand side. â™
+ poisson_equation : ⊦ D ' ≠Qâ™
-
+âš
/T This is a theory containing build-in potential in
- thermodynamic equilibrium.
+ thermodynamic equilibrium. âš
// theory ThermodynamicEquilibrium : top:?Base =
- include ?Charge
+ include ?Charge â™
/T Value of build-in potential ψ_0 at top contact guranteeing
- local charge neutrality.
- equilibrium_potential_top : QE ElectricPotential # ψ_0_2
+ local charge neutrality. â™
+ equilibrium_potential_top : QE ElectricPotential ☠# ψ_0_2 â™
/T Value of build-in potential ψ_0 at bottom contact guranteeing
local charge neutrality.
- N.B. the build-in potential is given as U_b = $ψ_0_2 - ψ_0_1$ (Check!)
+ N.B. the build-in potential is given as U_b = $ψ_0_2 - ψ_0_1$ (Check!) â™
- equilibrium_potential_bottom : QE ElectricPotential # ψ_0_1
-
+ equilibrium_potential_bottom : QE ElectricPotential ☠# ψ_0_1 â™
+âš
-/T This is a theory containing the boundary values for the Poisson eqauation.
+/T This is a theory containing the boundary values for the Poisson eqauation. âš
// theory PoissonBoundaryConditions : top:?Base =
- include ?ThermodynamicEquilibrium
+ include ?ThermodynamicEquilibrium â™
/T Boundary value for electrostatic potential at top contact
- for an applied voltage $U_1$.
- potential_top : QE ElectricPotential = ψ_0_1 + U_1 # ψ_1
+ for an applied voltage $U_1$. â™
+ potential_top : QE ElectricPotential ☠= ψ_0_1 + U_1 ☠# ψ_1 â™
/T Boundary value for electrostatic potential at bottom contact
for an applied voltage $U_2$.
- N.B.: the applied bias voltage is U_bias = $U_2-U_1$
- potential_bottom : QE ElectricPotential = ψ_0_2 + U_2 # ψ_2
-
\ No newline at end of file
+ N.B.: the applied bias voltage is U_bias = $U_2-U_1$ â™
+ potential_bottom : QE ElectricPotential ☠= ψ_0_2 + U_2 ☠# ψ_2 â™
+âš
\ No newline at end of file
diff --git a/source/mmt/recombination.mmt b/source/mmt/recombination.mmt
index 50e33d3e36682dacbd94d7be671e30ce5f8439de..eff374de2c51174655f522752a295a94a12cfb5b 100644
--- a/source/mmt/recombination.mmt
+++ b/source/mmt/recombination.mmt
@@ -1,27 +1,27 @@
-namespace http://mathhub.info/MitM/Models/recombination
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/recombination âš
+import top http://mathhub.info/MitM/Models âš
/T This is a theory containing the general structure for
- a recombination rate.
+ a recombination rate. âš
theory Recombination : top:?Base =
- include top:/Species?ElectronsAndHoles
- include top:?RecombinationCoefficient
- include top:?RecombinationRate
- /T Recombination rate for right hand side of continuity equations.
+ include top:/Species?ElectronsAndHoles â™
+ include top:?RecombinationCoefficient â™
+ include top:?RecombinationRate â™
+ /T Recombination rate for right hand side of continuity equations. â™
recombination_rate : {x : Ω} ⊦ R x â‰
(r (electrons/spatialdensity x) (holes/spatialdensity x)) â‹… (electrons/spatialdensity x) â‹… (holes/spatialdensity x)
- â‹… (1 - (exponential (q â‹… ((electrons/fermi/potential x) - (holes/fermi/potential x)) / (k_B â‹… T))))
-
+ â‹… (1 - (exponential (q â‹… ((electrons/fermi/potential x) - (holes/fermi/potential x)) / (k_B â‹… T)))) â™
+âš
-/T Kernel for spontaneous recombination with coefficient B.
+/T Kernel for spontaneous recombination with coefficient B. âš
theory SpontaneousRecombination : top:?Base =
- include ?Recombination
+ include ?Recombination â™
- /T The coefficient for the sponanteous recombination rate is denoted by $B$
- spontaneous_recombination_coefficient : QE (Volume /' SItime) # B
- /T Formula for sponanteous recombination $r$($n$,$p$) = $B$
- axiom_spontaneous : {x,y} ⊦ r x y ≠B role Simplify
-
+ /T The coefficient for the sponanteous recombination rate is denoted by $B$ â™
+ spontaneous_recombination_coefficient : QE (Volume /' SItime) ☠# Bâ™
+ /T Formula for sponanteous recombination $r$($n$,$p$) = $B$ â™
+ axiom_spontaneous : {x,y} ⊦ r x y ≠B ☠role Simplify â™
+âš
diff --git a/source/mmt/species.mmt b/source/mmt/species.mmt
index 8488f6110c9ccf17b00e1c8d470b7600f32f802e..8fd488f557cfe889b8e914f3b69bdcb0c3cf98de 100644
--- a/source/mmt/species.mmt
+++ b/source/mmt/species.mmt
@@ -1,21 +1,21 @@
-namespace http://mathhub.info/MitM/Models/Species
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/Species âš
+import top http://mathhub.info/MitM/Models âš
theory Species : top:?Base =
- include densities?DensityLaw
- include top:?SpatialCurrentDensity
- // include CurrentLaw
-
+ include densities?DensityLaw â™
+ include top:?SpatialCurrentDensity â™
+ // include CurrentLaw â™
+âš
theory Electrons : top:?Base =
- structure electrons : ?Species =
-
+ structure electrons : ?Species = âš
+âš
theory Holes : top:?Base =
- structure holes : ?Species =
-
+ structure holes : ?Species = âš
+âš
theory ElectronsAndHoles : top:?Base =
- include ?Electrons
- include ?Holes
-
\ No newline at end of file
+ include ?Electrons â™
+ include ?Holes â™
+âš
\ No newline at end of file
diff --git a/source/thermistor/quantities.mmt b/source/thermistor/quantities.mmt
index ddedcc31071eb2b16dacacb652a27234d5412f57..7dcb2fbeca59ce09f1f47494f3417b6937818513 100644
--- a/source/thermistor/quantities.mmt
+++ b/source/thermistor/quantities.mmt
@@ -1,229 +1,229 @@
-namespace http://mathhub.info/MitM/Models/thermistor
-import qe http://mathhub.info/MMT/physics-units
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/thermistor âš
+import qe http://mathhub.info/MMT/physics-units âš
+import top http://mathhub.info/MitM/Models âš
-/T This theory intentionally left empty. It has a narrative in sTeX
-/T Background
-theory Device =
+/T This theory intentionally left empty. It has a narrative in sTeX âš
+/T Background âš
+theory Device = âš
-/T This is a theory containing description of device geometry.
-/T Parameter
+/T This is a theory containing description of device geometry. âš
+/T Parameter âš
theory DeviceGeometry : top:?Base =
- include ?Device
- // domain_prop : â„3 → bool
- domain_prop : ℠→ bool
- /T The one-dimensional spatial domain of the device (denoted by $Ω$).
- domain : type = pred domain_prop # Ω
-
+ include ?Device â™
+ // domain_prop : â„3 ⟶ bool â™
+ domain_prop : ℠⟶ bool â™
+ /T The one-dimensional spatial domain of the device (denoted by $Ω$). â™
+ domain : type ☠= pred domain_prop ☠# Ω â™
+âš
theory SpatialPotential : top:?Base =
- include ?DeviceGeometry
+ include ?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- potential : Ω → (QE ElectricPotential) # φ
-
+ usually denoted by $φ$. â™
+ potential : Ω ⟶ (QE ElectricPotential) ☠# φâ™
+âš
theory ElectricFieldStrength : qe:?QEBase =
- electricfieldstrength_dim : type = QE (ElectricPotential /' SIlength)
- electricfieldstrength : electricfieldstrength_dim
-
+ electricfieldstrength_dim : type ☠= QE (ElectricPotential /' SIlength) â™
+ electricfieldstrength : electricfieldstrength_dim â™
+âš
theory SpatialElectricField : top:?Base =
- include ?DeviceGeometry
- include ?ElectricFieldStrength
+ include ?DeviceGeometry â™
+ include ?ElectricFieldStrength â™
/T Spatial variation of the electric field strength,
- usually denoted by $E$.
- electricfield : Ω → (electricfieldstrength_dim) # E
-
+ usually denoted by $E$. â™
+ electricfield : Ω ⟶ (electricfieldstrength_dim) ☠# Eâ™
+âš
theory CurrentDensity : qe:?QEBase =
- // meta modeltype physical_quantity
- currentdensity_dim : type = QE (SIcurrent /' Area)
- currentdensity : currentdensity_dim
-
+ // meta modeltype physical_quantity â™
+ currentdensity_dim : type ☠= QE (SIcurrent /' Area) â™
+ currentdensity : currentdensity_dim â™
+âš
theory SpatialCurrentDensity : top:?Base =
- include ?DeviceGeometry
- include ?CurrentDensity
- currentdensity : Ω → (currentdensity_dim) # j 1
-
+ include ?DeviceGeometry â™
+ include ?CurrentDensity â™
+ currentdensity : Ω ⟶ (currentdensity_dim) ☠# j 1 â™
+âš
theory ElectricalConductivity : qe:?QEBase =
- // meta modeltype physical_quantity
- electricalconductitvity_dim : type = QE (SIcurrent /' (ElectricPotential * SIlength))
- electricalconductitvity : electricalconductitvity_dim
-
+ // meta modeltype physical_quantity â™
+ electricalconductitvity_dim : type ☠= QE (SIcurrent /' (ElectricPotential * SIlength)) â™
+ electricalconductitvity : electricalconductitvity_dim â™
+âš
theory SpatialElectricalConductivity : top:?Base =
- include ?DeviceGeometry
- include ?ElectricalConductivity
- spatialelectricalconductivity : Ω → (electricalconductitvity_dim) # σ 1
-
+ include ?DeviceGeometry â™
+ include ?ElectricalConductivity â™
+ spatialelectricalconductivity : Ω ⟶ (electricalconductitvity_dim) ☠# σ 1 â™
+âš
theory SpatialReferenceConductivity : top:?Base =
- include ?DeviceGeometry
- include ?ElectricalConductivity
- spatialreferenceconductivity : Ω → (electricalconductitvity_dim) # σ_0 1
-
+ include ?DeviceGeometry â™
+ include ?ElectricalConductivity â™
+ spatialreferenceconductivity : Ω ⟶ (electricalconductitvity_dim) ☠# σ_0 1 â™
+âš
theory SpatialReferenceElectricalField : top:?Base =
- include ?DeviceGeometry
- include ?ElectricalFieldStrength
- referebceelectricfield : Ω → (electricfieldstrength_dim) # Eref
-
+ include ?DeviceGeometry â™
+ include ?ElectricalFieldStrength â™
+ referebceelectricfield : Ω ⟶ (electricfieldstrength_dim) ☠# Erefâ™
+âš
theory SpatialFieldEnhancement : top:?Base =
- include ?DeviceGeometry
- spatialfieldenhancement : Ω → ℠# G
-
+ include ?DeviceGeometry â™
+ spatialfieldenhancement : Ω ⟶ ℠☠# Gâ™
+âš
theory SpatialLaplacep : top:?Base =
- include ?DeviceGeometry
- spatiallaplacep : Ω → ℠# p
-
+ include ?DeviceGeometry â™
+ spatiallaplacep : Ω ⟶ ℠☠# pâ™
+âš
theory SpatialArrheniusFaktor : top:?Base =
- include ?DeviceGeometry
- spatialarrheniusfaktor : Ω → ℠# F
-
+ include ?DeviceGeometry â™
+ spatialarrheniusfaktor : Ω ⟶ ℠☠# Fâ™
+âš
theory Heat : qe:?QEBase =
- // meta modeltype physical_quantity
- heat_dim : type = QE (Energy)
- heat : heat_dim
-
+ // meta modeltype physical_quantity â™
+ heat_dim : type ☠= QE (Energy) â™
+ heat : heat_dim â™
+âš
theory SpatialHeatSource : top:?Base =
- include ?DeviceGeometry
- include ?Heat
- spatialheatsource : Ω → (heat_dim) # Q 1
-
+ include ?DeviceGeometry â™
+ include ?Heat â™
+ spatialheatsource : Ω ⟶ (heat_dim) ☠# Q 1 â™
+âš
theory SpatialJouleHeat : top:?Base =
- include ?DeviceGeometry
- include ?Heat
- spatialheatsource : Ω → (heat_dim) # Q_Joule 1
-
+ include ?DeviceGeometry â™
+ include ?Heat â™
+ spatialheatsource : Ω ⟶ (heat_dim) ☠# Q_Joule 1 â™
+âš
theory ThermalConductivity : qe:?QEBase =
- include ?Heat
- // meta modeltype physical_quantity
- thermalconductitvity_dim : type = QE ( Energy /' (SIlength * SItemperature))
- thermalconductitvity : thermalconductitvity_dim
-
+ include ?Heat â™
+ // meta modeltype physical_quantity â™
+ thermalconductitvity_dim : type ☠= QE ( Energy /' (SIlength * SItemperature)) â™
+ thermalconductitvity : thermalconductitvity_dim â™
+âš
theory SpatialThermalConductivity : top:?Base =
- include ?DeviceGeometry
- include ?ThermalConductivity
- spatialthermalconductivity : Ω → (thermalconductitvity_dim) # λ 1
-
+ include ?DeviceGeometry â™
+ include ?ThermalConductivity â™
+ spatialthermalconductivity : Ω ⟶ (thermalconductitvity_dim) ☠# λ 1 â™
+âš
theory ThermalHeatFlux : qe:?QEBase =
- // meta modeltype physical_quantity electricfield_law : {x : Ω} ⊦ E x ≠- ((φ ') x) / unitlengt
- thermalheatflux_dim : type = QE (Energy /' Area)
- thermalheatflux : thermalheatflux_dim
-
+ // meta modeltype physical_quantity electricfield_law : {x : Ω} ⊦ E x ≠- ((φ ') x) / unitlengt â™
+ thermalheatflux_dim : type ☠= QE (Energy /' Area) â™
+ thermalheatflux : thermalheatflux_dim â™
+âš
theory SpatialHeatFluxDensity : top:?Base =
- include ?DeviceGeometry
- include ?ThermalHeatFlux
- heatfluxdensity : Ω → (thermalheatflux_dim) # q 1
-
+ include ?DeviceGeometry â™
+ include ?ThermalHeatFlux â™
+ heatfluxdensity : Ω ⟶ (thermalheatflux_dim) ☠# q 1 â™
+âš
theory SpatialTemperature : top:?Base =
- include ?DeviceGeometry
+ include ?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- potential : Ω → (QE Temperature) # T
-
+ usually denoted by $φ$. â™
+ potential : Ω ⟶ (QE Temperature) ☠# Tâ™
+âš
theory ReferenceTemperature : top:?Base =
-include ?DeviceGeometry
+include ?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- referencetemperature : QE SItemperature # Tref
-
+ usually denoted by $φ$. â™
+ referencetemperature : QE SItemperature ☠# Trefâ™
+âš
theory ActivationEnergy : top:?Base =
-include ?DeviceGeometry
+include ?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- activationenergy : QE Energy # E_act
-
+ usually denoted by $φ$. â™
+ activationenergy : QE Energy ☠# E_actâ™
+âš
theory ElectricFieldLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialElectricField
- include ?SpatialPotential
- electricfield_law : {x : Ω} ⊦ E x ≠-((QEderiv φ) x)
-
+ include ?DeviceGeometry â™
+ include ?SpatialElectricField â™
+ include ?SpatialPotential â™
+ electricfield_law : {x : Ω} ⊦ E x ≠-((QEderiv φ) x) â™
+âš
theory OhmsLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialCurrentDensity
- include ?SpatialElectricField
- include ?SpatialElectricalConductivity
- ohmscurrent_law : {x : Ω} ⊦ j ≠(σ x) ⋅ (E x)
-
+ include ?DeviceGeometry â™
+ include ?SpatialCurrentDensity â™
+ include ?SpatialElectricField â™
+ include ?SpatialElectricalConductivity â™
+ ohmscurrent_law : {x : Ω} ⊦ j ≠(σ x) â‹… (E x) â™
+âš
theory KirchhoffsCurrentLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialCurrentDensity
- kirchhoffscurrent_law : {x : Ω} ⊦ ((QEderiv j) x) ≠0
-
+ include ?DeviceGeometry â™
+ include ?SpatialCurrentDensity â™
+ kirchhoffscurrent_law : {x : Ω} ⊦ ((QEderiv j) x) ≠0â™
+âš
theory JouleHeat : top:?Base =
- include ?DeviceGeometry
- include ?SpatialJouleHeat
- include ?SpatialCurrentDensity
- include ?SpatialElectricField
- jouleheat : {x : Ω} ⊦ Q_Joule ≠(j x) ⋅ (E x)
-
+ include ?DeviceGeometry â™
+ include ?SpatialJouleHeat â™
+ include ?SpatialCurrentDensity â™
+ include ?SpatialElectricField â™
+ jouleheat : {x : Ω} ⊦ Q_Joule ≠(j x) â‹… (E x) â™
+âš
theory FieldEnhancement : top:?Base =
- include ?DeviceGeometry
- include ?SpatialFieldEnhancement
- include ?SpatialElectricField
- include ?SpatialReferenceElectricField
- include ?SpatialLaplacep
+ include ?DeviceGeometry â™
+ include ?SpatialFieldEnhancement â™
+ include ?SpatialElectricField â™
+ include ?SpatialReferenceElectricField â™
+ include ?SpatialLaplacep â™
- fieldenhancement : {x : Ω} ⊦ G ≠|(E x) / (Eref x)|^(p-2)
-
+ fieldenhancement : {x : Ω} ⊦ G ≠|(E x) / (Eref x)|^(p-2) â™
+âš
theory ArrheniusLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialArrheniusFactor
- include ?SpatialActivationEnergy
- include ?ReferenceTemperature
- include ?SpatialTemperature
+ include ?DeviceGeometry â™
+ include ?SpatialArrheniusFactor â™
+ include ?SpatialActivationEnergy â™
+ include ?ReferenceTemperature â™
+ include ?SpatialTemperature â™
- arrhenius_law : {x : Ω} ⊦ F ≠exp( ( E_act / k_B) ⋅ (1 / (T x) - 1 / Tref)
-
+ arrhenius_law : {x : Ω} ⊦ F ≠exp( ( E_act / k_B) â‹… (1 / (T x) - 1 / Tref) â™
+âš
theory ConductivityLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialElectricalConductivity
- include ?SpatialReferenceConductivity
- include ?SpatialArrheniusFactor
- include ?SpatialFieldEnhancement
- include ?ReferenceTemperature
- include ?SpatialTemperature
+ include ?DeviceGeometry â™
+ include ?SpatialElectricalConductivity â™
+ include ?SpatialReferenceConductivity â™
+ include ?SpatialArrheniusFactor â™
+ include ?SpatialFieldEnhancement â™
+ include ?ReferenceTemperature â™
+ include ?SpatialTemperature â™
- conductivity_law : {x : Ω} ⊦ σ ≠(σ_0 x) ⋅ (F x) ⋅ G(x)
-
+ conductivity_law : {x : Ω} ⊦ σ ≠(σ_0 x) â‹… (F x) â‹… G(x) â™
+âš
theory FouriersLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialThermalConductivity
- include ?SpatialTemperature
+ include ?DeviceGeometry â™
+ include ?SpatialThermalConductivity â™
+ include ?SpatialTemperature â™
- conductivity_law : {x : Ω} ⊦ σ ≠(σ_0 x) ⋅ (F x) ⋅ (G x)
-
+ conductivity_law : {x : Ω} ⊦ σ ≠(σ_0 x) â‹… (F x) â‹… (G x) â™
+âš
\ No newline at end of file