OAI/Probability/GaussianRegression/Observation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absolute continuity of noiseless spherical observation laws.

  1. lemma OAI.NoiselessRegression.projectionLaw_absolutelyContinuous line 25

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

  2. lemma OAI.NoiselessRegression.sphere_observation_quasi line 52

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