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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
s : Set E
hs : MeasurableSet s
⊢ (μ.withDensity (pdf X ℙ μ)) s = (μ.withDensity (pdf X ℙ μ)) s

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X Y : Ω → E
hXY : X =ᵐ[ℙ] Y
⊢ (map Y ℙ).rnDeriv μ = (map Y ℙ).rnDeriv μ

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
⊢ ∀ᵐ (a : α) ∂μ,
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s ∩ (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t) =
      (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t)

Tactic:
]

Goal state after:
case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
⊢ ∀ᵐ (a : α) ∂μ,
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s ∩ (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t) =
      (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t)
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ μ
⊢ ℙ Set.univ = ℙ Set.univ

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ μ.withDensity (pdf X ℙ μ) = μ.withDensity f ↔ pdf X ℙ μ =ᵐ[μ] f

Tactic:
]

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ μ.withDensity (pdf X ℙ μ) = μ.withDensity f ↔ pdf X ℙ μ =ᵐ[μ] f
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ Indep (generateFrom (piiUnionInter (fun k ↦ {s k}) S)) (generateFrom (piiUnionInter (fun k ↦ {s k}) T)) η μ

Tactic:
]

Goal state after:
case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
⊢ Indep (generateFrom (piiUnionInter (fun k ↦ {s k}) S)) (generateFrom (piiUnionInter (fun k ↦ {s k}) T)) η μ
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ ℙ Set.univ ≠ ∞

Tactic:
]

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ ℙ Set.univ ≠ ∞
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : E), f x ∂map X ℙ = ∫⁻ (a : E), f a ∂map X ℙ

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable f (map X ℙ) ↔ Integrable f (μ.withDensity ((map X ℙ).rnDeriv μ))

Tactic:
]

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable f (map X ℙ) ↔ Integrable f (μ.withDensity ((map X ℙ).rnDeriv μ))
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable f (map X ℙ) ↔ Integrable f (map X ℙ)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : E), f x ∂map X ℙ = ∫ (y : E), f y ∂map X ℙ

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
hgm : AEMeasurable g (map X ℙ)
⊢ AEMeasurable (g ∘ X) ℙ ∧ (map g (map X ℙ)).HaveLebesgueDecomposition ν ∧ map g (map X ℙ) ≪ ν

Tactic:
]

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
hgm : AEMeasurable g (map X ℙ)
⊢ AEMeasurable (g ∘ X) ℙ ∧ (map g (map X ℙ)).HaveLebesgueDecomposition ν ∧ map g (map X ℙ) ≪ ν
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : SFinite ℙ
⊢ AEMeasurable X ℙ ∧ map X ℙ ≪ volume ↔ AEMeasurable X ℙ ∧ map X ℙ ≪ volume

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : SFinite ℙ
hX : AEMeasurable X ℙ
⊢ map X ℙ ≪ volume ↔ map X ℙ ≪ volume

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ∞

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ∞
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
this : (fun x ↦ ‖f x‖ₑ * g x) =ᵐ[volume] fun x ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ
⊢ ∫⁻ (a : ℝ), ‖f a‖ₑ * g a ≠ ∞

Tactic:
]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
this : (fun x ↦ ‖f x‖ₑ * g x) =ᵐ[volume] fun x ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ
⊢ ∫⁻ (a : ℝ), ‖f a‖ₑ * g a ≠ ∞
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
    (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (x : F) in t, pdf Y ℙ ν x ∂ν

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, ν s ≠ ∞
hμ : ∀ s ∈ S, ∀ (i : ι), (μ i) s ≠ ∞
A : ∀ (i : ι), (μ i).real (⋃ s ∈ t, s) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * (μ i).real (⋂ s ∈ u, s)
⊢ Tendsto (fun i ↦ ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * (μ i).real (⋂ s ∈ u, s)) l
    (𝓝 (∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * ν.real (⋂ i ∈ u, i)))

Tactic:
refine tendsto_finsetSum _ (fun u hu ↦ ?_)

Goal state after:
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, ν s ≠ ∞
hμ : ∀ s ∈ S, ∀ (i : ι), (μ i) s ≠ ∞
A : ∀ (i : ι), (μ i).real (⋃ s ∈ t, s) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * (μ i).real (⋂ s ∈ u, s)
u : Finset (Set Ω)
hu : u ∈ {u ∈ t.powerset | u.Nonempty}
⊢ Tendsto (fun i ↦ (-1) ^ (#u + 1) * (μ i).real (⋂ s ∈ u, s)) l (𝓝 ((-1) ^ (#u + 1) * ν.real (⋂ i ∈ u, i)))
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ (map (fun ω ↦ (X ω, Y ω)) ℙ = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) ↔
    map (fun ω ↦ (X ω, Y ω)) ℙ = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

pp: case hmf
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ AEMeasurable (fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)

Tactic:
]

Goal state after:
case hmf
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ AEMeasurable (fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ HasPDF (X * Y) ℙ μ

Tactic:
hasPDF_iff_of_aemeasurable (by fun_prop),

Goal state after:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ (map (X * Y) ℙ).HaveLebesgueDecomposition μ ∧ map (X * Y) ℙ ≪ μ
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ (map X ℙ ∗ₘ map Y ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ∗ₘ map Y ℙ ≪ μ

Tactic:
]

Goal state after:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ (map X ℙ ∗ₘ map Y ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ∗ₘ map Y ℙ ≪ μ
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
⊢ Tendsto (fun i ↦ (μ i) (⋃ s ∈ t, s)) l (𝓝 (ν (⋃ s ∈ t, s)))

Tactic:
have : Tendsto (fun i ↦ (μ i : Measure Ω).real (⋃ s ∈ t, s)) l
      (𝓝 ((ν : Measure Ω).real (⋃ s ∈ t, s))) := by
    apply hS.tendsto_measureReal_biUnion ht hmeas
    simpa using h

Goal state after:
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
this : Tendsto (fun i ↦ (↑(μ i)).real (⋃ s ∈ t, s)) l (𝓝 ((↑ν).real (⋃ s ∈ t, s)))
⊢ Tendsto (fun i ↦ (μ i) (⋃ s ∈ t, s)) l (𝓝 (ν (⋃ s ∈ t, s)))
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SigmaFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
⊢ (map X ℙ ∗ₘ map Y ℙ).rnDeriv μ =ᵐ[μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ

Tactic:
]

Goal state after:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SigmaFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
⊢ (map X ℙ ∗ₘ map Y ℙ).rnDeriv μ =ᵐ[μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩
h_sets_s'_univ : ∀ {i : ι}, i ∈ T → sets_s' i = univ
sets_t' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
h_sets_t'_univ : ∀ {i : ι}, i ∈ S → sets_t' i = univ
i : ι
hi : i ∈ S
⊢ MeasurableSet (sets_s ⟨i, hi⟩)

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩
h_sets_s'_univ : ∀ {i : ι}, i ∈ T → sets_s' i = univ
sets_t' : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
h_sets_t'_univ : ∀ {i : ι}, i ∈ S → sets_t' i = univ
i : ι
hi : i ∈ S
⊢ MeasurableSet (sets_s ⟨i, hi⟩)
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁷ : Group G
mG : MeasurableSpace G
inst✝⁶ : MeasurableMul₂ G
inst✝⁵ : MeasurableInv G
μ : Measure G
inst✝⁴ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝³ : SFinite μ
inst✝² : HasPDF X ℙ μ
inst✝¹ : HasPDF Y ℙ μ
inst✝ : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ (map X ℙ ∗ₘ map Y ℙ).rnDeriv μ =ᵐ[μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ

Tactic:
]

Goal state after:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁷ : Group G
mG : MeasurableSpace G
inst✝⁶ : MeasurableMul₂ G
inst✝⁵ : MeasurableInv G
μ : Measure G
inst✝⁴ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝³ : SFinite μ
inst✝² : HasPDF X ℙ μ
inst✝¹ : HasPDF Y ℙ μ
inst✝ : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ (map X ℙ ∗ₘ map Y ℙ).rnDeriv μ =ᵐ[μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
a' : α
ha' : (κ a') (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a') (f i)
⊢ (κ a') (⋂ n ∈ s, f n) = (κ a') (⋂ i ∈ s, f i)

Tactic:
]

Goal state after: