def
definition
action_quadratic_tensor
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.GW.ActionExpansion on GitHub at line 15.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
12open Fields
13open Cosmology
14
15noncomputable def action_quadratic_tensor (scale : ScaleFactor) (h : TensorPerturbation) (α C_lag : ℝ) : ℝ :=
16 0.0
17
18def expand_action_around_FRW (scale : ScaleFactor) (psi : Fields.ScalarField) (α C_lag : ℝ) : Prop :=
19 True
20
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