structure
definition
def or abbrev
TensorPerturbation
show as:
view Lean formalization →
formal statement (Lean)
12structure TensorPerturbation where
13 h_TT : ℝ → (Fin 3 → Fin 3 → ℝ)
14 transverse : ∀ t i, Finset.sum (Finset.range 3) (fun j =>
15 if hj : j < 3 then h_TT t i ⟨j, hj⟩ else 0) = 0
16 traceless : ∀ t, Finset.sum (Finset.range 3) (fun i =>
17 if hi : i < 3 then h_TT t ⟨i, hi⟩ ⟨i, hi⟩ else 0) = 0
18
19/-- Decomposition of a general spatial metric perturbation into TT part and other sectors. -/