test module

`Tests.AccumulatedEnergy`

0 named declarations scanned from Tests/AccumulatedEnergy.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.AccumulatedEnergy

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/AccumulatedEnergy.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.AccumulatedEnergy

namespace AutoSamplingTheory.Tests.AccumulatedEnergy

open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.AccumulatedEnergy

#check accumulatedEnergy
#check accumulatedEnergy_zero
#check accumulatedEnergy_mono
#check accumulatedEnergy_eq_terminal_of_le
#check accumulatedEnergy_le_terminal
#check accumulatedEnergy_nonneg

example {Omega : Type*} [MeasurableSpace Omega]
    (eta : NNReal → Omega → ℝ) (T : NNReal) (omega : Omega) :
    accumulatedEnergy eta T 0 omega = 0 :=
  accumulatedEnergy_zero eta T omega

end AutoSamplingTheory.Tests.AccumulatedEnergy