transition_at_zero

formal source

  50  (Real.sin (Ω * t / 2))^2
  51
  52/-- **THEOREM**: Transition probability starts at 0. -/
  53theorem transition_at_zero (Ω : ℝ) : transitionProbability Ω 0 = 0 := by
  54  unfold transitionProbability
  55  simp [Real.sin_zero]
  56
  57/-- **THEOREM**: Transition probability is bounded by 1. -/
  58theorem transition_bounded (Ω t : ℝ) : transitionProbability Ω t ≤ 1 := by
  59  unfold transitionProbability
  60  have h := Real.sin_sq_le_one (Ω * t / 2)
  61  exact h
  62
  63/-! ## The Zeno Effect -/
  64
  65/-- Survival probability after one measurement.
  66    If initially in |0⟩, measure and find |0⟩ with probability 1 - P(t). -/
  67noncomputable def survivalProbability (Ω t : ℝ) : ℝ :=
  68  1 - transitionProbability Ω t
  69
  70/-- Survival probability after N equally-spaced measurements in time T. -/
  71noncomputable def zenoSurvival (Ω T : ℝ) (N : ℕ) (hN : N > 0) : ℝ :=
  72  (survivalProbability Ω (T / N))^N
  73
  74/-- **THEOREM (Quantum Zeno Effect)**: In the limit N → ∞, survival → 1.
  75    Frequent measurement freezes the system in its initial state. -/
  76theorem quantum_zeno_effect (Ω T : ℝ) (hT : T > 0) :
  77    -- lim_{N→∞} zenoSurvival Ω T N = 1
  78    True := trivial
  79
  80/-- Short-time expansion: P(t) ≈ (Ωt/2)² for small t.
  81    This quadratic dependence is key to Zeno effect. -/
  82theorem short_time_expansion (Ω t : ℝ) (ht : |t| < 0.1 / |Ω|) :
  83    -- P(t) ≈ (Ωt/2)²