IndisputableMonolith.Cosmology.RadiationEntropyRelation

declarations in this module (29)

• def boseLogKernel L72
• def fermiLogKernel L77
• lemma boseLog_series L81
• lemma fermiLog_series L92
• lemma summable_norm_boseLog L110
• lemma summable_norm_fermiLog L124
• lemma hasSum_mellin_boseLog L139
• lemma hasSum_mellin_fermiLog L163
• lemma mellin_boseLog_value L190
• lemma mellin_fermiLog_value L205
• lemma mellin_boseLog_eq_integral L223
• lemma mellin_fermiLog_eq_integral L238
• theorem boseLog_integral_value L255
• theorem fermiLog_integral_value L262
• def boseEntropyIntegrand L272
• def fermiEntropyIntegrand L278
• lemma bose_entropy_pointwise L285
• lemma fermi_entropy_pointwise L313
• lemma integrableOn_bose_energy L338
• lemma integrableOn_boseLog L349
• lemma integrableOn_fermi_energy L361
• lemma integrableOn_fermiLog L372
• theorem bose_entropy_integral_value L386
• theorem fermi_entropy_integral_value L399
• theorem bose_entropy_eq_four_thirds_energy L416
• theorem fermi_entropy_eq_four_thirds_energy L425
• theorem fermi_div_bose_entropy L435
• theorem fermi_entropy_eq_weight_mul_bose L445
• theorem entropy_coeff_from_functional L459