Skip to content
Snippets Groups Projects
Commit be5bebf8 authored by Tom Wiesing's avatar Tom Wiesing :speech_balloon:
Browse files

Automatically replace old LF symbols and delimiters

parent a60a87ac
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 439 additions and 439 deletions
content/http..mathhub.info/MitM/Models/poisson/$Displacement$Law.omdoc
+ 1
− 1
View file @ be5bebf8
<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
content/http..mathhub.info/MitM/Models/thermistor/$Spatial$Reference$Electrical$Field.omdoc
+ 1
− 1
View file @ be5bebf8
<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
source/mmt/Quantities.mmt
+ 45
− 45
View file @ be5bebf8
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
source/mmt/VanRoosbroeck.mmt
+ 11
− 11
View file @ be5bebf8
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
source/mmt/band.mmt
+ 16
− 16
View file @ be5bebf8
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
source/mmt/constants.mmt
+ 25
− 25
View file @ be5bebf8
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 ❙
❚
source/mmt/continuity.mmt
+ 33
− 33
View file @ be5bebf8
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
source/mmt/densities.mmt
+ 17
− 17
View file @ be5bebf8
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
source/mmt/device.mmt
+ 45
− 45
View file @ be5bebf8
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
source/mmt/poisson.mmt
+ 22
− 22
View file @ be5bebf8
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
source/mmt/poissonElectrostatics.mmt
+ 45
− 45
View file @ be5bebf8
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
source/mmt/recombination.mmt
+ 16
− 16
View file @ be5bebf8
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 ❙
❚
source/mmt/species.mmt
+ 13
− 13
View file @ be5bebf8
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
source/thermistor/quantities.mmt
+ 149
− 149
View file @ be5bebf8
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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment