decoherenceTime

formal source

  90/-- Decoherence time for a quantum system with given environment coupling.
  91    τ_decoherence = τ_0 × φ^(-N × g)
  92    where N is number of modes and g is coupling strength. -/
  93noncomputable def decoherenceTime (env : EnvironmentCoupling) : ℝ :=
  94  tau0_seconds * Real.rpow phi (-(env.modes : ℝ) * env.strength)
  95
  96/-- **THEOREM**: Decoherence time decreases with more environmental modes. -/
  97theorem decoherence_decreases_with_modes (env1 env2 : EnvironmentCoupling)
  98    (h : env1.modes < env2.modes) (heq : env1.strength = env2.strength)
  99    (hg : env1.strength > 0) :
 100    decoherenceTime env2 < decoherenceTime env1 := by
 101  unfold decoherenceTime tau0_seconds phi
 102  -- τ₀ × φ^(-n₂g) < τ₀ × φ^(-n₁g) ⟺ φ^(-n₂g) < φ^(-n₁g)
 103  have htau_pos : (7.3e-15 : ℝ) > 0 := by norm_num
 104  rw [heq]
 105  apply mul_lt_mul_of_pos_left _ htau_pos
 106  -- Need: φ^(-n₂g) < φ^(-n₁g), i.e., for φ > 1, -n₂g < -n₁g
 107  have hphi_gt_1 : Constants.phi > 1 := by
 108    have := Constants.phi_gt_onePointFive
 109    linarith
 110  have hg2 : env2.strength > 0 := by rw [← heq]; exact hg
 111  have hexp : -(env2.modes : ℝ) * env2.strength < -(env1.modes : ℝ) * env2.strength := by
 112    have hm : (env1.modes : ℝ) < (env2.modes : ℝ) := Nat.cast_lt.mpr h
 113    nlinarith
 114  exact Real.rpow_lt_rpow_of_exponent_lt hphi_gt_1 hexp
 115
 116/-- **THEOREM**: Stronger coupling causes faster decoherence. -/
 117theorem decoherence_decreases_with_coupling (env1 env2 : EnvironmentCoupling)
 118    (h : env1.strength < env2.strength) (heq : env1.modes = env2.modes)
 119    (hn : env1.modes > 0) :
 120    decoherenceTime env2 < decoherenceTime env1 := by
 121  unfold decoherenceTime tau0_seconds phi
 122  -- τ₀ × φ^(-n*g₂) < τ₀ × φ^(-n*g₁) ⟺ φ^(-n*g₂) < φ^(-n*g₁)
 123  have htau_pos : (7.3e-15 : ℝ) > 0 := by norm_num