theorem proved term proof

`integrate_add`

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

Last generation error: xAI API error (429): The model is currently at capacity due to high demand. Please try again in a few minutes. For guaranteed processing and availability, please request Provisioned Throughput: https://docs.x.ai/developers/advanced-api-usage/provisioned-throughput

generate prose now

formal statement (Lean)

  54theorem integrate_add (f₁ f₂ : (Fin 4 → ℝ) → ℝ) (g : MetricTensor) (vol : VolumeElement) :
  55    integrate_scalar (fun x => f₁ x + f₂ x) g vol =
  56      integrate_scalar f₁ g vol + integrate_scalar f₂ g vol := by

proof body

Term-mode proof.

  57  unfold integrate_scalar
  58  simp [Finset.sum_add_distrib, mul_add]
  59
  60/-- Integration scaling property.
  61    STATUS: PROVED — Scaling of finite sums. -/

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
mul_add in IndisputableMonolith.Foundation.ArithmeticFromLogic 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
MetricTensor in IndisputableMonolith.Gravity.Connection decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
MetricTensor in IndisputableMonolith.Meta.Homogenization decl_use
integrate_scalar in IndisputableMonolith.Relativity.Fields.Integration decl_use
VolumeElement in IndisputableMonolith.Relativity.Fields.Integration decl_use
MetricTensor in IndisputableMonolith.Relativity.Geometry.Metric decl_use
VolumeElement in IndisputableMonolith.Relativity.ILG.Action decl_use