structure
definition
ConfigProps
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.ILG on GitHub at line 35.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
32 , eps_t := 0.01
33 , eps_a := 1e-12 }
34
35structure ConfigProps (cfg : Config) : Prop where
36 eps_t_nonneg : 0 ≤ cfg.eps_t
37 eps_t_le_one : cfg.eps_t ≤ 1
38
39@[simp] lemma defaultConfig_props : ConfigProps defaultConfig := by
40 refine ⟨?h0, ?h1⟩ <;> norm_num
41
42def vbarSq_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
43 max 0 ((C.vgas r) ^ 2 + ((Real.sqrt cfg.upsilonStar) * (C.vdisk r)) ^ 2 + (C.vbul r) ^ 2)
44
45def vbar_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
46 Real.sqrt (max cfg.eps_v (vbarSq_with cfg C r))
47
48def gbar_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
49 (vbar_with cfg C r) ^ 2 / max cfg.eps_r r
50
51structure Params where
52 alpha : ℝ
53 Clag : ℝ
54 A : ℝ
55 r0 : ℝ
56 p : ℝ
57 hz_over_Rd : ℝ
58
59structure ParamProps (P : Params) : Prop where
60 alpha_nonneg : 0 ≤ P.alpha
61 Clag_nonneg : 0 ≤ P.Clag
62 Clag_le_one : P.Clag ≤ 1
63 A_nonneg : 0 ≤ P.A
64 r0_pos : 0 < P.r0
65 p_pos : 0 < P.p