def
definition
proof_requirements
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.NonlinearConvergence on GitHub at line 150.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
147
148 This is a multi-year project for the Mathlib community.
149 We axiomatize instead, clearly labeling the axioms. -/
150def proof_requirements : List String :=
151 [ "Simplicial geometry (Cayley-Menger)"
152 , "Schläfli identity"
153 , "Comparison geometry (smooth vs piecewise-flat)"
154 , "Curvature error analysis"
155 , "Compactness and convergence extraction" ]
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