module module

`IndisputableMonolith.Cosmology.FermionWeightIntegral`

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 (4)

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

IndisputableMonolith.Cosmology.GrandPotential module_import
IndisputableMonolith.Cosmology.NumberDensityIntegral module_import
IndisputableMonolith.Cosmology.OccupationEnergy module_import
IndisputableMonolith.Cosmology.RadiationEntropyRelation module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.EntropyPerPhoton module_import
IndisputableMonolith.Cosmology.FermionWeight module_import

declarations in this module (19)

def boseKernel L53
def fermiKernel L56
lemma bose_series L61
lemma fermi_series L79
lemma hasSum_zeta_shift L102
lemma hasSum_eta_shift L113
lemma summable_shift_rpow L126
lemma hasSum_mellin_bose L137
lemma hasSum_mellin_fermi L158
lemma gamma_four L183
lemma cpow_shift L190
lemma mellin_bose_value L197
lemma mellin_fermi_value L211
lemma mellin_bose_eq_integral L227
lemma mellin_fermi_eq_integral L242
theorem bose_integral_value L259
theorem fermi_integral_value L266
theorem fermi_div_bose_integral L276
theorem fermi_integral_eq_weight_mul_bose L290