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

Partial

Declarations

def AutoSamplingTheory.Tests.CarreDuChamp.zeroGenerator Partial 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 ed709a7f320d

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp

namespace AutoSamplingTheory.Tests.CarreDuChamp

open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp

variable {X : Type*}

noncomputable section

#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.carreDuChamp
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.iteratedCarreDuChamp
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.SatisfiesBakryEmery
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.carreDuChamp_nonneg_of_markov_jensen_rightGenerator
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.fundamental_integration_by_parts
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.negativeGenerator_quadratic_nonneg

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