`kinetic_coefficient`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.GW.ActionExpansion
domain: Relativity
line: 24 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.GW.ActionExpansion on GitHub at line 24.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  21def isolate_tensor_contribution (scale : ScaleFactor) (h : TensorPerturbation) : Prop :=
  22  True
  23
  24noncomputable def kinetic_coefficient (scale : ScaleFactor) (α C_lag : ℝ) (t : ℝ) : ℝ :=
  25  let a := scale.a t
  26  a^3 * (1 + 0.01 * α * C_lag)
  27
  28noncomputable def gradient_coefficient (scale : ScaleFactor) (α C_lag : ℝ) (t : ℝ) : ℝ :=
  29  let a := scale.a t
  30  a * (1 + 0.01 * α * C_lag)
  31
  32def action_form_verified (scale : ScaleFactor) (h : TensorPerturbation) (α C_lag : ℝ) : Prop :=
  33  True
  34
  35end GW
  36end Relativity
  37end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.