Documentation Verification Report

Basic

📁 Source: PhysLean/Cosmology/FLRW/Basic.lean

Statistics

Metric	Count
Definitions `FLRW`, `FirstOrderFriedmann`, `SecondOrderFriedmann`, `decelerationParameter`, `decelerationParameter_eq_one_plus_hubbleConstant`, `hubbleConstant`, `hubbleConstant_decrease_iff`, `time_evolution_hubbleConstant`, `SpatialGeometry`, `S`	10
Theorems `limit_S_saddle`, `limit_S_sphere`, `mul_sin_as_div`, `mul_sinh_as_div`, `tendsto_sin_rx_over_x`, `tendsto_sinh_rx_over_x`	6
Total	16
⚠️ With sorry `FLRW`	1

Cosmology

Definitions

Name	Category	Theorems
`FLRW` 📖 ⚠️	CompOp	—
`SpatialGeometry` 📖	CompData	—

Cosmology.FLRW.FriedmannEquation

Definitions

Name	Category	Theorems
`FirstOrderFriedmann` 📖	MathDef	—
`SecondOrderFriedmann` 📖	MathDef	—
`decelerationParameter` 📖	CompOp	—
`decelerationParameter_eq_one_plus_hubbleConstant` 📖	CompOp	—
`hubbleConstant` 📖	CompOp	—
`hubbleConstant_decrease_iff` 📖	CompOp	—
`time_evolution_hubbleConstant` 📖	CompOp	—

Cosmology.SpatialGeometry

Definitions

Name	Category	Theorems
`S` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`limit_S_saddle` 📖	—	—	—	—	—
`limit_S_sphere` 📖	—	—	—	—	—
`mul_sin_as_div` 📖	—	—	—	—	—
`mul_sinh_as_div` 📖	—	—	—	—	—
`tendsto_sin_rx_over_x` 📖	—	—	—	—	—
`tendsto_sinh_rx_over_x` 📖	—	—	—	—	—

---

← Back to Index