No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
54def ParallelTransported (g : MetricTensor) (γ : SpacetimeCurve)
55 (V : ℝ → (Fin 4 → ℝ)) : Prop :=
proof body
Definition body.
56 ∀ lam μ,
57 deriv (fun l => V l μ) lam +
58 Finset.univ.sum (fun α =>
59 Finset.univ.sum (fun β =>
60 christoffel g (γ.path lam) μ α β *
61 γ.tangent lam α *
62 V lam β)) = 0
63
64/-- Smoothness of a vector field along the affine parameter. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (15)
Lean names referenced from this declaration's body.
-
christoffel
in IndisputableMonolith.Action.EulerLagrange
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
MetricTensor
in IndisputableMonolith.Foundation.Hamiltonian
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
MetricTensor
in IndisputableMonolith.Gravity.Connection
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
MetricTensor
in IndisputableMonolith.Meta.Homogenization
decl_use
-
christoffel
in IndisputableMonolith.Relativity.Geometry.Curvature
decl_use
-
MetricTensor
in IndisputableMonolith.Relativity.Geometry.Metric
decl_use
-
SpacetimeCurve
in IndisputableMonolith.Relativity.Geometry.ParallelTransport
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use