module module

`IndisputableMonolith.Verification.GWTC3RingdownOneMemberDampingStatistic`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary module_import

declarations in this module (23)

def rsDampingTarget L37
def dampingMean L38
def dampingStd L39
def dampingMedian L40
def dampingQ05 L41
def dampingQ16 L42
def dampingQ84 L43
def dampingQ95 L44
def dampingResidualFromMean L45
def dampingZFromMean L46
def dampingFractionBelowTarget L47
def ftauMean L48
def rsFtauTarget L49
theorem damping_target_inside_90_interval L53
theorem damping_target_inside_68_interval L58
theorem damping_z_from_mean_lt_one L63
theorem damping_fraction_below_target_between_zero_and_one L68
theorem ftau_mean_gt_rs_target L73
theorem sample_summary_available L78
structure GWTC3RingdownOneMemberDampingStatisticCert L84
def gwtc3RingdownOneMemberDampingStatisticCert L95
theorem gwtc3RingdownOneMemberDampingStatisticCert_inhabited L104
theorem gwtc3_ringdown_one_member_damping_statistic_one_statement L109