production module

`AutoSamplingTheory.SDE`

4 named declarations scanned from AutoSamplingTheory/SDE.lean.

Imports

AutoSamplingTheory.Probability

Imported by

AutoSamplingTheoryAutoSamplingTheory.RMFLDAutoSamplingTheory.SALD

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

structure AutoSamplingTheory.ItoDiffusionContract Compiled 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 77184245109a

structure AutoSamplingTheory.FokkerPlanckContract Compiled 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 77184245109a

structure AutoSamplingTheory.EulerMaruyamaContract Compiled 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 77184245109a

structure AutoSamplingTheory.DiscretizationErrorContract Compiled 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 77184245109a