IndisputableMonolith.Gravity.SevenGaps.WickActionEuclidSchlaefli

declarations in this module (24)

• theorem euclidCos_denom_pos L69
• theorem euclidCos_denom_ne L73
• theorem euclidCos_mem_Ioo L80
• theorem euclidCos_abs_lt_one L94
• theorem one_sub_euclidCos_sq_pos L98
• theorem hasDerivAt_mul_sub_const L106
• theorem hasDerivAt_const_sub_mul L113
• theorem hasDerivAt_euclidCos L123
• def euclidAreaFun L145
• theorem hasDerivAt_euclidArea L147
• def euclidAngleDeriv L152
• theorem euclidAngle_deriv_eq L155
• theorem hasDerivAt_euclidAngle L166
• theorem wickActionPath_eq_euclidRegge L175
• theorem wickActionPath_re_eq_euclidRegge L189
• def euclidAngleWeightedArea L197
• theorem hasDerivAt_euclidAngleWeightedArea L202
• theorem euclid_angle_deriv_term_ne_zero_at_one L213
• theorem euclidSchlaefli_holds L234
• theorem euclidSchlaefli_field_inhabited L262
• theorem euclidSchlaefli_field_inhabited_one L266
• structure WickActionEuclidSchlaefliStatus L272
• def wickActionEuclidSchlaefliStatus L282
• theorem wickActionEuclidSchlaefliStatus_flags L288