Finite-exponent contraction for sub-Markov kernels #
This file proves the scalar subprobability estimate behind contraction of a
sub-Markov kernel on finite Lᵖ spaces, and its fibrewise integrated form.
theorem
MarkovProcess.eLpNorm_one_le_of_measure_univ_le_one
{α : Type u_1}
[MeasurableSpace α]
{ν : MeasureTheory.Measure α}
{f : α → ℝ}
{p : NNReal}
(hp : 1 ≤ p)
(hν : ν Set.univ ≤ 1)
(hf : MeasureTheory.AEStronglyMeasurable f ν)
:
On a finite measure of mass at most one, the L¹ seminorm is bounded by
every finite Lᵖ seminorm with p ≥ 1.
theorem
MarkovProcess.enorm_integral_rpow_le_lintegral_enorm_rpow
{α : Type u_1}
[MeasurableSpace α]
{ν : MeasureTheory.Measure α}
{f : α → ℝ}
{p : NNReal}
(hp : 1 ≤ p)
(hν : ν Set.univ ≤ 1)
(hf : MeasureTheory.MemLp f (↑p) ν)
:
Jensen's power estimate for a finite subprobability measure. This form is
well suited to fibrewise use because both sides take values in ℝ≥0∞.
theorem
MarkovProcess.lintegral_enorm_kernelIntegral_rpow_le
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α α}
(hκ : IsSubMarkovKernel κ)
(hκμ : μ.bind ⇑κ ≤ μ)
{f : α → ℝ}
{p : NNReal}
(hp : 1 ≤ p)
(hf : MeasureTheory.MemLp f (↑p) μ)
:
The integrated fibrewise power estimate for a sub-Markov kernel.
theorem
MarkovProcess.eLpNorm_kernelIntegral_le
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α α}
(hκ : IsSubMarkovKernel κ)
(hκμ : μ.bind ⇑κ ≤ μ)
{f : α → ℝ}
{p : NNReal}
(hp : 1 ≤ p)
(hf : MeasureTheory.MemLp f (↑p) μ)
:
A sub-Markov kernel which is subinvariant for μ is contractive on every
finite Lᵖ seminorm, 1 ≤ p < ∞.
theorem
MarkovProcess.MemLp.kernelIntegral
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α α}
(hκ : IsSubMarkovKernel κ)
(hκμ : μ.bind ⇑κ ≤ μ)
{f : α → ℝ}
{p : NNReal}
(hp : 1 ≤ p)
(hf : MeasureTheory.MemLp f (↑p) μ)
:
MeasureTheory.MemLp (MarkovProcess.kernelIntegral κ f) (↑p) μ
The kernel integral of an Lᵖ function is again in Lᵖ for every finite
exponent p ≥ 1.