weight_equals_born

formal source

 182  ring
 183
 184/-- Weight equals Born probability: exp(-2A) = |α₂|² -/
 185theorem weight_equals_born (rot : TwoBranchRotation) :
 186  pathWeight (pathFromRotation rot) = initialAmplitudeSquared rot := by
 187  unfold pathWeight initialAmplitudeSquared
 188  rw [measurement_bridge_C_eq_2A]
 189  have h := Measurement.born_weight_from_rate rot
 190  have hWeight :
 191      Real.exp (-(2 * rateAction rot)) = initialAmplitudeSquared rot := by
 192    simpa [rateAction, Measurement.initialAmplitudeSquared] using h
 193  simpa using hWeight
 194
 195/-- Amplitude bridge modulus: |𝒜| = exp(-A) -/
 196theorem amplitude_modulus_bridge (rot : TwoBranchRotation) (φ : ℝ) :
 197  ‖pathAmplitude (pathFromRotation rot) φ‖ = Real.exp (- rateAction rot) := by
 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)‖