`pathWeight_pos`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Measurement.PathAction on GitHub at line 37.

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

  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.