def
definition
decompose_perturbation
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.GW.TensorDecomposition on GitHub at line 20.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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. -/
20def decompose_perturbation (h : Fin 3 → Fin 3 → ℝ) : Prop :=
21 ∃ (tp : TensorPerturbation) (scalar : ℝ) (vector : Fin 3 → ℝ),
22 h = (fun i j => tp.h_TT 0 i j + (if i = j then scalar else 0) + (vector i + vector j))
23
24/-- Existence of a TT projection operator. -/
25def projection_operator_TT : Prop :=
26 ∃ P : (Fin 3 → Fin 3 → ℝ) → (Fin 3 → Fin 3 → ℝ),
27 ∀ h, ∃ tp : TensorPerturbation, P h = tp.h_TT 0
28
29/-- Uniqueness of the TT decomposition. -/
30def decomposition_unique : Prop :=
31 ∀ tp1 tp2 : TensorPerturbation, tp1.h_TT = tp2.h_TT → tp1 = tp2
32
33theorem decomposition_unique_holds : decomposition_unique := by
34 intro tp1 tp2 h
35 cases tp1; cases tp2; simp at h; subst h
36 rfl
37
38
39end GW
40end Relativity
41end IndisputableMonolith