module module

`IndisputableMonolith.Cosmology.PhaseSpaceReduction`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cosmology.PartitionKernels module_import
IndisputableMonolith.Cosmology.StatisticsKernels module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.GrandPotential module_import

declarations in this module (15)

def phaseSpaceDensity L77
def boseLogKernel L81
def fermiLogKernel L84
def boseEnergyKernel L87
def fermiEnergyKernel L90
theorem integral_norm_fin_three L98
theorem radial_scale_pow L116
theorem phaseSpaceDensity_reduction L149
theorem plasmaPressure_from_phaseSpace L171
theorem plasmaEnergy_from_phaseSpace L182
theorem phaseSpacePressure_closed_form L200
theorem phaseSpaceEnergy_closed_form L208
theorem phaseSpaceDensity_T_scaling L226
theorem stefan_boltzmann_from_D3 L252
theorem phaseSpacePressure_potential L269