theorem
proved
weight_equals_born
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement.C2ABridge on GitHub at line 185.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
bridge -
Measurement -
A -
modulus -
A -
measurement_bridge_C_eq_2A -
pathFromRotation -
pathWeight -
Measurement -
born_weight_from_rate -
initialAmplitudeSquared -
rateAction -
TwoBranchRotation -
A -
Amplitude -
Measurement
used by
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)‖