OAI/Probability/GaussianRegression/Transfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Prefix integration and transfer between almost-everywhere equal transitions.

  1. lemma OAI.NoiselessRegression.measurePreserving_pi_prefix line 27

    Also declared: OAI/Probability/GaussianReplacement/StreamTransfer.lean:108 (same declaration text).

  2. lemma OAI.NoiselessRegression.sphere_sample_observation_quasi line 37

    Also declared: OAI/Probability/GaussianReplacement/StreamTransfer.lean:118 (same declaration text).

  3. lemma OAI.NoiselessRegression.streamRoute_congr line 49

    Also declared: OAI/Probability/GaussianReplacement/StreamTransfer.lean:130 (same declaration text).

  4. lemma OAI.NoiselessRegression.prefix_route_cap_bound line 59

    Also declared: OAI/Probability/GaussianReplacement/StreamTransfer.lean:140 (same declaration text).