module
module
IndisputableMonolith.Verification.CassiniStrongFieldLikelihood
show as:
view Lean formalization →
used by (1)
depends on (2)
declarations in this module (13)
-
def
cassiniGammaMinusOneCentral -
def
cassiniGammaSigma -
def
cassiniRSTargetScale -
def
cassiniStrongFieldResidual -
theorem
cassiniGammaSigma_pos -
theorem
cassiniRSTargetScale_pos -
theorem
cassini_residual_lt_one_sigma -
theorem
cassini_sigma_gt_rs_target -
theorem
cassini_dataset_attachment_status -
structure
CassiniStrongFieldLikelihoodCert -
def
cassiniStrongFieldLikelihoodCert -
theorem
cassiniStrongFieldLikelihoodCert_inhabited -
theorem
cassini_strong_field_likelihood_one_statement