pith. machine review for the scientific record. sign in
theorem proved term proof

etherington_duality_preserved

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  52theorem etherington_duality_preserved (z : ℝ) (bg_DA bg_DL : ℝ) (P : ILG.KernelParams)
  53    (h_bg_dual : bg_DL = (1 + z)^2 * bg_DA) :
  54    DL_rescaled z bg_DL P = (1 + z)^2 * DA_rescaled z bg_DA P := by

proof body

Term-mode proof.

  55  unfold DL_rescaled
  56  rw [h_bg_dual]
  57  field_simp
  58  ring
  59
  60/-- Theorem: Optical rescaling reduces to GR when the coupling C = 0. -/

depends on (3)

Lean names referenced from this declaration's body.