IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily

declarations in this module (27)

• def dsFamilyModelName L53
• def dsFamilyMemberCount L54
• def dsFamilyEventCount L55
• def dsFamilyTotalSampleCount L56
• def dsRSDampingTarget L57
• def dsPooledMean L58
• def dsPooledStd L59
• def dsPooledMedian L60
• def dsPooledQ05 L61
• def dsPooledQ16 L62
• def dsPooledQ84 L63
• def dsPooledQ95 L64
• def dsPooledZFromMean L65
• def dsPooledFractionBelowTarget L66
• def dsMembersInside68Count L67
• theorem ds_family_member_count_matches_taxonomy L71
• theorem ds_family_event_count_pos L74
• theorem ds_family_sample_count_pos L78
• theorem ds_target_inside_pooled_90 L82
• theorem ds_target_inside_pooled_68 L87
• theorem ds_z_from_mean_lt_one L92
• theorem ds_fraction_below_target_valid L97
• theorem ds_members_inside68_nonzero L102
• structure GWTC3RingdownDS1Mode10MDampingFamilyCert L109
• def gwtc3RingdownDS1Mode10MDampingFamilyCert L126
• theorem gwtc3RingdownDS1Mode10MDampingFamilyCert_inhabited L139
• theorem gwtc3_ringdown_ds1mode10m_damping_family_one_statement L144