The kernel integral on L^∞ #
This file proves the real-valued L^∞ contraction estimate for integration
against a sub-Markov kernel preserving a subinvariant measure. The operator
itself is packaged as a continuous linear map by kernelLpTop in
Kernel/Lp.lean.
theorem
MarkovProcess.enorm_kernelIntegral_le_of_ae
{α : Type u_1}
[MeasurableSpace α]
{κ : ProbabilityTheory.Kernel α α}
(hκ : IsSubMarkovKernel κ)
{f : α → ℝ}
{C : ENNReal}
{x : α}
(hf : ∀ᵐ (y : α) ∂κ x, ‖f y‖ₑ ≤ C)
:
Integrating a function bounded almost everywhere by C against a
sub-Markov kernel measure preserves that bound.
theorem
MarkovProcess.enorm_kernelIntegral_ae_le_eLpNormEssSup
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α α}
(hκ : IsSubMarkovKernel κ)
(hκμ : μ.bind ⇑κ ≤ μ)
(f : α → ℝ)
:
∀ᵐ (x : α) ∂μ, ‖kernelIntegral κ f x‖ₑ ≤ MeasureTheory.eLpNormEssSup f μ
The essential-supremum bound for f bounds its kernel integral almost
everywhere under subinvariance.
theorem
MarkovProcess.eLpNorm_kernelIntegral_top_le
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α α}
(hκ : IsSubMarkovKernel κ)
(hκμ : μ.bind ⇑κ ≤ μ)
(f : α → ℝ)
:
Integration against a sub-Markov kernel is a contraction for the raw
L^∞ seminorm under subinvariance.
theorem
MarkovProcess.MemLp.kernelIntegral_top
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α α}
(hκ : IsSubMarkovKernel κ)
(hκμ : μ.bind ⇑κ ≤ μ)
{f : α → ℝ}
(hf : MeasureTheory.MemLp f ⊤ μ)
:
MeasureTheory.MemLp (kernelIntegral κ f) ⊤ μ
Integration against a sub-Markov kernel sends L^∞ functions to
L^∞ functions under subinvariance.