def
definition
falsifiers_default
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.ILG.Falsifiers on GitHub at line 19.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
16 0 ≤ f.ppn_tight ∧ 0 ≤ f.lensing_band ∧ 0 ≤ f.gw_band
17
18/-- Default admissible bands (illustrative). -/
19def falsifiers_default : Falsifiers :=
20 { ppn_tight := (1/100000 : ℝ)
21 , lensing_band := 1
22 , gw_band := (1/1000000 : ℝ) }
23
24@[simp] theorem falsifiers_default_ok : falsifiers_ok falsifiers_default := by
25 simp [falsifiers_ok, falsifiers_default]
26 repeat' constructor <;> norm_num
27
28end ILG
29end Relativity
30end IndisputableMonolith