production module

`AutoSamplingTheory.SDE`

4 named declarations scanned from AutoSamplingTheory/SDE.lean.

Imports

AutoSamplingTheory.Probability

Imported by

AutoSamplingTheoryAutoSamplingTheory.SALD

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

structure AutoSamplingTheory.ItoDiffusionContract Partial Not mapped

No declaration docstring.

structure ItoDiffusionContract where
  id : String
  forwardSde : String
  marginalPath : String
  reversePath : String
  velocityFormula : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

AutoSamplingTheory/SDE.lean:9published source at ed709a7f320d

structure AutoSamplingTheory.FokkerPlanckContract Partial Not mapped

No declaration docstring.

structure FokkerPlanckContract where
  id : String
  lawName : String
  equation : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

AutoSamplingTheory/SDE.lean:19published source at ed709a7f320d

structure AutoSamplingTheory.EulerMaruyamaContract Partial Not mapped

No declaration docstring.

structure EulerMaruyamaContract where
  id : String
  updateFormula : String
  interpolationFormula : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

AutoSamplingTheory/SDE.lean:27published source at ed709a7f320d

structure AutoSamplingTheory.DiscretizationErrorContract Partial Not mapped

No declaration docstring.

structure DiscretizationErrorContract where
  id : String
  localDefect : String
  boundShape : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

end AutoSamplingTheory

AutoSamplingTheory/SDE.lean:35published source at ed709a7f320d

Complete Lean source

AutoSamplingTheory/SDE.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.Probability

/-!
# SDE and discretization contracts
-/

namespace AutoSamplingTheory

structure ItoDiffusionContract where
  id : String
  forwardSde : String
  marginalPath : String
  reversePath : String
  velocityFormula : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

structure FokkerPlanckContract where
  id : String
  lawName : String
  equation : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

structure EulerMaruyamaContract where
  id : String
  updateFormula : String
  interpolationFormula : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

structure DiscretizationErrorContract where
  id : String
  localDefect : String
  boundShape : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

end AutoSamplingTheory