OAI/Probability/StrongRayleigh/DecoderUniqueness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336AdditiveD139.Decoder.envelope line 14
2. theorem OAI.Problem336AdditiveD139.Decoder.envelope_nonneg line 17
3. theorem OAI.Problem336AdditiveD139.Decoder.continuous_envelope line 22
4. theorem OAI.Problem336AdditiveD139.Decoder.integral_envelope line 26
5. theorem OAI.Problem336AdditiveD139.Decoder.envelope_tendsto_zero line 38
6. theorem OAI.Problem336AdditiveD139.Decoder.uniform_volterra_unique line 43
7. theorem OAI.Problem336AdditiveD139.Decoder.bounded_drift_decoder_unique line 65