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

Goal state before:
pp: case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (a : Ω) in T, c ∂μ

Tactic:
]

Goal state after:
case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (a : Ω) in T, c ∂μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : ∀ (t1 t2 : Set Ω), t1 ∈ {s | MeasurableSet s} → t2 ∈ {T} → μ (t1 ∩ t2) = μ t1 * μ t2
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ c' * c * μ (s' ∩ T) = c' * μ s' * (c * μ T)

Tactic:
]

Goal state after:
case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : ∀ (t1 t2 : Set Ω), t1 ∈ {s | MeasurableSet s} → t2 ∈ {T} → μ (t1 ∩ t2) = μ t1 * μ t2
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ c' * c * μ (s' ∩ T) = c' * μ s' * (c * μ T)
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : ∀ (t1 t2 : Set Ω), t1 ∈ {s | MeasurableSet s} → t2 ∈ {T} → μ (t1 ∩ t2) = μ t1 * μ t2
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ c' * c * (μ s' * μ T) = c' * c * (μ s' * μ T)

Tactic:
]

Goal state after:
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
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
⊢ f a ∩ ⋂ n ∈ s, f n = f a ∩ ⋂ x ∈ s, f x

Tactic:
]

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
s : ↑G → Set Ω
hsS : ∀ (x : ↑G), s x ∈ S
hs_nhds : ∀ (x : ↑G), s x ∈ 𝓝 ↑x
hsG : ∀ (x : ↑G), s x ⊆ G
T₀ : Set ↑G
T₀_count : T₀.Countable
hT₀ : ⋃ i ∈ T₀, interior (s i) = ⋃ i, interior (s i)
this : G ⊆ ⋃ i, interior (s i)
⊢ ⋃ i ∈ T₀, interior (s i) ⊆ ⋃ y ∈ T₀, s y

Tactic:
]

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
s : ↑G → Set Ω
hsS : ∀ (x : ↑G), s x ∈ S
hs_nhds : ∀ (x : ↑G), s x ∈ 𝓝 ↑x
hsG : ∀ (x : ↑G), s x ⊆ G
T₀ : Set ↑G
T₀_count : T₀.Countable
hT₀ : ⋃ i ∈ T₀, interior (s i) = ⋃ i, interior (s i)
this : G ⊆ ⋃ i, interior (s i)
⊢ ⋃ i ∈ T₀, interior (s i) ⊆ ⋃ y ∈ T₀, s 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
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_t1_inter_t2 : t1 ∩ t2 = ⋂ n ∈ insert a s, f n
a' : α
ha' : (κ a') (⋂ i ∈ insert a s, f i) = ∏ i ∈ insert a s, (κ a') (f i)
⊢ (κ a') (⋂ n ∈ insert a s, f n) = (κ a') (⋂ i ∈ insert a s, f i)

Tactic:
]

Goal state after:
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
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_μ_inter : ∀ᵐ (a' : α) ∂μ, (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
has : a ∉ s
a' : α
ha1 : (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
ha2 : (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
⊢ (∏ x ∈ s, (κ a') (f x)) * (κ a') (f a) = (∏ n ∈ s, (κ a') (f n)) * (κ a') (f a)

Tactic:
]

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this✝ : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ n, f n
this : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν G))
⊢ ∃ T, (∀ t ∈ T, t ∈ S) ∧ r < ν (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G

Tactic:
]

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
T : Set (Set Ω)
TS : T ⊆ S
T_count : T.Countable
hT : ⋃ t ∈ T, t = G
this✝ : T.Nonempty
f : ℕ → Set Ω
hf : T = range f
G_eq : G = ⋃ n, f n
this : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν G))
⊢ ∃ T, (∀ t ∈ T, t ∈ S) ∧ r < ν (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
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 α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
h : ∀ᵐ (a_1 : α) ∂μ, (η a_1) (f a ∩ ⋂ n ∈ S, f n) = (η a_1) (f a) * (η a_1) (⋂ n ∈ S, f n)
a' : α
ha' : (η a') (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a') (f i)
h' : (η a') (f a ∩ ⋂ n ∈ S, f n) = (η a') (f a) * (η a') (⋂ n ∈ S, f n)
⊢ (η a') (f a ∩ ⋂ x ∈ S, f x) = (η a') (f a) * (η a') (⋂ i ∈ S, f i)

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
h : ∀ᵐ (a_1 : α) ∂μ, (η a_1) (f a ∩ ⋂ n ∈ S, f n) = (η a_1) (f a) * (η a_1) (⋂ n ∈ S, f n)
a' : α
ha' : (η a') (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a') (f i)
h' : (η a') (f a ∩ ⋂ n ∈ S, f n) = (η a') (f a) * (η a') (⋂ n ∈ S, f n)
⊢ (η a') (f a ∩ ⋂ x ∈ S, f x) = (η a') (f a) * (η a') (⋂ i ∈ S, f i)
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case add
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f' : Measurable f'
⊢ (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ +
      (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ =
    (∫⁻ (a : Ω), f' a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ +
      (∫⁻ (a : Ω), g a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
]

Goal state after:
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 α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
n : ι
hn : n ∈ S
⊢ generateFrom (π n) ≤ generateFrom p

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
n : ι
hn : n ∈ S
⊢ generateFrom (π n) ≤ generateFrom p
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h : IndepSets {s} {t} κ μ
u : Set Ω
hu : u ∈ {s}
⊢ MeasurableSet s

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h : IndepSets {s} {t} κ μ
u : Set Ω
hu : u ∈ {s}
⊢ MeasurableSet s
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h : IndepSets {s} {t} κ μ
u : Set Ω
hu : u ∈ {t}
⊢ MeasurableSet t

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
m0 : MeasurableSpace Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h : IndepSets {s} {t} κ μ
u : Set Ω
hu : u ∈ {t}
⊢ MeasurableSet t
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ

pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ (∫ (x : Ω), X x ∂μ) * Y ω - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ (∫ (x : Ω), X x ∂μ) * Y ω - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (a : Ω), X a * Y a ∂μ - ∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * Y a) μ

pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * ∫ (x : Ω), Y x ∂μ) μ

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ

pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ (∫ (x : Ω), X x ∂μ) * Y ω - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (a : Ω), X a * Y a ∂μ - ∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * Y a) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * ∫ (x : Ω), Y x ∂μ) μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ (∫ (x : Ω), X x ∂μ) * Y ω - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ((∫⁻ (x : Ω), ‖(X - fun x ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^ 2 < ∞
⊢ eVar[X; μ] < ∞

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ((∫⁻ (x : Ω), ‖(X - fun x ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^ 2 < ∞
⊢ eVar[X; μ] < ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ < ∞
⊢ eVar[X; μ] < ∞

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ < ∞
⊢ eVar[X; μ] < ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ False

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ False
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ s ∈ {s | MeasurableSet s}

Tactic:
]

Goal state after:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ s ∈ {s | MeasurableSet s}
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2) < ∞

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2) < ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
ω : Ω
⊢ X ω = X ω

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → eVar[X; μ] = ∞

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → eVar[X; μ] = ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] = eVar[X; μ]

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] ≠ ∞

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] ≠ ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) =ᵐ[μ] 0
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ = 0
⊢ 0 ≤ fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2

pp: case hfi
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ = 0
⊢ Integrable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) μ

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) =ᵐ[μ] 0
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ = 0
⊢ 0 ≤ fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2

case hfi
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ = 0
⊢ Integrable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ ∫⁻ (ω : Ω), ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ ^ 2 ∂μ =
    ∫⁻ (a : Ω), ENNReal.ofReal (c ^ 2) * ‖X a - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ ∫⁻ (ω : Ω), ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ ^ 2 ∂μ =
    ∫⁻ (a : Ω), ENNReal.ofReal (c ^ 2) * ‖X a - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case add
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
a✝ : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
⊢ (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' a ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), g a ∂μ

Tactic:
]

Goal state after: