mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ 0 Set.univ = 1

Tactic:
rw [hu, Measure.smul_apply, restrict_apply MeasurableSet.univ,
      Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel hns hnt]

Goal state after:
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case inl
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = 0
⊢ pdf X ℙ μ =ᵐ[μ] 0

pp: case inr
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] 0

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = 0
⊢ pdf X ℙ μ =ᵐ[μ] 0
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case inr
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] 0

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] 0
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case pos
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)

pp: case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : μ s = ∞
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case pos
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : μ s = 0
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)

pp: case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : μ s = 0
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ Measure.map X ℙ = μ.withDensity (s.indicator ((μ s)⁻¹ • 1))

pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ AEMeasurable (s.indicator ((μ s)⁻¹ • 1)) μ

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ Measure.map X ℙ = μ.withDensity (s.indicator ((μ s)⁻¹ • 1))
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ AEMeasurable (s.indicator ((μ s)⁻¹ • 1)) μ

Tactic:
·

Goal state after:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ AEMeasurable (s.indicator ((μ s)⁻¹ • 1)) μ
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝¹ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this✝ : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ ∏ i, (map (s.restrict X i) P) (t ↑i) = ∏ i ∈ s, (map (X i) P) (t i)

pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝¹ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this✝ : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict X i) P

Tactic:
·

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝¹ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this✝ : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ ∏ i, (map (s.restrict X i) P) (t ↑i) = ∏ i ∈ s, (map (X i) P) (t i)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ∞
⊢ Integrable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

pp: case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬(volume s = 0 ∨ volume s = ∞)
⊢ Integrable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

Tactic:
·

Goal state after:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : volume s = 0 ∨ volume s = ∞
⊢ Integrable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case neg.left
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
⊢ AEStronglyMeasurable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

pp: case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
⊢ HasFiniteIntegral (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

Tactic:
·

Goal state after:
case neg.left
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
⊢ AEStronglyMeasurable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case hf
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
⊢ AEMeasurable (fun ω i ↦ X i ω) P

pp: case hs
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
⊢ MeasurableSet (Set.univ.pi fun i ↦ t ↑i)

Tactic:
·

Goal state after:
case hf
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
⊢ AEMeasurable (fun ω i ↦ X i ω) P
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case hs
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
⊢ MeasurableSet (Set.univ.pi fun i ↦ t ↑i)

Tactic:
·

Goal state after:
case hs
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
⊢ MeasurableSet (Set.univ.pi fun i ↦ t ↑i)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

pp: case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : ¬AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

Tactic:
·

Goal state after:
case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : ¬AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

Tactic:
·

Goal state after:
case neg
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : ¬AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ iIndepFun (s.restrict X) P

Tactic:
iIndepFun_iff_map_fun_eq_pi_map

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ map (fun ω i ↦ s.restrict X i ω) P = Measure.pi fun i ↦ map (s.restrict X i) P

ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict X i) P
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ map (fun ω i ↦ s.restrict X i ω) P = Measure.pi fun i ↦ map (s.restrict X i) P

pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict X i) P

Tactic:
·

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
⊢ map (fun ω i ↦ s.restrict X i ω) P = Measure.pi fun i ↦ map (s.restrict X i) P
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ (∑ a ∈ s, if a ∈ s then (↑(#s))⁻¹ else 0) = 1

pp: case refine_2
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ∀ a ∉ s, (if a ∈ s then (↑(#s))⁻¹ else 0) = 0

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ (∑ a ∈ s, if a ∈ s then (↑(#s))⁻¹ else 0) = 1
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ∀ a ∉ s, (if a ∈ s then (↑(#s))⁻¹ else 0) = 0

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ∀ a ∉ s, (if a ∈ s then (↑(#s))⁻¹ else 0) = 0
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ (Measure.pi fun i ↦ map (X ↑i) P) = Measure.pi fun i ↦ map (s.restrict X i) P

pp: case hg
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable s.restrict (map (fun ω i ↦ X i ω) P)

pp: case hf
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable (fun ω i ↦ X i ω) P

Tactic:
·

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ (Measure.pi fun i ↦ map (X ↑i) P) = Measure.pi fun i ↦ map (s.restrict X i) P
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case hg
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable s.restrict (map (fun ω i ↦ X i ω) P)

pp: case hf
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable (fun ω i ↦ X i ω) P

Tactic:
·

Goal state after:
case hg
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable s.restrict (map (fun ω i ↦ X i ω) P)
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case a
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (fun ω ↦ ω i) ⟂ᵢ[infinitePi P] fun ω ↦ ω j

pp: ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (map (fun ω ↦ ω i) (infinitePi P)).prod (map (fun ω ↦ ω j) (infinitePi P)) = (P i).prod (P j)

pp: case hf
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω i) (infinitePi P)

pp: case hg
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω j) (infinitePi P)

Tactic:
·

Goal state after:
case a
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (fun ω ↦ ω i) ⟂ᵢ[infinitePi P] fun ω ↦ ω j
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (map (fun ω ↦ ω i) (infinitePi P)).prod (map (fun ω ↦ ω j) (infinitePi P)) = (P i).prod (P j)

pp: case hf
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω i) (infinitePi P)

pp: case hg
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ AEMeasurable (fun ω ↦ ω j) (infinitePi P)

Tactic:
·

Goal state after:
ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ (map (fun ω ↦ ω i) (infinitePi P)).prod (map (fun ω ↦ ω j) (infinitePi P)) = (P i).prod (P j)
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ (infinitePi fun i ↦ map (fun ω ↦ ω (f i)) (infinitePi P)) = infinitePi fun i ↦ P (f i)

pp: ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ iIndepFun (fun i ω ↦ ω (f i)) (infinitePi P)

Tactic:
·

Goal state after:
ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ (infinitePi fun i ↦ map (fun ω ↦ ω (f i)) (infinitePi P)) = infinitePi fun i ↦ P (f i)
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case inl
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : IsEmpty Ω
⊢ IsMarkovKernel (condExpKernel μ m)

pp: case inr
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : Nonempty Ω
⊢ IsMarkovKernel (condExpKernel μ m)

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : IsEmpty Ω
⊢ IsMarkovKernel (condExpKernel μ m)
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case inr
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : Nonempty Ω
⊢ IsMarkovKernel (condExpKernel μ m)

Tactic:
·

Goal state after:
case inr
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : Nonempty Ω
⊢ IsMarkovKernel (condExpKernel μ m)
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case inl
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : IsEmpty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map Function.diag μ

pp: case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map Function.diag μ

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : IsEmpty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map Function.diag μ