module module

`IndisputableMonolith.Verification.GWTC3RingdownFamilyComparison`

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.GWTC3RingdownLikelihoodSelector module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily module_import
IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily module_import
IndisputableMonolith.Verification.GWTC3RingdownKerr22010MDampingFamily module_import

declarations in this module (18)

def comparisonFamilyCount L41
def comparisonTotalMembers L42
def comparisonTotalSamples L43
def dsMeanMinusKerr0Mean L44
def kerr0MeanMinusKerr10Mean L45
def dsHitDiffVsKerr0 L46
def kerr0HitDiffVsKerr10 L47
theorem comparison_total_members L51
theorem comparison_total_samples L57
theorem family_mean_order L64
theorem family_median_order L69
theorem hit_count_order L75
theorem ds_mean_difference_pos L81
theorem kerr_mean_difference_pos L86
structure GWTC3RingdownFamilyComparisonCert L93
def gwtc3RingdownFamilyComparisonCert L113
theorem gwtc3RingdownFamilyComparisonCert_inhabited L124
theorem gwtc3_ringdown_family_comparison_one_statement L129