IndisputableMonolith.Relativity.GW.ActionExpansion

   1import Mathlib
   2import IndisputableMonolith.Relativity.Geometry
   3import IndisputableMonolith.Relativity.Fields
   4import IndisputableMonolith.Relativity.Cosmology.FRWMetric
   5import IndisputableMonolith.Relativity.GW.TensorDecomposition
   6
   7namespace IndisputableMonolith
   8namespace Relativity
   9namespace GW
  10
  11open Geometry
  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
  38