OAI/Probability/GaussianInformation/Kernel/Model.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KernelPotential.Ambient line 10

    Also declared: ComparatorChallenges/GaussianInformation.lean:148 (same declaration text).

  2. abbrev OAI.KernelPotential.Rows line 11

    Also declared: ComparatorChallenges/GaussianInformation.lean:149 (same declaration text).

  3. def OAI.KernelPotential.radial line 12

    Also declared: ComparatorChallenges/GaussianInformation.lean:150 (same declaration text).

  4. def OAI.KernelPotential.sphereProbability line 13

    Also declared: ComparatorChallenges/GaussianInformation.lean:151 (same declaration text).

  5. def OAI.KernelPotential.J line 15

    Also declared: ComparatorChallenges/GaussianInformation.lean:153 (same declaration text).

  6. def OAI.KernelPotential.B line 17

    Also declared: ComparatorChallenges/GaussianInformation.lean:155 (same declaration text).

  7. def OAI.KernelPotential.Phi line 19

    Also declared: ComparatorChallenges/GaussianInformation.lean:157 (same declaration text).

  8. def OAI.KernelPotential.BoundedDensity line 22

    Also declared: ComparatorChallenges/GaussianInformation.lean:160 (same declaration text).

  9. def OAI.KernelPotential.rowLaw line 25

    Also declared: ComparatorChallenges/GaussianInformation.lean:163 (same declaration text).

  10. def OAI.KernelPotential.labels line 27

    Also declared: ComparatorChallenges/GaussianInformation.lean:165 (same declaration text).

  11. structure OAI.KernelPotential.BlockRule line 29

    Also declared: ComparatorChallenges/GaussianInformation.lean:167 (same declaration text).

  12. def OAI.KernelPotential.outgoingLaw line 35

    Also declared: ComparatorChallenges/GaussianInformation.lean:173 (same declaration text).

  13. def OAI.KernelPotential.component line 39

    Also declared: ComparatorChallenges/GaussianInformation.lean:177 (same declaration text).

  14. def OAI.KernelPotential.posterior line 41

    Also declared: ComparatorChallenges/GaussianInformation.lean:179 (same declaration text).

  15. def OAI.KernelPotential.averagePhi line 43

    Also declared: ComparatorChallenges/GaussianInformation.lean:181 (same declaration text).

  16. def OAI.KernelPotential.CoercivityStatement line 46

    Also declared: ComparatorChallenges/GaussianInformation.lean:184 (same declaration text).

  17. def OAI.KernelPotential.DriftStatement line 56

    Distinct definitions of this name: ComparatorChallenges/GaussianInformation.lean:194 (same statement text; different proof or body). Qualify references as OAI.KernelPotential.DriftStatement@path.