Cross-exponent consistency of kernel integral operators

The finite- and infinite-exponent operators are packages of the same raw kernel integral. Consequently their representatives agree almost everywhere whenever their inputs do, even when the inputs and outputs inhabit different Lp types.

theorem MarkovProcess.kernelLpFinite_consistent {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) (hκ : IsSubMarkovKernel κ) (hκμ : μ.bind ⇑κ ≤ μ) (p q : NNReal) [Fact (1 ≤ p)] [Fact (1 ≤ q)] (f : ↥(MeasureTheory.Lp ℝ (↑p) μ)) (g : ↥(MeasureTheory.Lp ℝ (↑q) μ)) (hfg : ↑↑f =ᵐ[μ] ↑↑g) : ↑↑((kernelLpFinite μ κ hκ hκμ p) f) =ᵐ[μ] ↑↑((kernelLpFinite μ κ hκ hκμ q) g)

Finite-exponent kernel operators at possibly different exponents have almost-everywhere equal representatives on almost-everywhere equal inputs.

theorem MarkovProcess.kernelLpFinite_consistent_top {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) (hκ : IsSubMarkovKernel κ) (hκμ : μ.bind ⇑κ ≤ μ) (p : NNReal) [Fact (1 ≤ p)] (f : ↥(MeasureTheory.Lp ℝ (↑p) μ)) (g : ↥(MeasureTheory.Lp ℝ ⊤ μ)) (hfg : ↑↑f =ᵐ[μ] ↑↑g) : ↑↑((kernelLpFinite μ κ hκ hκμ p) f) =ᵐ[μ] ↑↑((kernelLpTop μ κ hκ hκμ) g)

The finite-exponent and infinite-exponent packages have almost-everywhere equal representatives on almost-everywhere equal inputs.

theorem MarkovProcess.kernelLpTop_consistent_finite {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) (hκ : IsSubMarkovKernel κ) (hκμ : μ.bind ⇑κ ≤ μ) (p : NNReal) [Fact (1 ≤ p)] (f : ↥(MeasureTheory.Lp ℝ ⊤ μ)) (g : ↥(MeasureTheory.Lp ℝ (↑p) μ)) (hfg : ↑↑f =ᵐ[μ] ↑↑g) : ↑↑((kernelLpTop μ κ hκ hκμ) f) =ᵐ[μ] ↑↑((kernelLpFinite μ κ hκ hκμ p) g)

Symmetric orientation of kernelLpFinite_consistent_top.