def
definition
def or abbrev
ppnInverseStub
show as:
view Lean formalization →
formal statement (Lean)
75noncomputable def ppnInverseStub : PPNInverseFacts where
76 inverse_approx := by
proof body
Definition body.
77 intro pots params x μ ρ
78 simpa using show |(0 : ℝ)| < 0.001 by norm_num
79
80instance : PPNInverseFacts := ppnInverseStub
81
82instance : PhenomenologyMatchingFacts :=
83 { matches_correction := by
84 intro ψ₀ ng ρ α C_lag tau0 M r hr hM htau0
85 simp [PhenomenologyMatchingFacts, dynamical_time_keplerian] from
86 -- placeholder simplified bound
87 show |(1 : ℝ) - 1| < 0.1 by norm_num }
88
89instance : SphericalWeightFacts :=
90 { param_identification := by simp [SphericalWeightFacts, lambda_phenom, xi_phenom, n_phenom, zeta_phenom, C_lag_RS, alpha_RS] }
91