def
definition
deflectionAngle
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.GravitationalLensingFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
25
26theorem lensingRegime_count : Fintype.card LensingRegime = 5 := by decide
27
28noncomputable def deflectionAngle (k : ℕ) : ℝ := phi ^ k
29
30theorem deflection_ratio (k : ℕ) :
31 deflectionAngle (k + 1) / deflectionAngle k = phi := by
32 unfold deflectionAngle
33 have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
34 rw [div_eq_iff hpos.ne', pow_succ]
35 ring
36
37theorem deflection_pos (k : ℕ) : 0 < deflectionAngle k := pow_pos phi_pos k
38
39structure GravitationalLensingCert where
40 five_regimes : Fintype.card LensingRegime = 5
41 phi_ratio : ∀ k, deflectionAngle (k + 1) / deflectionAngle k = phi
42 deflection_always_pos : ∀ k, 0 < deflectionAngle k
43
44noncomputable def gravitationalLensingCert : GravitationalLensingCert where
45 five_regimes := lensingRegime_count
46 phi_ratio := deflection_ratio
47 deflection_always_pos := deflection_pos
48
49end IndisputableMonolith.Cosmology.GravitationalLensingFromRS