 156
 157/-! ## Certificate -/
 158
 159structure NonlinearConvergenceCert where
 160  second_order : ∀ a : ℝ, 0 < a → a < 1 → (a/2)^2 = a^2/4
 161  error_goes_to_zero : ∀ C : ℝ, 0 < C →
 162    Filter.Tendsto (fun a => C * a ^ 2) (nhds 0) (nhds 0)
 163  kappa : rs_kappa = 8 * phi ^ 5
 164
 165theorem nonlinear_convergence_cert : NonlinearConvergenceCert where
 166  second_order := fun _ _ _ => convergence_is_second_order _ (by linarith) (by linarith)
 167  error_goes_to_zero := error_vanishes
 168  kappa := rs_kappa_value
 169
 170end
 171
 172end NonlinearConvergence
 173end Gravity
 174end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.