IndisputableMonolith.Verification.GWTC3RingdownKerr22010MDampingFamily

declarations in this module (28)

• def kerr22010ModelName L42
• def kerr22010MemberCount L43
• def kerr22010EventCount L44
• def kerr22010TotalSampleCount L45
• def kerr22010RSDampingTarget L46
• def kerr22010PooledMean L47
• def kerr22010PooledStd L48
• def kerr22010PooledMedian L49
• def kerr22010PooledQ05 L50
• def kerr22010PooledQ16 L51
• def kerr22010PooledQ84 L52
• def kerr22010PooledQ95 L53
• def kerr22010PooledZFromMean L54
• def kerr22010PooledFractionBelowTarget L55
• def kerr22010MembersInside68Count L56
• theorem kerr22010_member_count_pos L60
• theorem kerr22010_event_count_pos L64
• theorem kerr22010_sample_count_pos L68
• theorem kerr22010_target_above_pooled_95 L72
• theorem kerr22010_target_above_pooled_84 L77
• theorem kerr22010_z_from_mean_gt_two L82
• theorem kerr22010_fraction_below_target_valid L87
• theorem kerr22010_no_members_inside68 L92
• theorem kerr22010_mean_lt_kerr2200_mean L95
• structure GWTC3RingdownKerr22010MDampingFamilyCert L102
• def gwtc3RingdownKerr22010MDampingFamilyCert L115
• theorem gwtc3RingdownKerr22010MDampingFamilyCert_inhabited L128
• theorem gwtc3_ringdown_kerr22010m_damping_family_one_statement L133