module module

`IndisputableMonolith.Cosmology.StatisticsKernels`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.PhaseSpaceReduction module_import

declarations in this module (31)

def boltzmannWeight L71
def bosePartition L75
def fermiPartition L79
def boseOccupation L83
def fermiOccupation L87
lemma boltzmannWeight_pow L91
lemma exp_neg_lt_one L97
lemma one_lt_exp L100
theorem bosePartition_eq L108
theorem fermiPartition_eq L117
lemma bosePartition_pos L122
lemma fermiPartition_pos L127
theorem boseLogKernel_eq_log_partition L136
theorem fermiLogKernel_eq_log_partition L143
theorem boseOccupation_eq L153
theorem fermiOccupation_eq L173
theorem fermiOccupation_lt_one L189
theorem boseOccupation_pos L196
theorem boseEnergyKernel_eq_occupation L205
theorem fermiEnergyKernel_eq_occupation L212
theorem boseLogKernel_hasDerivAt L224
theorem fermiLogKernel_hasDerivAt L249
theorem boseEnergyKernel_from_logKernel L272
theorem fermiEnergyKernel_from_logKernel L278
theorem mode_energy_bose L288
theorem mode_energy_fermi L304
lemma phaseSpaceDensity_congr_pos L322
theorem plasmaPressure_from_partitionFunction L339
theorem plasmaEnergy_from_occupation L356
theorem number_integrand_bose L374
theorem number_integrand_fermi L380