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

amplitude_modulus_bridge

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)

 196theorem amplitude_modulus_bridge (rot : TwoBranchRotation) (φ : ℝ) :
 197  ‖pathAmplitude (pathFromRotation rot) φ‖ = Real.exp (- rateAction rot) := by

proof body

Tactic-mode proof.

 198  unfold pathAmplitude
 199  have hExpReal :
 200      ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)‖ =
 201        Real.exp (-(pathAction (pathFromRotation rot)) / 2) := by
 202    simpa using Complex.norm_exp_ofReal (-(pathAction (pathFromRotation rot)) / 2)
 203  have hExpI :
 204      ‖Complex.exp (φ * Complex.I)‖ = 1 := by
 205    simpa using Complex.norm_exp_ofReal_mul_I φ
 206  have hAction :
 207      -(pathAction (pathFromRotation rot)) / 2 = - rateAction rot := by
 208    have h := measurement_bridge_C_eq_2A rot
 209    calc
 210      -(pathAction (pathFromRotation rot)) / 2
 211          = -(2 * rateAction rot) / 2 := by simpa [h]
 212      _ = - rateAction rot := by ring
 213  calc
 214    ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)
 215        * Complex.exp (φ * Complex.I)‖
 216        = ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)‖ *
 217          ‖Complex.exp (φ * Complex.I)‖ := by simpa using norm_mul _ _
 218    _ = Real.exp (-(pathAction (pathFromRotation rot)) / 2) * 1 := by
 219        simpa [hExpReal, hExpI]
 220    _ = Real.exp (- rateAction rot) := by
 221        simpa [hAction]
 222
 223end Measurement
 224end IndisputableMonolith

depends on (9)

Lean names referenced from this declaration's body.