CapacityAchievability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GAD.phase_rate_achievable line 12
Source documentation
Direct operational coding for the phase pair; conditional and global typical subspaces and a sequential collective POVM, rather than an assumed coding theorem.
```
theorem phase_rate_achievable (γ ν : ℝ) (hγ : γ ∈ Set.Icc (0:ℝ) 1)
    (hν : ν ∈ Set.Icc (0:ℝ) 1) {p : ℝ} (hp : p ∈ Set.Icc (0:ℝ) 1)
    {r : ℝ} (hr : 0 ≤ r) (hrχ : r < objective γ ν p) :
    Achievable γ ν (r/Real.log 2) := by
…
```
Mentions: OAI.GAD.objective, OAI.GAD.Achievable