Manuscript Em05-B@1 · Em05-B-v1.tex · proposition · 6c050f5b

Proposition: Transmission intervals

Referenced certification interfaces › Transmission and phase certificates · lines 2039–2070 · proof included or linked

Em05-B@1#prop:transmissionInterval

If a validated calculation establishes $0 \leq η_{-} \leq η \leq η_{+} \leq 1$ , 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 fixed known $p$ ,

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

Purity and the balanced upper bound can be enclosed by inclusion-preserving interval evaluation of their displayed expressions. Purity must not be presumed monotone in $η$ .

Proof. The first four quantities are affine with the stated monotonicity. The remaining expressions are explicit continuous functions on the closed parameter interval; validated outward evaluation encloses them.

Displayed formulas in this passage

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

Proposition: Transmission intervals

Displayed formulas in this passage

Nearby in this section