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

C_equals_2A

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)

  16theorem C_equals_2A (rot : TwoBranchRotation) :
  17  ∃ (C A : ℝ), C = 2 * A ∧ Real.exp (-C) = initialAmplitudeSquared rot := by

proof body

Term-mode proof.

  18  use 2 * rateAction rot, rateAction rot
  19  refine ⟨by ring, ?_⟩
  20  simp only [initialAmplitudeSquared]
  21  have h := born_weight_from_rate rot
  22  convert h using 2
  23  ring
  24
  25end Measurement
  26end IndisputableMonolith

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.