`pathWeight_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Measurement.PathAction
domain: Measurement
line: 37 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.PathAction on GitHub at line 37.

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

  34  Complex.exp (- pathAction γ / 2) * Complex.exp (φ * I)
  35
  36/-- Weight is positive. -/
  37lemma pathWeight_pos (γ : RecognitionPath) : 0 < pathWeight γ := by
  38  unfold pathWeight
  39  exact Real.exp_pos _
  40
  41/-- Amplitude modulus squared equals weight. -/
  42theorem amplitude_mod_sq_eq_weight (γ : RecognitionPath) (φ : ℝ) :
  43  ‖pathAmplitude γ φ‖ ^ 2 = pathWeight γ := by
  44  unfold pathAmplitude pathWeight
  45  have h1 : ‖Complex.exp (-(pathAction γ) / 2)‖ = Real.exp (-(pathAction γ) / 2) := by
  46    simpa using Complex.norm_exp_ofReal (-(pathAction γ) / 2)
  47  have h2 := Complex.norm_exp_ofReal_mul_I φ
  48  rw [norm_mul]
  49  simp only [h1, h2, mul_one, sq]
  50  rw [← Real.exp_add]
  51  ring
  52
  53end Measurement
  54end IndisputableMonolith

papers checked against this theorem

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