module module

`IndisputableMonolith.Verification.GWTC3RingdownOneMemberRSStatistic`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary module_import

declarations in this module (22)

def rsLogPhiNeg44Target L52
def logAPosteriorMean L53
def logAPosteriorStd L54
def logAPosteriorMedian L55
def logAQ05 L56
def logAQ16 L57
def logAQ84 L58
def logAQ95 L59
def logAResidualFromMean L60
def logAResidualFromMedian L61
def logAZFromMean L62
def logAFractionAboveTarget L63
theorem target_above_q95 L67
theorem target_outside_90_interval L72
theorem target_outside_68_interval L78
theorem z_from_mean_gt_two L84
theorem fraction_above_target_small L89
theorem posterior_summary_available L94
structure GWTC3RingdownOneMemberRSStatisticCert L100
def gwtc3RingdownOneMemberRSStatisticCert L110
theorem gwtc3RingdownOneMemberRSStatisticCert_inhabited L119
theorem gwtc3_ringdown_one_member_rs_statistic_one_statement L124