IndisputableMonolith.QFT.LambShift

declarations in this module (33)

• def lambShift_MHz L39
• theorem lamb_shift_approx L42
• def alpha_approx L48
• theorem alpha_value L51
• def lambShiftFraction L55
• theorem lamb_shift_tiny L58
• def s_wave_at_origin_nonzero L67
• def p_wave_at_origin_zero L71
• def s_wave_l L74
• def p_wave_l L77
• theorem orbital_angular_momentum L80
• theorem s_wave_penetrates_nucleus L86
• theorem p_wave_excluded_from_origin L92
• def e_2S_eV L100
• def e_2P_eV L103
• def dirac_degeneracy L106
• theorem dirac_prediction L109
• def lamb_shift_ueV L112
• theorem s_higher_than_p_by_lamb_shift L115
• def experimental_uncertainty L123
• def theoretical_uncertainty L126
• theorem theory_more_precise L129
• theorem uncertainties_small L135
• def significant_figures L142
• theorem precision_agreement L145
• def alpha_power_in_formula L154
• theorem alpha_fifth_power L157
• theorem alpha_fifth_small L161
• def rsInterpretation L170
• def potentialSmearin L175
• structure LambShiftProofs L186
• def lambShiftProofs L194
• def relatedEffects L204