OAI/Probability/Subsphere/Regression/Model.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SubsphereRegression.Vector line 15
  2. abbrev OAI.SubsphereRegression.UnitSphere line 16
  3. abbrev OAI.SubsphereRegression.State line 17
  4. abbrev OAI.SubsphereRegression.Samples line 18
  5. def OAI.SubsphereRegression.uniformSphere line 20
  6. def OAI.SubsphereRegression.sampleLaw line 24
  7. def OAI.SubsphereRegression.observationReference line 27
  8. structure OAI.SubsphereRegression.Learner line 32

    Source documentation

    A finite-state one-pass procedure. The Boolean true means stop. All indices are prescribed ordinary sample indices, not stored real registers.

    structure Learner (d M T : ℕ) (Ω : Type u) where
…
  9. abbrev OAI.SubsphereRegression.Learner.RunStatus line 40

    Source documentation

    Active finite state, or stopped index and terminal finite state.

    abbrev RunStatus (M : ℕ) := Sum (State M) (ℕ × State M)

    Mentions: OAI.SubsphereRegression.State

  10. def OAI.SubsphereRegression.Learner.start line 42
  11. def OAI.SubsphereRegression.Learner.run line 47
  12. def OAI.SubsphereRegression.Learner.terminal line 60
  13. def OAI.SubsphereRegression.Learner.estimate line 66
  14. structure OAI.SubsphereRegression.Learner.Admissible line 71
  15. def OAI.SubsphereRegression.Learner.angularError line 83
  16. def OAI.SubsphereRegression.Learner.success line 86
  17. def OAI.SubsphereRegression.Learner.uniformSuccess line 91
  18. def OAI.SubsphereRegression.SubquadraticMemory line 98
  19. def OAI.SubsphereRegression.FixedQuadraticMemory line 109