IndisputableMonolith.Gravity.SevenGaps.WickActionCutLimitFamily

declarations in this module (43)

• def lorentzK L45
• theorem lorentzCos_eq_neg_lorentzK L47
• theorem lorentzK_den_pos L52
• theorem lorentzK_gt_one L57
• theorem lorentzK_pos L64
• theorem lorentzK_sq_sub_one_pos L68
• theorem sqrt_lorentzK_sq_sub_one_lt L73
• theorem rapidityPinned_of_causal L81
• theorem continuous_arcZ L90
• theorem tendsto_pentHingeCosPath_of_causal L100
• lemma lorentzK_sq_sub_one_mem_slitPlane L161
• theorem tendsto_csqrt_sq_sub_one_of_causal L166
• lemma eventually_ioo_of_nhdsWithin_zero L201
• lemma eventually_re_pent_neg L208
• lemma eventually_im_pent_neg L216
• lemma eventually_im_one_sub_sq_neg L222
• theorem eventually_carccos_log_arg_eq_of_causal L239
• lemma eventually_csqrt_re_pos L258
• lemma eventually_csqrt_add_re_neg L271
• lemma eventually_sq_sub_one_ne L292
• theorem eventually_im_log_arg_nonneg_of_causal L307
• def u0 L341
• lemma u0_eq_ofReal L344
• lemma u0_re L350
• lemma u0_im L355
• lemma u0_re_neg L359
• lemma tendsto_log_arg_to_u0 L364
• lemma tendsto_log_arg_nhdsWithin_im_nonneg L373
• lemma tendsto_log_of_log_arg L383
• lemma norm_u0 L395
• lemma log_norm_u0_eq_neg_arcosh L403
• theorem carccos_tendsto_at_cut_of_causal L419
• theorem carccos_tendsto_at_cut_family_holds L475
• theorem lorentzAnchor_of_causal L480
• theorem euclidCos_lt_one L531
• theorem euclidCos_gt_neg_one L540
• theorem offArccosCut_pentHingeCosPath_Ioc_of_causal L554
• theorem continuousOn_pentHingeCosPath_Ioc_of_causal L566
• theorem continuousOn_carccos_comp_pent_Ioc_of_causal L584
• theorem continuousOn_wickActionPath_Ioc_of_causal L593
• structure WickActionCutLimitFamilyStatus L620
• def wickActionCutLimitFamilyStatus L628
• theorem wickActionCutLimitFamilyStatus_flags L636