module module

`IndisputableMonolith.Cosmology.Inflation`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (24)

def inflatonPotential L48
theorem potential_min_at_one L51
theorem potential_positive L59
def slowRollEpsilon L68
def slowRollEta L77
theorem slow_roll_at_large_phi L85
def eFoldings L94
theorem sixty_efolds L100
theorem horizon_problem_solved L109
theorem flatness_problem_solved L116
theorem monopole_problem_solved L122
def powerSpectrum L130
def spectralIndex L137
theorem nearly_scale_invariant L142
def tensorScalarRatio L148
theorem small_tensor_modes L153
structure Reheating L161
theorem efficient_reheating L169
theorem inflation_is_cost_relaxation L184
structure InflationPredictions L195
def rsPredictions L201
def planckMeasurements L208
structure InflationFalsifier L218
def experimentalStatus L225