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

Goal state before:
pp: case right
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ (⋂ i, f i ⁻¹' s i) = μ ((fun c x ↦ f x c) ⁻¹' univ.pi s)

Tactic:
]

Goal state after:
case right
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ (⋂ i, f i ⁻¹' s i) = μ ((fun c x ↦ f x c) ⁻¹' univ.pi s)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsZeroOrMarkovKernel κ
c : β'
X : Ω → β
⊢ Indep ⊥ (MeasurableSpace.comap X mβ) κ μ

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsZeroOrMarkovKernel κ
c : β'
X : Ω → β
⊢ Indep ⊥ (MeasurableSpace.comap X mβ) κ μ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∑' (i : ℕ), (κ a) (t2 ∩ f i) = ∑' (i : ℕ), (κ a) (f i) * (κ a) t2

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∑' (i : ℕ), (κ a) (t2 ∩ f i) = ∑' (i : ℕ), (κ a) (f i) * (κ a) t2
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
⊢ (∀ (s : Set β) (t : Set γ),
      MeasurableSet s →
        MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)) ↔
    (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g)

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
⊢ (∀ (s : Set β) (t : Set γ),
      MeasurableSet s →
        MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)) ↔
    (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case e_f
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
i : ℕ
⊢ (κ a) (f i) * (κ a) t2 = (κ a) (f i) * (κ a) t2

Tactic:
]

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

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
⊢ ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u → (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (s ×ˢ t ×ˢ u) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (s ×ˢ t ×ˢ u)

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
⊢ ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u → (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (s ×ˢ t ×ˢ u) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (s ×ˢ t ×ˢ u)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
⊢ limsup (fun i ↦ ↑((μs i) F)) L ≤ ↑(μ F)

Tactic:
]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
⊢ limsup (fun i ↦ ↑((μs i) F)) L ≤ ↑(μ F)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K)) + ↑ε) L ≤ ↑(μ F) + ↑ε

pp: case h
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ (fun i ↦ ↑((μs i) F)) ≤ᶠ[L] fun i ↦ ↑((μs i) (F ∩ K)) + ↑ε

Tactic:
]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K)) + ↑ε) L ≤ ↑(μ F) + ↑ε

case h
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ (fun i ↦ ↑((μs i) F)) ≤ᶠ[L] fun i ↦ ↑((μs i) (F ∩ K)) + ↑ε
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : α), ((κ.map fun ω ↦ (f ω, g ω)) a) (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ =
    ∫⁻ (a : α), ((κ.map f ×ₖ κ.map g) a) (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : α), ((κ.map fun ω ↦ (f ω, g ω)) a) (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ =
    ∫⁻ (a : α), ((κ.map f ×ₖ κ.map g) a) (Prod.mk a ⁻¹' u ×ˢ s ×ˢ t) ∂μ
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K))) L + ↑ε ≤ ↑(μ F) + ↑ε

Tactic:
]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K))) L + ↑ε ≤ ↑(μ F) + ↑ε
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
h₀ :
  ∏ x ∈ S, μ (f x ⁻¹' s x) = (∏ x ∈ S, (Measure.map (f x) μ) (s x)) * ∏ x with x ∉ S, (Measure.map (f x) μ) univ ∧
    μ (⋂ i ∈ S, f i ⁻¹' s i) = (∏ x ∈ S, (Measure.map (f x) μ) (s x)) * ∏ x with x ∉ S, (Measure.map (f x) μ) univ
⊢ ∏ x ∈ S, μ (f x ⁻¹' s x) = ∏ i ∈ S, μ (f i ⁻¹' s i)

Tactic:
]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
h₂ : limsup (fun i ↦ ↑((μs i) (F ∩ K))) L ≤ ↑(μ (F ∩ K))
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K))) L ≤ ↑(μ F)

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
h₂ : limsup (fun i ↦ ↑((μs i) (F ∩ K))) L ≤ ↑(μ (F ∩ K))
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K))) L ≤ ↑(μ F)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_2
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
⊢ (Measure.pi fun i ↦ Measure.map (X i) (μ i)) = Measure.pi fun i ↦ Measure.map (fun ω ↦ X i (ω i)) (Measure.pi μ)

Tactic:
]

Goal state after:
case refine_2
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
⊢ (Measure.pi fun i ↦ Measure.map (X i) (μ i)) = Measure.pi fun i ↦ Measure.map (fun ω ↦ X i (ω i)) (Measure.pi μ)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case hn
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
i j : ℕ
hij : i ≠ j
⊢ Disjoint (f i ∩ t2) (f j ∩ t2)

Tactic:
]

Goal state after:
case hn
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
i j : ℕ
hij : i ≠ j
⊢ Disjoint (f i ∩ t2) (f j ∩ t2)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
h₂ : limsup (fun i ↦ ↑((μs i) (F ∩ K))) L ≤ ↑(μ (F ∩ K))
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ ↑(μ (F ∩ K)) ≤ ↑(μ F)

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
h₂ : limsup (fun i ↦ ↑((μs i) (F ∩ K))) L ≤ ↑(μ (F ∩ K))
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ ↑(μ (F ∩ K)) ≤ ↑(μ F)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_2
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ Measure.map (fun x ↦ X i (Function.eval i x)) (Measure.pi μ) = Measure.map (fun ω ↦ X i (ω i)) (Measure.pi μ)

pp: case refine_2.hg
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (X i) (Measure.map (Function.eval i) (Measure.pi μ))

pp: case refine_2.hf
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (Function.eval i) (Measure.pi μ)

Tactic:
]

Goal state after:
case refine_2.hg
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (X i) (Measure.map (Function.eval i) (Measure.pi μ))

case refine_2.hf
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (Function.eval i) (Measure.pi μ)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_2.hg
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (X i) (μ i)

Tactic:
]

Goal state after:
case refine_2.hg
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (X i) (μ i)
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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi_mem_union : i ∈ p1 ∨ i ∈ p2
⊢ g i ∈ s i

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
i : ι
hi_mem_union : i ∈ p1 ∨ i ∈ p2
⊢ g i ∈ s i
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ (μ (⋂ i, Y i ⁻¹' t i))⁻¹ * μ ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) =
    (μ (⋂ i, Y i ⁻¹' t i))⁻¹ * μ ((⋂ i, Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i)

pp: case hms
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ MeasurableSet (⋂ i, Y i ⁻¹' t i)

Tactic:
]

Goal state after:
case hms
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ MeasurableSet (⋂ i, Y i ⁻¹' t i)