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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
⊢ IsFiniteMeasure P ↔ IsFiniteMeasure P

Tactic:
]

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
⊢ IsProbabilityMeasure P ↔ IsProbabilityMeasure P

Tactic:
]

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

Goal state before:
pp: case neg.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᵐ[μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᵐ[μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
i : ι
hi : i ∈ s
⊢ ∑ j ∈ s, cov[X i, X j; μ] = cov[X i, X i; μ]

Tactic:
]

Goal state after:
case neg.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᵐ[μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᵐ[μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
i : ι
hi : i ∈ s
⊢ ∑ j ∈ s, cov[X i, X j; μ] = cov[X i, X i; μ]
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ ν = ν

pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y (map X P)

Tactic:
]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y (map X P)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∑ i, Var[fun ω ↦ X i (ω i); Measure.pi μ] = ∑ i, Var[X i; μ i]

pp: case hs
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∀ i ∈ univ, MemLp (fun ω ↦ X i (ω i)) 2 (Measure.pi μ)

pp: case h
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ (↑univ).Pairwise fun i j ↦ (fun ω ↦ X i (ω i)) ⟂ᵢ[Measure.pi μ] fun ω ↦ X j (ω j)

Tactic:
]

Goal state after:
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∑ i, Var[fun ω ↦ X i (ω i); Measure.pi μ] = ∑ i, Var[X i; μ i]

case hs
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∀ i ∈ univ, MemLp (fun ω ↦ X i (ω i)) 2 (Measure.pi μ)

case h
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ (↑univ).Pairwise fun i j ↦ (fun ω ↦ X i (ω i)) ⟂ᵢ[Measure.pi μ] fun ω ↦ X j (ω j)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y μ

Tactic:
]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e_f
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ Var[X i; μ i] = Var[X i; μ i]

pp: case e_f.hX
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (X i) (Measure.map (fun ω ↦ ω i) (Measure.pi μ))

pp: case e_f.hY
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (fun ω ↦ ω i) (Measure.pi μ)

Tactic:
]

Goal state after:
case e_f.hX
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (X i) (Measure.map (fun ω ↦ ω i) (Measure.pi μ))

case e_f.hY
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (fun ω ↦ ω i) (Measure.pi μ)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ μ ∗ₘ ν = μ ∗ₘ ν

pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map X P)

pp: case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map Y P)

Tactic:
]

Goal state after:
case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map X P)

case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map Y P)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e_f.hX
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (X i) (μ i)

Tactic:
]

Goal state after:
case e_f.hX
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (X i) (μ i)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite μ

Tactic:
]

Goal state after:
case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite ν

Tactic:
]

Goal state after:
case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite ν
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : Ω), (fun x ↦ f (X x)) x ∂P = ∫ (x : Ω), f (X x) ∂P

pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (map X P)

Tactic:
]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (map X P)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (ω : Ω), f (X ω) ∂P = ∫⁻ (a : Ω), f (X a) ∂P

pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
⊢ AEMeasurable f (map X P)

Tactic:
]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
⊢ AEMeasurable f (map X P)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
⊢ AEMeasurable f μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : SecondCountableTopology E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
X : Ω → E
hX : HasLaw X μ P
⊢ ∫ (x : E), id x ∂μ = ∫ (x : E), x ∂μ

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : SecondCountableTopology E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
X : Ω → E
hX : HasLaw X μ P
⊢ ∫ (x : E), id x ∂μ = ∫ (x : E), x ∂μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ cov[f ∘ X, g ∘ X; P] = cov[f ∘ X, g ∘ X; P]

pp: case hX
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable f (map X P)

pp: case hY
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable g (map X P)

pp: case hZ
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable X P

Tactic:
]

Goal state after:
case hX
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable f (map X P)

case hY
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable g (map X P)

case hZ
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable X P
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: case hX
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable f μ

Tactic:
]

Goal state after:
case hX
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable f μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: case hY
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable g μ

Tactic:
]

Goal state after:
case hY
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable g μ
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
μ : Measure ℝ
X : Ω → ℝ
hX : HasLaw X μ P
⊢ Var[X; P] = Var[X; P]

Tactic:
]

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
P : Measure Ω
c : ℝ≥0∞
inst✝ : MeasurableSingletonClass 𝓧
x : 𝓧
hX : HasLaw X (c • dirac x) P
⊢ ∀ᵐ (y : 𝓧) ∂c • dirac x, y = x

Tactic:
]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
P : Measure Ω
c : ℝ≥0∞
inst✝ : MeasurableSingletonClass 𝓧
x : 𝓧
hX : HasLaw X (c • dirac x) P
⊢ ∀ᵐ (y : 𝓧) ∂c • dirac x, y = x
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
ω : Ω
⊢ (fun ω ↦ (b - X ω) * (X ω - a)) ω = (fun ω ↦ -X ω ^ 2 + (a + b) * X ω - a * b) ω

Tactic:
by ring

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
P : Measure Ω
x : 𝓧
hX : X =ᵐ[P] fun x_1 ↦ x
⊢ map (fun x_1 ↦ x) P = P Set.univ • dirac x

Tactic:
]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
P : Measure Ω
x : 𝓧
hX : X =ᵐ[P] fun x_1 ↦ x
⊢ map (fun x_1 ↦ x) P = P Set.univ • dirac x
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
⊢ μ.prod ν = μ.prod ν

Tactic:
]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), (X ^ 2) x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2 ≤ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), (X ^ 2) x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2 ≤ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - (∫ (x : Ω), X x ∂μ) ^ 2
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun ω ↦ (X ω, Y ω)) (μ.prod ν) P
⊢ μ.prod ν = μ.prod ν

Tactic:
]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), (X ^ 2) x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
⊢ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - (∫ (x : Ω), X x ∂μ) ^ 2 = (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)

Tactic:
by ring

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : iIndepFun X P
⊢ (Measure.pi fun i ↦ map (X i) P) = Measure.pi μ

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : iIndepFun X P
⊢ (Measure.pi fun i ↦ map (X i) P) = Measure.pi μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case neg
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB✝ : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖(B x) y‖ₑ
h : ¬Integrable (fun ω ↦ (B (f (X ω))) (g (Y ω))) μ
⊢ 0 = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
]

Goal state after:
case neg
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB✝ : ∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖(B x) y‖ₑ
h : ¬Integrable (fun ω ↦ (B (f (X ω))) (g (Y ω))) μ
⊢ 0 = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
⊢ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a) = ((b - a) / 2) ^ 2 - (∫ (x : Ω), X x ∂μ - (b + a) / 2) ^ 2

Tactic:
by ring

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

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ Var[X; μ] + Var[Y; ν] = Var[X; μ] + Var[Y; ν]

Tactic:
]

Goal state after: