New lemmas for mathlib
theorem
indicator_one_mul_const
{α : Type u_1}
{M : Type u_2}
[MonoidWithZero M]
(s : Set α)
(c : M)
(a : α)
:
theorem
indicator_one_mul_const'
{α : Type u_1}
{M : Type u_2}
[MonoidWithZero M]
(s : Set α)
(c : M)
(a : α)
:
theorem
Set.indicator_one_smul_apply
{α : Type u_1}
{M : Type u_2}
{β : Type u_3}
[Zero β]
[MonoidWithZero M]
[MulActionWithZero M β]
(f : α → β)
(s : Set α)
(a : α)
:
theorem
eq_of_measurable_comap
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[m : MeasurableSpace Y]
[MeasurableSingletonClass Z]
(f : X → Y)
{g : X → Z}
(hg : Measurable g)
{x₁ : X}
{x₂ : X}
(h : f x₁ = f x₂)
:
g x₁ = g x₂
If a function g is measurable with respect to the pullback along some function f, then
to prove g x = g y it is enough to prove f x = f y.
theorem
eq_of_stronglyMeasurable_comap
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_6}
[m : MeasurableSpace Y]
[TopologicalSpace Z]
[TopologicalSpace.PseudoMetrizableSpace Z]
[T1Space Z]
(f : X → Y)
{g : X → Z}
(hg : MeasureTheory.StronglyMeasurable g)
{x₁ : X}
{x₂ : X}
(h : f x₁ = f x₂)
:
g x₁ = g x₂
If a function g is strongly measurable with respect to the pullback along some function f,
then to prove g x = g y it is enough to prove f x = f y.
theorem
Kernel.compProd_apply_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel (X × Y) Z)
[ProbabilityTheory.IsSFiniteKernel η]
{s : Set Y}
(hs : MeasurableSet s)
{t : Set Z}
(ht : MeasurableSet t)
(x : X)
:
theorem
Kernel.map_map
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{T : Type u_4}
[MeasurableSpace Z]
[MeasurableSpace T]
[MeasurableSpace X]
[MeasurableSpace Y]
(κ : ProbabilityTheory.Kernel X Y)
{f : Y → Z}
(hf : Measurable f)
{g : Z → T}
(hg : Measurable g)
:
theorem
Measure.map_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{T : Type u_4}
[MeasurableSpace Z]
[MeasurableSpace T]
[MeasurableSpace X]
[MeasurableSpace Y]
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsFiniteMeasure μ]
(ν : MeasureTheory.Measure Y)
[MeasureTheory.IsFiniteMeasure ν]
{f : X → Z}
(hf : Measurable f)
{g : Y → T}
(hg : Measurable g)
:
MeasureTheory.Measure.map (Prod.map f g) (μ.prod ν) = (MeasureTheory.Measure.map f μ).prod (MeasureTheory.Measure.map g ν)
theorem
Kernel.map_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{T : Type u_4}
{U : Type u_5}
[MeasurableSpace Z]
[MeasurableSpace T]
[MeasurableSpace U]
[MeasurableSpace X]
[MeasurableSpace Y]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsFiniteKernel κ]
(η : ProbabilityTheory.Kernel X T)
[ProbabilityTheory.IsFiniteKernel η]
{f : Y → Z}
(hf : Measurable f)
{g : T → U}
(hg : Measurable g)
:
theorem
Kernel.map_prod_fst
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsMarkovKernel η]
:
(κ.prod η).map Prod.fst = κ
theorem
Kernel.map_prod_snd
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsMarkovKernel κ]
(η : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsSFiniteKernel η]
:
(κ.prod η).map Prod.snd = η
theorem
Kernel.map_deterministic
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{f : X → Y}
(hf : Measurable f)
{g : Y → Z}
(hg : Measurable g)
:
(ProbabilityTheory.Kernel.deterministic f hf).map g = ProbabilityTheory.Kernel.deterministic (g ∘ f) ⋯
theorem
Kernel.deterministic_prod_apply'
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{f : X → Y}
(mf : Measurable f)
(η : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsSFiniteKernel η]
(x : X)
{s : Set (Y × Z)}
(ms : MeasurableSet s)
:
(((ProbabilityTheory.Kernel.deterministic f mf).prod η) x) s = (η x) {z : Z | (f x, z) ∈ s}
theorem
Kernel.prod_apply_symm'
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsSFiniteKernel κ]
(η : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsSFiniteKernel η]
(x : X)
{s : Set (Y × Z)}
(hs : MeasurableSet s)
:
theorem
Kernel.prod_deterministic_apply'
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{f : X → Z}
(mf : Measurable f)
(η : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsSFiniteKernel η]
(x : X)
{s : Set (Y × Z)}
(ms : MeasurableSet s)
:
((η.prod (ProbabilityTheory.Kernel.deterministic f mf)) x) s = (η x) {y : Y | (y, f x) ∈ s}
theorem
Measure.map_snd_compProd
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsProbabilityMeasure μ]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsSFiniteKernel κ]
{f : Y → Z}
(hf : Measurable f)
:
MeasureTheory.Measure.map f (μ.compProd κ).snd = (μ.compProd (κ.map f)).snd
theorem
Measure.fst_compProd
{X : Type u_1}
{Y : Type u_2}
[MeasurableSpace X]
[MeasurableSpace Y]
(μ : MeasureTheory.Measure X)
[MeasureTheory.SFinite μ]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsMarkovKernel κ]
:
(μ.compProd κ).fst = μ
theorem
Kernel.comap_const
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
(μ : MeasureTheory.Measure Z)
{f : X → Y}
(hf : Measurable f)
:
(ProbabilityTheory.Kernel.const Y μ).comap f hf = ProbabilityTheory.Kernel.const X μ
theorem
Kernel.integrable_prod_iff
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{E : Type u_6}
[NormedAddCommGroup E]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsFiniteKernel κ]
(η : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsFiniteKernel η]
(x : X)
{f : Y × Z → E}
(hf : MeasureTheory.AEStronglyMeasurable f ((κ.prod η) x))
:
MeasureTheory.Integrable f ((κ.prod η) x) ↔ (∀ᵐ (y : Y) ∂κ x, MeasureTheory.Integrable (fun (z : Z) => f (y, z)) (η x)) ∧ MeasureTheory.Integrable (fun (y : Y) => ∫ (z : Z), ‖f (y, z)‖ ∂η x) (κ x)
theorem
Kernel.integrable_prod_iff'
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{E : Type u_6}
[NormedAddCommGroup E]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsFiniteKernel κ]
(η : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsFiniteKernel η]
(x : X)
{f : Y × Z → E}
(hf : MeasureTheory.AEStronglyMeasurable f ((κ.prod η) x))
:
MeasureTheory.Integrable f ((κ.prod η) x) ↔ (∀ᵐ (z : Z) ∂η x, MeasureTheory.Integrable (fun (y : Y) => f (y, z)) (κ x)) ∧ MeasureTheory.Integrable (fun (z : Z) => ∫ (y : Y), ‖f (y, z)‖ ∂κ x) (η x)
theorem
integrable_dirac
{X : Type u_1}
[MeasurableSpace X]
{E : Type u_6}
[NormedAddCommGroup E]
{f : X → E}
(mf : MeasureTheory.StronglyMeasurable f)
{x : X}
:
theorem
Kernel.integrable_deterministic_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{E : Type u_6}
[NormedAddCommGroup E]
{f : X → Y}
(mf : Measurable f)
(κ : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsFiniteKernel κ]
(x : X)
{g : Y × Z → E}
(mg : MeasureTheory.StronglyMeasurable g)
:
MeasureTheory.Integrable g (((ProbabilityTheory.Kernel.deterministic f mf).prod κ) x) ↔ MeasureTheory.Integrable (fun (z : Z) => g (f x, z)) (κ x)
theorem
Kernel.integrable_comp_iff
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{E : Type u_6}
[NormedAddCommGroup E]
(η : ProbabilityTheory.Kernel Y Z)
[ProbabilityTheory.IsSFiniteKernel η]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsSFiniteKernel κ]
(x : X)
{f : Z → E}
(hf : MeasureTheory.AEStronglyMeasurable f ((η.comp κ) x))
:
MeasureTheory.Integrable f ((η.comp κ) x) ↔ (∀ᵐ (y : Y) ∂κ x, MeasureTheory.Integrable f (η y)) ∧ MeasureTheory.Integrable (fun (y : Y) => ∫ (z : Z), ‖f z‖ ∂η y) (κ x)
theorem
Kernel.integral_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsFiniteKernel κ]
(η : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsFiniteKernel η]
(x : X)
{f : Y × Z → E}
(hf : MeasureTheory.Integrable f ((κ.prod η) x))
:
theorem
Kernel.integral_comp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(η : ProbabilityTheory.Kernel Y Z)
[ProbabilityTheory.IsFiniteKernel η]
(κ : ProbabilityTheory.Kernel X Y)
[ProbabilityTheory.IsFiniteKernel κ]
(x : X)
{g : Z → E}
(hg : MeasureTheory.Integrable g ((η.comp κ) x))
:
∫ (z : Z), g z ∂(η.comp κ) x = ∫ (y : Y), ∫ (z : Z), g z ∂η y ∂κ x
theorem
Kernel.integral_deterministic_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : X → Y}
(mf : Measurable f)
(κ : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsFiniteKernel κ]
(x : X)
{g : Y × Z → E}
(mg : MeasureTheory.StronglyMeasurable g)
(i_g : MeasureTheory.Integrable (fun (z : Z) => g (f x, z)) (κ x))
:
∫ (p : Y × Z), g p ∂((ProbabilityTheory.Kernel.deterministic f mf).prod κ) x = ∫ (z : Z), g (f x, z) ∂κ x
theorem
Kernel.lintegral_deterministic_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[MeasurableSpace Z]
[MeasurableSpace X]
[MeasurableSpace Y]
{f : X → Y}
(mf : Measurable f)
(κ : ProbabilityTheory.Kernel X Z)
[ProbabilityTheory.IsFiniteKernel κ]
(x : X)
{g : Y × Z → ENNReal}
(mg : Measurable g)
:
∫⁻ (p : Y × Z), g p ∂((ProbabilityTheory.Kernel.deterministic f mf).prod κ) x = ∫⁻ (z : Z), g (f x, z) ∂κ x
theorem
MeasureTheory.Filtration.condexp_condexp
{X : Type u_1}
[MeasurableSpace X]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_7}
[Preorder ι]
(f : X → E)
{μ : MeasureTheory.Measure X}
(ℱ : MeasureTheory.Filtration ι inferInstance)
{i : ι}
{j : ι}
(hij : i ≤ j)
[MeasureTheory.SigmaFinite (μ.trim ⋯)]
:
MeasureTheory.condexp (↑ℱ i) μ (MeasureTheory.condexp (↑ℱ j) μ f) =ᵐ[μ] MeasureTheory.condexp (↑ℱ i) μ f
theorem
updateFinset_self
{ι : Type u_1}
[DecidableEq ι]
{α : ι → Type u_2}
(x : (i : ι) → α i)
{s : Finset ι}
(y : (i : { x : ι // x ∈ s }) → α ↑i)
:
(fun (i : { x : ι // x ∈ s }) => Function.updateFinset x s y ↑i) = y
theorem
Finset.Iic_sdiff_Ioc_same
{α : Type u_1}
[LinearOrder α]
[OrderBot α]
[LocallyFiniteOrder α]
{a : α}
{b : α}
(hab : a ≤ b)
:
Finset.Iic b \ Finset.Ioc a b = Finset.Iic a
theorem
Finset.right_mem_Iic
{α : Type u_1}
[Preorder α]
[LocallyFiniteOrderBot α]
(a : α)
:
a ∈ Finset.Iic a
theorem
Finset.Iic_union_Ioc_eq_Iic
{α : Type u_1}
[LinearOrder α]
[LocallyFiniteOrder α]
[OrderBot α]
{a : α}
{b : α}
(h : a ≤ b)
:
Finset.Iic a ∪ Finset.Ioc a b = Finset.Iic b
theorem
Finset.disjoint_Iic_Ioc
{α : Type u_1}
[Preorder α]
[LocallyFiniteOrder α]
[OrderBot α]
{a : α}
{b : α}
{c : α}
(h : a ≤ b)
:
Disjoint (Finset.Iic a) (Finset.Ioc b c)
theorem
prod_Ioc
{M : Type u_1}
[CommMonoid M]
(n : ℕ)
(f : { x : ℕ // x ∈ Finset.Ioc 0 (n + 1) } → M)
:
f ⟨n + 1, ⋯⟩ * ∏ i : { x : ℕ // x ∈ Finset.Ioc 0 n }, f ⟨↑i, ⋯⟩ = ∏ i : { x : ℕ // x ∈ Finset.Ioc 0 (n + 1) }, f i