def
definition
no_background_modification
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Cosmology.Buchert on GitHub at line 43.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
40
41/-- The "No Background Modification" result: because Q_D = 0, the background
42 expansion (H) remains that of the chosen matter content. -/
43def no_background_modification (H f δ : ℝ) : Prop :=
44 localBackreaction (-H * f * δ) ((1/3 : ℝ) * (H * f * δ)^2) = 0
45
46theorem background_is_stable (H f δ : ℝ) : no_background_modification H f δ :=
47 buchert_cancellation H f δ
48
49end Cosmology
50end Relativity
51end IndisputableMonolith