IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimit

declarations in this module (33)

• theorem csqrt_of_im_neg L38
• theorem tendsto_pentHingeCosPath_one L65
• lemma sq_sub_one_limit L108
• lemma fiftySevenOver64_mem_slitPlane L112
• lemma sqrt_fiftySeven_div_eight L118
• theorem tendsto_csqrt_sq_sub_one_one L128
• lemma eventually_ioo_of_nhdsWithin_zero L160
• lemma eventually_re_pent_neg L167
• lemma eventually_im_pent_neg L174
• lemma eventually_im_one_sub_sq_neg L180
• theorem eventually_carccos_log_arg_eq L196
• lemma eventually_csqrt_re_pos L214
• lemma eventually_csqrt_add_re_neg L225
• lemma eventually_sq_sub_one_ne L248
• theorem eventually_im_log_arg_nonneg L261
• def u0 L294
• lemma u0_eq_ofReal L296
• lemma u0_re L301
• lemma u0_im L305
• lemma sqrt57_lt_11 L309
• lemma u0_re_neg L313
• lemma tendsto_log_arg_to_u0 L317
• lemma tendsto_log_arg_nhdsWithin_im_nonneg L326
• lemma tendsto_log_of_log_arg L335
• lemma norm_u0 L346
• lemma log_norm_u0_eq_neg_arcosh L353
• theorem carccos_tendsto_at_cut_one_holds L378
• theorem carccos_tendsto_at_cut_one_inhabited L434
• theorem lorentzAnchor_one_holds L437
• theorem lorentzAnchor_one_inhabited L482
• structure WickActionCutLimitStatus L485
• def wickActionCutLimitStatus L492
• theorem wickActionCutLimitStatus_flags L499