module module

`IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSchema`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownZipSchema module_import

declarations in this module (23)

def sampleMemberName L51
def sampleCompressedSize L52
def sampleUncompressedSize L53
def sampleLocalHeaderOffset L54
def sampleDataOffset L55
def sampleHDF5ObjectCount L56
def sampleGroupCount L57
def sampleDatasetCount L58
def sampleRootAttrCount L59
def posteriorSamplesDatasetPath L60
def posteriorSamplesCount L61
def posteriorFieldCount L62
theorem sample_sizes_pos L66
theorem sample_uncompressed_gt_compressed L71
theorem sample_object_count_split L76
theorem sample_posterior_samples_nonempty L81
theorem sample_posterior_field_count_pos L86
theorem sample_member_is_h5 L91
theorem sample_posterior_dataset_named L94
structure GWTC3RingdownHDF5SampleSchemaCert L99
def gwtc3RingdownHDF5SampleSchemaCert L117
theorem gwtc3RingdownHDF5SampleSchemaCert_inhabited L128
theorem gwtc3_ringdown_hdf5_sample_schema_one_statement L133