OAI/Probability/GaussianReplacement/StreamTransfer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.continuation_le_one_no_borel line 22
2. lemma OAI.NoiselessRegression.projectionLaw_absolutelyContinuous line 47

   Distinct definitions of this name: OAI/Probability/GaussianRegression/Observation.lean:25 (same statement text; different proof or body). Qualify references as OAI.NoiselessRegression.projectionLaw_absolutelyContinuous@path.

3. lemma OAI.NoiselessRegression.sphere_observation_quasi line 73

   Also declared: OAI/Probability/GaussianRegression/Observation.lean:52 (same declaration text).

4. lemma OAI.NoiselessRegression.measurePreserving_pi_prefix line 108

   Also declared: OAI/Probability/GaussianRegression/Transfer.lean:27 (same declaration text).

5. lemma OAI.NoiselessRegression.sphere_sample_observation_quasi line 118

   Also declared: OAI/Probability/GaussianRegression/Transfer.lean:37 (same declaration text).

6. lemma OAI.NoiselessRegression.streamRoute_congr line 130

   Also declared: OAI/Probability/GaussianRegression/Transfer.lean:49 (same declaration text).

7. lemma OAI.NoiselessRegression.prefix_route_cap_bound line 140

   Also declared: OAI/Probability/GaussianRegression/Transfer.lean:59 (same declaration text).