module module

`IndisputableMonolith.Verification.NANOGravPTALikelihood`

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

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

IndisputableMonolith.Verification.FalsifierLikelihoodRegister module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.FalsifierRegisterDatasets module_import

declarations in this module (16)

def nanogravBetaLower95 L46
def nanogravBetaUpper95 L49
def nanogravBetaMidpoint L52
def nanogravBetaHalfWidth95 L55
def nanogravRSTarget L58
def nanogravPTAResidual L61
theorem nanogravBetaHalfWidth95_pos L64
theorem nanogravRSTarget_pos L68
theorem nanograv_rs_target_inside_95_interval L75
theorem nanograv_residual_lt_half_width L82
theorem nanograv_half_width_gt_rs_target L90
theorem nanograv_dataset_attachment_status L98
structure NANOGravPTALikelihoodCert L106
def nanogravPTALikelihoodCert L121
theorem nanogravPTALikelihoodCert_inhabited L129
theorem nanograv_pta_likelihood_one_statement L134