def
definition
falsifiers_ok
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.ILG.Falsifiers on GitHub at line 15.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
12 deriving Repr
13
14/-- Predicate that falsifier bands are nonnegative (admissible). -/
15def falsifiers_ok (f : Falsifiers) : Prop :=
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