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)
388theorem deriv_coordRay_j (x : Fin 4 → ℝ) (i j : Fin 4) (h : j ≠ i) :
389 deriv (fun t => (coordRay x i t) j) 0 = 0 := by
proof body
Term-mode proof.
390 simp only [coordRay_apply, basisVec_ne h, mul_zero, add_zero]
391 exact deriv_const 0 (x j)
392
393/-- **THEOREM**: Functional derivative of spatialNormSq.
394 ∂_μ (∑ x_i²) = 2 x_μ for μ ∈ {1,2,3}, else 0.
395
396 **Derivation**: Using the chain rule and ∂_μ(x_i²) = 2x_i δ_{iμ}, we get:
397 ∂_μ(x₁² + x₂² + x₃²) = 2x₁δ_{1μ} + 2x₂δ_{2μ} + 2x₃δ_{3μ} = 2x_μ for μ ∈ {1,2,3}. -/
depends on (14)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
add_zero
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
mul_zero
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
basisVec_ne
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
coordRay
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
coordRay_apply
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
spatialNormSq
in IndisputableMonolith.Relativity.Calculus.Derivatives
decl_use
-
get
in IndisputableMonolith.RRF.Core.Vantage
decl_use