structure definition def or abbrev

`NonlinearConvergenceCert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

nonlinear_convergence_cert in IndisputableMonolith.Gravity.NonlinearConvergence decl_use

depends on (3)

Lean names referenced from this declaration's body.

rs_kappa in IndisputableMonolith.Gravity.ReggeCalculus decl_use
kappa in IndisputableMonolith.Materials.ThermalConductivityRegimesFromPhiLadder decl_use
kappa in IndisputableMonolith.NumberTheory.AnnularCost decl_use