theorem MeasureTheory.preimage_proj {ι : Type u_1} {α : ι → Type u_2} (I : Finset ι) (J : Finset ι) [(i : ι) → Decidable (i ∈ I)] (hIJ : I ⊆ J) (s : (i : { x : ι // x ∈ I }) → Set (α ↑i)) : Finset.restrict₂ hIJ ⁻¹' Set.univ.pi s = Set.univ.pi fun (j : { x : ι // x ∈ J }) => if h : ↑j ∈ I then s ⟨↑j, h⟩ else Set.univ

theorem MeasureTheory.isProjectiveMeasureFamily_pi {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] : MeasureTheory.IsProjectiveMeasureFamily fun (I : Finset ι) => MeasureTheory.Measure.pi fun (i : { x : ι // x ∈ I }) => μ ↑i

Consider a family of probability measures. You can take their products for any fimite subfamily. This gives a projective family of measures, see IsProjectiveMeasureFamily.

theorem MeasureTheory.kolContent_eq_measure_pi {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [Fintype ι] {s : Set ((i : ι) → X i)} (hs : MeasurableSet s) : (MeasureTheory.kolContent ⋯) s = (MeasureTheory.Measure.pi μ) s

theorem MeasureTheory.mem_Iic_zero {i : ℕ} (hi : i ∈ Finset.Iic 0) : 0 = i

def MeasureTheory.zer {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] : X 0 ≃ᵐ ((i : { x : ℕ // x ∈ Finset.Iic 0 }) → X ↑i)

{0} = Ici 0, version as a measurable equivalence for dependent functions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MeasureTheory.Measure.infinitePiNat {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure (X n)) [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] : MeasureTheory.Measure ((n : ℕ) → X n)

Infinite product measure indexed by ℕ. Use instead Measure.productMeasure for the case of a general index space.

Equations

• One or more equations did not get rendered due to their size.

instance MeasureTheory.instIsProbabilityMeasureBindCoeKernelMeasureOfIsMarkovKernel_kolmogorovExtension4 {X : Type u_2} {Y : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {κ : ProbabilityTheory.Kernel X Y} [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.IsProbabilityMeasure (μ.bind ⇑κ)

Equations

• ⋯ = ⋯

instance MeasureTheory.instIsProbabilityMeasureForallInfinitePiNat {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure (X n)) [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.infinitePiNat μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.er_succ_preimage_pi {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {n : ℕ} (hn : 0 < n) (s : (i : { x : ℕ // x ∈ Finset.Ioc 0 (n + 1) }) → Set (X ↑i)) : ⇑(er 0 n (n + 1) hn ⋯) ⁻¹' Set.univ.pi s = (Set.univ.pi fun (i : { x : ℕ // x ∈ Finset.Ioc 0 n }) => s ⟨↑i, ⋯⟩) ×ˢ (⇑(e n).symm ⁻¹' s ⟨n + 1, ⋯⟩)

theorem MeasureTheory.kerNat_prod {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure (X n)) [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {N : ℕ} (hN : 0 < N) : ProbabilityTheory.Kernel.kerNat (fun (n : ℕ) => ProbabilityTheory.Kernel.const ((l : { x : ℕ // x ∈ Finset.Iic n }) → X ↑l) (μ (n + 1))) 0 N = ProbabilityTheory.Kernel.const ((l : { x : ℕ // x ∈ Finset.Iic 0 }) → X ↑l) (MeasureTheory.Measure.pi fun (i : { x : ℕ // x ∈ Finset.Ioc 0 N }) => μ ↑i)

theorem MeasureTheory.prod_noyau_proj {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure (X n)) [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] (N : ℕ) : ProbabilityTheory.Kernel.partialKernel (fun (n : ℕ) => ProbabilityTheory.Kernel.const ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (μ (n + 1))) 0 N = ((ProbabilityTheory.Kernel.deterministic id ⋯).prod (ProbabilityTheory.Kernel.const ((i : { x : ℕ // x ∈ Finset.Iic 0 }) → X ↑i) (MeasureTheory.Measure.pi fun (i : { x : ℕ // x ∈ Finset.Ioc 0 N }) => μ ↑i))).map ⇑(el 0 N ⋯)

theorem MeasureTheory.el_preimage {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {n : ℕ} (s : (i : { x : ℕ // x ∈ Finset.Iic n }) → Set (X ↑i)) : ⇑(el 0 n ⋯) ⁻¹' Set.univ.pi s = (Set.univ.pi fun (i : { x : ℕ // x ∈ Finset.Iic 0 }) => s ⟨↑i, ⋯⟩) ×ˢ Set.univ.pi fun (i : { x : ℕ // x ∈ Finset.Ioc 0 n }) => s ⟨↑i, ⋯⟩

theorem MeasureTheory.Measure.map_bind {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] (μ : MeasureTheory.Measure X) (κ : ProbabilityTheory.Kernel X Y) (f : Y → Z) (mf : Measurable f) : MeasureTheory.Measure.map f (μ.bind ⇑κ) = μ.bind ⇑(κ.map f)

theorem MeasureTheory.map_bind_eq_bind_comap {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] (μ : MeasureTheory.Measure X) (κ : ProbabilityTheory.Kernel Y Z) (f : X → Y) (mf : Measurable f) : (MeasureTheory.Measure.map f μ).bind ⇑κ = μ.bind ⇑(κ.comap f mf)

theorem MeasureTheory.isProjectiveLimit_infinitePiNat {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure (X n)) [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] : MeasureTheory.IsProjectiveLimit (MeasureTheory.Measure.infinitePiNat μ) fun (I : Finset ℕ) => MeasureTheory.Measure.pi fun (i : { x : ℕ // x ∈ I }) => μ ↑i

theorem MeasureTheory.kolContent_eq_infinitePiNat {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure (X n)) [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {A : Set ((n : ℕ) → X n)} (hA : A ∈ MeasureTheory.measurableCylinders X) : (MeasureTheory.kolContent ⋯) A = (MeasureTheory.Measure.infinitePiNat μ) A

theorem MeasureTheory.cast_pi_eval {ι : Type u_1} {X : ι → Type u_3} (s : Set ι) (x : (i : ↑s) → X ↑i) (i : ↑s) (j : ↑s) (h : i = j) (h' : X ↑i = X ↑j) : cast h' (x i) = x j

theorem MeasureTheory.cast_mem_cast (α : Type u) (β : Type u) (h : α = β) (a : α) (s : Set α) (h' : Set α = Set β) : (cast h a ∈ cast h' s) = (a ∈ s)

theorem MeasureTheory.HEq_meas {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] {i : ι} {j : ι} (hij : i = j) : HEq inferInstance inferInstance

theorem MeasureTheory.secondLemma {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (φ : ℕ ≃ ι) {A : ℕ → Set ((i : ι) → X i)} (A_mem : ∀ (n : ℕ), A n ∈ MeasureTheory.measurableCylinders X) (A_anti : Antitone A) (A_inter : ⋂ (n : ℕ), A n = ∅) : Filter.Tendsto (fun (n : ℕ) => (MeasureTheory.kolContent ⋯) (A n)) Filter.atTop (nhds 0)

This theorem is used to prove the existence of the product measure: the kolContent of a decresaing sequence of cylinders with empty intersection converges to 0, in the case where the measurable spaces are indexed by a countable type. This implies the σ-additivity of kolContent (see sigma_additive_addContent_of_tendsto_zero), which allows to extend it to the σ-algebra by Carathéodory's theorem.

theorem MeasureTheory.kolContent_eq_lmarginal {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [DecidableEq ι] (I : Finset ι) {S : Set ((i : { x : ι // x ∈ I }) → X ↑i)} (mS : MeasurableSet S) (x : (i : ι) → X i) : (MeasureTheory.kolContent ⋯) (MeasureTheory.cylinder I S) = (∫⋯∫⁻_I, (MeasureTheory.cylinder I S).indicator 1 ∂μ) x

The kolContent of cylinder I S can be computed by integrating the indicator of cylinder I S over the variables indexed by I.

theorem MeasureTheory.thirdLemma {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (A : ℕ → Set ((i : ι) → X i)) (A_mem : ∀ (n : ℕ), A n ∈ MeasureTheory.measurableCylinders X) (A_anti : Antitone A) (A_inter : ⋂ (n : ℕ), A n = ∅) : Filter.Tendsto (fun (n : ℕ) => (MeasureTheory.kolContent ⋯) (A n)) Filter.atTop (nhds 0)

theorem MeasureTheory.kolContent_pi_sigma_subadditive {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] ⦃f : ℕ → Set ((i : ι) → X i)⦄ (hf : ∀ (n : ℕ), f n ∈ MeasureTheory.measurableCylinders X) (hf_Union : ⋃ (n : ℕ), f n ∈ MeasureTheory.measurableCylinders X) : (MeasureTheory.kolContent ⋯) (⋃ (n : ℕ), f n) ≤ ∑' (n : ℕ), (MeasureTheory.kolContent ⋯) (f n)

The kolContent associated to a family of probability measures is σ-subadditive.

noncomputable def MeasureTheory.productMeasure {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] : MeasureTheory.Measure ((i : ι) → X i)

The product measure of an arbitrary family of probability measures. It is defined as the unique extension of the function which gives to cylinders the measure given by the associated product measure.

Equations

• MeasureTheory.productMeasure μ = MeasureTheory.Measure.ofAddContent ⋯ ⋯ (MeasureTheory.kolContent ⋯) ⋯

theorem MeasureTheory.isProjectiveLimit_productMeasure {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] : MeasureTheory.IsProjectiveLimit (MeasureTheory.productMeasure μ) fun (I : Finset ι) => MeasureTheory.Measure.pi fun (i : { x : ι // x ∈ I }) => μ ↑i

The product measure is the projective limit of the partial product measures. This ensures uniqueness and expresses the value of the product measures applied to cylinders.

instance MeasureTheory.instIsProbabilityMeasureForallProductMeasure {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] : MeasureTheory.IsProbabilityMeasure (MeasureTheory.productMeasure μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.productMeasure_boxes {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {s : Finset ι} {t : (i : ι) → Set (X i)} (mt : ∀ i ∈ s, MeasurableSet (t i)) : (MeasureTheory.productMeasure μ) ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)

theorem MeasureTheory.productMeasure_cylinder {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {s : Finset ι} {S : Set ((i : { x : ι // x ∈ s }) → X ↑i)} (mS : MeasurableSet S) : (MeasureTheory.productMeasure μ) (MeasureTheory.cylinder s S) = (MeasureTheory.Measure.pi fun (i : { x : ι // x ∈ s }) => μ ↑i) S

theorem MeasureTheory.integral_dep_productMeasure {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Finset ι} {f : ((i : { x : ι // x ∈ s }) → X ↑i) → E} (hf : MeasureTheory.StronglyMeasurable f) : ∫ (y : (i : ι) → X i), f (s.restrict y) ∂MeasureTheory.productMeasure μ = ∫ (y : (i : { x : ι // x ∈ s }) → X ↑i), f y ∂MeasureTheory.Measure.pi fun (i : { x : ι // x ∈ s }) => μ ↑i

def MeasureTheory.ℱ {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] : MeasureTheory.Filtration (Finset ι) inferInstance

The canonical filtration on dependent functions indexed by ι, where 𝓕 s consists of measurable sets depending only on coordinates is s.

Equations

• MeasureTheory.ℱ = { seq := fun (s : Finset ι) => MeasurableSpace.comap s.restrict inferInstance, mono' := ⋯, le' := ⋯ }

theorem MeasureTheory.stronglyMeasurable_dependsOn' {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] {E : Type u_3} [NormedAddCommGroup E] {s : Finset ι} {f : ((i : ι) → X i) → E} (mf : MeasureTheory.StronglyMeasurable f) : DependsOn f ↑s

If a function is strongly measurable with respect to the σ-algebra generated by the finite set of coordinates s, then it only depends on those coordinates.

theorem MeasureTheory.integral_stronglyMeasurable {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [DecidableEq ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Finset ι} {f : ((i : ι) → X i) → E} (mf : MeasureTheory.StronglyMeasurable f) (x : (i : ι) → X i) : ∫ (y : (i : ι) → X i), f y ∂MeasureTheory.productMeasure μ = ∫ (y : (i : { x : ι // x ∈ s }) → X ↑i), f (Function.updateFinset x s y) ∂MeasureTheory.Measure.pi fun (i : { x : ι // x ∈ s }) => μ ↑i

theorem MeasureTheory.lintegral_dep {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {s : Finset ι} {f : ((i : { x : ι // x ∈ s }) → X ↑i) → ENNReal} (hf : Measurable f) : ∫⁻ (y : (i : ι) → X i), f (s.restrict y) ∂MeasureTheory.productMeasure μ = ∫⁻ (y : (i : { x : ι // x ∈ s }) → X ↑i), f y ∂MeasureTheory.Measure.pi fun (i : { x : ι // x ∈ s }) => μ ↑i

theorem MeasureTheory.measurable_dependsOn' {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] {s : Finset ι} {f : ((i : ι) → X i) → ENNReal} (mf : Measurable f) : DependsOn f ↑s

If a function is measurable with respect to the σ-algebra generated by the finite set of coordinates s, then it only depends on those coordinates.

theorem MeasureTheory.lintegral_measurable {ι : Type u_1} {X : ι → Type u_2} [hX : (i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [DecidableEq ι] {s : Finset ι} {f : ((i : ι) → X i) → ENNReal} (mf : Measurable f) (x : (i : ι) → X i) : ∫⁻ (y : (i : ι) → X i), f y ∂MeasureTheory.productMeasure μ = (∫⋯∫⁻_s, f ∂μ) x