`amplitude_modulus_bridge`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Measurement.C2ABridge on GitHub at line 196.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.