def
definition
proof_requirements
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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