def
definition
BoundaryConditions
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Compact.StaticSpherical on GitHub at line 141.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
138 linarith
139 exact h_goal
140
141def BoundaryConditions (metric : StaticSphericalMetric) : Prop :=
142 (∀ ε > 0, ∃ R, ∀ r > R, |metric.f r - 1| < ε) ∧
143 (∀ ε > 0, ∃ R, ∀ r > R, |metric.g r - 1| < ε)
144
145/-!
146Schwarzschild limit (documentation / TODO).
147
148Intended claim: in the appropriate parameter regime, solutions reduce to the Schwarzschild metric.
149-/
150
151end Compact
152end Relativity
153end IndisputableMonolith