IndisputableMonolith.Gravity.GravitationalLensing

declarations in this module (16)

• def schwarzschild_radius L29
• def lensing_param L32
• def deflection_newtonian L38
• def deflection_GR L42
• theorem gr_is_twice_newton L47
• theorem deflection_angle_formula L59
• theorem deflection_positive L65
• theorem deflection_inverse_b L71
• def einstein_angle_sq L87
• theorem einstein_radius_positive L91
• def shapiro_delay L102
• theorem shapiro_delay_positive L106
• def solar_deflection L122
• theorem solar_deflection_positive L126
• def ilg_convergence_correction L139
• theorem ilg_correction_enhances L143