Manuscript Em05-A@1 · Em05-A-v1.tex · proposition · 9cac0def

Proposition: Transmission intervals

Certified approximation interfaces · lines 1094–1123 · proof included or linked

Em05-A@1#prop:interval

If a validated calculation establishes

0 \leq η_{-} \leq η \leq η_{+} \leq 1,

then the ideal-phase specified decoder satisfies

e_{specified} \in [1 - η_{+}, 1 - η_{-}],

C (Q : M^{'}) \in [η_{-}, η_{+}], F_{e} \in [\frac{1 + 3 η _{-}}{4}, \frac{1 + 3 η _{+}}{4}] .

For a fixed known $p$ ,

⟨ N_{R} ⟩ \in [2 p η_{-}, 2 p η_{+}] .

Purity can be enclosed by outward evaluation of (eq:purity), but it must not be presumed monotone in $η$ .

Proof. The first four quantities are affine in $η$ with the displayed monotonicity. The purity is an explicit polynomial in $η, t, p, ∣ z ∣^{2}$ , so inclusion-preserving interval evaluation encloses its value.

Displayed formulas in this passage

unlabeled · line 1097
$0 \leq η_{-} \leq η \leq η_{+} \leq 1,$
unlabeled · line 1101
$e_{specified} \in [1 - η_{+}, 1 - η_{-}],$
unlabeled · line 1104
$C (Q : M^{'}) \in [η_{-}, η_{+}], F_{e} \in [\frac{1 + 3 η _{-}}{4}, \frac{1 + 3 η _{+}}{4}] .$
unlabeled · line 1111
$⟨ N_{R} ⟩ \in [2 p η_{-}, 2 p η_{+}] .$

Proposition: Transmission intervals

Displayed formulas in this passage

Nearby in this section