Thermistor model: alle Quantities, ein ElectricFieldLaw, Ableitung mit Einheiten fehlen

source/thermistor/quantities.mmt

+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 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  # Ω 
+
+
+theory SpatialPotential : top:?Base =
+  include ?DeviceGeometry 
+  /T Spatial variation of the potential,
+	   usually denoted by $φ$. 
+	potential : Ω → (QE ElectricPotential)  # φ	
+
+
+theory ElectricFieldStrength : qe:?QEBase =
+  electricfieldstrength_dim : type  = QE (ElectricPotential /' SIlength) 
+  electricfieldstrength : electricfieldstrength_dim 
+
+
+	
+theory SpatialElectricField : top:?Base =
+  include ?DeviceGeometry 
+  include ?ElectricFieldStrength 
+  /T Spatial variation of the electric field strength,
+	   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 
+
+	
+	
+theory SpatialCurrentDensity : top:?Base =
+  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 
+
+	
+	
+theory SpatialElectricalConductivity : top:?Base =
+  include ?DeviceGeometry 
+  include ?ElectricalConductivity 
+	spatialelectricalconductivity : Ω → (electricalconductitvity_dim)  # σ 1 
+
+
+theory Heat : qe:?QEBase =
+  // 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 
+
+
+theory SpatialJouleHeat : top:?Base =
+  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 
+
+	
+theory SpatialThermalConductivity : top:?Base =
+  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 
+
+	
+theory SpatialHeatFluxDensity : top:?Base =
+  include ?DeviceGeometry 
+  include ?ThermalHeatFlux 
+	heatfluxdensity : Ω → (thermalheatflux_dim)  # q 1 
+
+	  
+theory ElectricFieldLaw : top:?Base =
+  include ?DeviceGeometry 
+  include ?SpatialElectricField  
+  include ?SpatialPotential 
+	electricfield_law : {x : Ω} ⊦ E x ≐ -((QEderiv φ) x) 
+
+
+  
\ No newline at end of file