`amplitude_modulus_bridge`

proved

show as: view math explainer →

module: IndisputableMonolith.Measurement.C2ABridge
domain: Measurement
line: 196 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.C2ABridge on GitHub at line 196.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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)‖
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.