lemma proved term proof

`deriv_add_lin`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  60lemma deriv_add_lin (f g : (Fin 4 → ℝ) → ℝ) (μ : Fin 4)
  61    (x : Fin 4 → ℝ) (hf : DifferentiableAt ℝ (fun t => f (coordRay x μ t)) 0)
  62    (hg : DifferentiableAt ℝ (fun t => g (coordRay x μ t)) 0) :
  63  partialDeriv_v2 (fun y => f y + g y) μ x =
  64    partialDeriv_v2 f μ x + partialDeriv_v2 g μ x := by

proof body

Term-mode proof.

  65  unfold partialDeriv_v2
  66  exact deriv_add hf hg
  67
  68/-- Linearity of directional derivative (scalar multiplication). -/

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
partialDeriv_v2 in IndisputableMonolith.Foundation.Hamiltonian decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
coordRay in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2 in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
deriv_add in IndisputableMonolith.Relativity.Fields.Scalar decl_use