IndisputableMonolith.Cosmology.EntropyPerPhoton

declarations in this module (43)

• def gPhoton L81
• def gElectron L84
• def gNeutrino L87
• def fermionWeight L99
• def gBefore L103
• def gAfter L106
• def dilutionCubed L119
• theorem dilutionCubed_eq L121
• def gStarS L127
• theorem gStarS_eq L130
• def zeta3 L141
• lemma zeta3_summable L143
• lemma tail_summable L150
• lemma zeta3_split L158
• def gLo L172
• lemma gLo_nonneg L174
• lemma gLo_tendsto L176
• lemma gLo_step L183
• lemma gLo_antitone L191
• lemma hasSum_gLo L196
• lemma term_lo L203
• lemma tail_ge L210
• def gHi L217
• lemma gHi_tendsto L219
• lemma gHi_step L227
• lemma gHi_antitone L235
• lemma hasSum_gHi L240
• lemma term_hi L247
• lemma tail_le L254
• lemma S40_gt L260
• lemma S40_lt L264
• theorem zeta3_gt L271
• theorem zeta3_lt L278
• theorem zeta3_pos L284
• theorem pi4_gt L289
• theorem pi4_lt L297
• def entropyPerPhoton L308
• theorem entropyPerPhoton_eq_formula L312
• theorem entropyPerPhoton_eq_ratio L320
• theorem entropyPerPhoton_gt L329
• theorem entropyPerPhoton_lt L338
• theorem entropyPerPhoton_pos L346
• theorem entropyPerPhoton_near_704 L352