structure definition def or abbrev

`PressureEquivalence`

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

formal statement (Lean)

  82structure PressureEquivalence where
  83  w_kernel : ℝ → ℝ
  84  rho_b : ℝ → ℝ
  85  delta_b : ℝ → ℝ
  86  effective_pressure : ℝ → ℝ
  87  equiv : ∀ x, effective_pressure x = w_kernel x * rho_b x * delta_b x
  88
  89/-- Any ILG kernel with w >= 1 defines a valid pressure equivalence. -/

depends on (3)

Lean names referenced from this declaration's body.

kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use
pressure in IndisputableMonolith.ILG.PressureForm decl_use