structure definition def or abbrev

`VolumeElement`

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

formal statement (Lean)

  19structure VolumeElement where
  20  grid_spacing : ℝ  -- Δx for discrete approximation
  21  grid_spacing_pos : 0 < grid_spacing
  22
  23/-- Sample points for discrete integration (uniform grid). -/

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

eh_action_minkowski in IndisputableMonolith.Relativity.Fields.Integration decl_use
einstein_hilbert_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
integrate_add in IndisputableMonolith.Relativity.Fields.Integration decl_use
integrate_scalar in IndisputableMonolith.Relativity.Fields.Integration decl_use
integrate_smul in IndisputableMonolith.Relativity.Fields.Integration decl_use
kinetic_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
kinetic_nonneg in IndisputableMonolith.Relativity.Fields.Integration decl_use
potential_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
sample_grid in IndisputableMonolith.Relativity.Fields.Integration decl_use
default_volume in IndisputableMonolith.Relativity.ILG.Action decl_use
VolumeElement in IndisputableMonolith.Relativity.ILG.Action decl_use

depends on (3)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
uniform in IndisputableMonolith.Information.ShannonEntropy decl_use
VolumeElement in IndisputableMonolith.Relativity.ILG.Action decl_use