IndisputableMonolith.Verification.OmegaLambdaPlanckLikelihood

declarations in this module (13)

• def planckOmegaLambdaCentral L43
• def planckOmegaLambdaSigma L46
• def omegaLambdaPlanckResidual L49
• def planckOmegaLambdaTwoSigma L53
• theorem planckOmegaLambdaSigma_pos L56
• theorem planckOmegaLambdaTwoSigma_pos L60
• theorem omegaLambda_residual_lt_two_sigma L67
• theorem omegaLambda_in_planck_two_sigma_interval L74
• theorem omegaLambda_dataset_attachment_active L84
• structure OmegaLambdaPlanckLikelihoodCert L92
• def omegaLambdaPlanckLikelihoodCert L105
• theorem omegaLambdaPlanckLikelihoodCert_inhabited L112
• theorem omega_lambda_planck_likelihood_one_statement L117