def
definition
def or abbrev
bandsFromParams
show as:
view Lean formalization →
formal statement (Lean)
115noncomputable def bandsFromParams (p : ILGParams) : Bands :=
proof body
Definition body.
116 let κ := |p.cLag * p.alpha|
117 { κ_ppn := κ, κ_lensing := κ, κ_gw := κ
118 , h_ppn := by exact abs_nonneg _
119 , h_lensing := by exact abs_nonneg _
120 , h_gw := by exact abs_nonneg _ }
121
122/-! Symbolic Einstein equations moved to Variation/Einstein.lean.
123 VacuumEinstein now defined with real G_μν = 0. -/
124
125/-- Bundle the action inputs `(g, ψ)` for convenience in downstream modules. -/