test module

`Tests.BakryEmeryCalculus`

2 named declarations scanned from Tests/BakryEmeryCalculus.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BakryEmeryCalculus

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.Tests.BakryEmeryCalculus.zeroGenerator Partial Not mapped

No declaration docstring.

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

Tests/BakryEmeryCalculus.lean:10published source at ed709a7f320d

theorem AutoSamplingTheory.Tests.BakryEmeryCalculus.zeroGenerator_satisfiesBakryEmery Partial Not mapped

No declaration docstring.

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

example {alpha : ℝ} (halpha : 0 < alpha) (f : X → ℝ) (x : X) :
    2 * alpha * carreDuChamp (zeroGenerator (X := X)) f f x ≤
      zeroGenerator (X := X)
          (carreDuChamp (zeroGenerator (X := X)) f f) x -
        2 * carreDuChamp (zeroGenerator (X := X)) f
          (zeroGenerator (X := X) f) x :=
  interpolationDerivative_lower_bound_of_expandedBakryEmery
    (zeroGenerator (X := X)) halpha (by
      intro g y
      simpa only [iteratedCarreDuChamp] using
        (zeroGenerator_satisfiesBakryEmery halpha).2 g y) f x

end AutoSamplingTheory.Tests.BakryEmeryCalculus

Tests/BakryEmeryCalculus.lean:12published source at ed709a7f320d

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BakryEmeryCalculus

namespace AutoSamplingTheory.Tests.BakryEmeryCalculus

open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp

variable {X : Type*}

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

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

example {alpha : ℝ} (halpha : 0 < alpha) (f : X → ℝ) (x : X) :
    2 * alpha * carreDuChamp (zeroGenerator (X := X)) f f x ≤
      zeroGenerator (X := X)
          (carreDuChamp (zeroGenerator (X := X)) f f) x -
        2 * carreDuChamp (zeroGenerator (X := X)) f
          (zeroGenerator (X := X) f) x :=
  interpolationDerivative_lower_bound_of_expandedBakryEmery
    (zeroGenerator (X := X)) halpha (by
      intro g y
      simpa only [iteratedCarreDuChamp] using
        (zeroGenerator_satisfiesBakryEmery halpha).2 g y) f x

end AutoSamplingTheory.Tests.BakryEmeryCalculus