test module

`Tests.CarreDuChamp`

1 named declarations scanned from Tests/CarreDuChamp.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

def AutoSamplingTheory.Tests.CarreDuChamp.zeroGenerator Compiled Not mapped

No declaration docstring.

def zeroGenerator : (X → ℝ) →ₗ[ℝ] (X → ℝ) := 0

example (f g : X → ℝ) :
    carreDuChamp (zeroGenerator (X := X)) f g = 0 := by
  ext x
  simp [carreDuChamp, zeroGenerator]

example (f g : X → ℝ) :
    iteratedCarreDuChamp (zeroGenerator (X := X)) f g = 0 := by
  ext x
  simp [iteratedCarreDuChamp, carreDuChamp, zeroGenerator]

example {alpha : ℝ} (halpha : 0 < alpha) :
    SatisfiesBakryEmery (zeroGenerator (X := X)) alpha := by
  refine ⟨halpha, ?_⟩
  intro f x
  simp [carreDuChamp, iteratedCarreDuChamp, zeroGenerator]

end

end AutoSamplingTheory.Tests.CarreDuChamp

Tests/CarreDuChamp.lean:18published source at 77184245109a