module module

`IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary`

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

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Verification.GWTC3RingdownOneMemberDampingStatistic module_import
IndisputableMonolith.Verification.GWTC3RingdownOneMemberRSStatistic module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSchema module_import

declarations in this module (30)

def summaryMemberName L37
def summaryPosteriorPath L38
def summarySampleCount L39
def summaryFieldCount L40
def psiMean L42
def logAMean L43
def fMean L44
def tauMean L45
def phiMean L46
def logLMean L47
def logPriorMean L48
def fQ16 L50
def fMedian L51
def fQ84 L52
def tauQ16 L54
def tauMedian L55
def tauQ84 L56
theorem summary_member_matches_schema L60
theorem summary_path_matches_schema L63
theorem summary_sample_count_matches_schema L66
theorem summary_field_count_matches_schema L69
theorem summary_sample_count_pos L72
theorem summary_field_count_pos L76
theorem mean_signs L80
theorem f_quantile_order L86
theorem tau_quantile_order L91
structure GWTC3RingdownHDF5SampleSummaryCert L98
def gwtc3RingdownHDF5SampleSummaryCert L112
theorem gwtc3RingdownHDF5SampleSummaryCert_inhabited L125
theorem gwtc3_ringdown_hdf5_sample_summary_one_statement L130