IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily

declarations in this module (28)

• def kerr2200ModelName L59
• def kerr2200MemberCount L60
• def kerr2200EventCount L61
• def kerr2200TotalSampleCount L62
• def kerr2200RSDampingTarget L63
• def kerr2200PooledMean L64
• def kerr2200PooledStd L65
• def kerr2200PooledMedian L66
• def kerr2200PooledQ05 L67
• def kerr2200PooledQ16 L68
• def kerr2200PooledQ84 L69
• def kerr2200PooledQ95 L70
• def kerr2200PooledZFromMean L71
• def kerr2200PooledFractionBelowTarget L72
• def kerr2200MembersInside68Count L73
• theorem kerr2200_member_count_pos L77
• theorem kerr2200_event_count_pos L81
• theorem kerr2200_sample_count_pos L85
• theorem kerr2200_target_inside_pooled_90 L89
• theorem kerr2200_target_not_inside_pooled_68 L95
• theorem kerr2200_z_from_mean_gt_one L100
• theorem kerr2200_fraction_below_target_valid L105
• theorem kerr2200_members_inside68_nonzero L110
• theorem ds_vs_kerr_mean_order L115
• structure GWTC3RingdownKerr2200MDampingFamilyCert L122
• def gwtc3RingdownKerr2200MDampingFamilyCert L141
• theorem gwtc3RingdownKerr2200MDampingFamilyCert_inhabited L155
• theorem gwtc3_ringdown_kerr2200m_damping_family_one_statement L160