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

Goal state before:
pp: Ω : Type u_1
f g : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_meas_g : Measurable g
⊢ ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

Tactic:
revert g

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
⊢ ∀ {g : Ω → ℝ≥0∞}, Measurable g → ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
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 a ∂μ) * ∫ (x : Ω), Y x ∂μ - (∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - (∫ (a : Ω), X a ∂μ) * ∫ (x : Ω), Y x ∂μ

Tactic:
simp

Goal state after:
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 μ
⊢ 1 ≤ 2

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case e_f
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
ω : Ω
⊢ (X ω + c - (∫ (a : Ω), X a ∂μ + ∫ (a : Ω), c ∂μ)) * (Y ω - ∫ (x : Ω), Y x ∂μ) =
    (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)

Tactic:
simp

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

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : MemLp X 2 μ
hX_int : Integrable X μ
⊢ ∫ (ω : Ω), (X ω + c - (∫ (a : Ω), X a ∂μ + μ.real Set.univ • c)) ^ 2 ∂μ = ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ

Tactic:
simp

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

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ Var[X; μ] = (-1) ^ 2 * Var[X; μ]

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y Z : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
hZ : MemLp Z 2 μ
x : Ω
⊢ 1 ≤ 2

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[-X, Y; μ] = cov[-1 • X, Y; μ]

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : ι → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
x✝ : Ω
⊢ ∑ i ∈ s, X i x✝ = (∑ i ∈ s, X i) x✝

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ -1 * cov[X, Y; μ] = -cov[X, Y; μ]

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[X, -Y; μ] = cov[X, -1 • Y; μ]

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
x✝ : Ω
⊢ ∑ i, X i x✝ = (∑ i, X i) x✝

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : MeasurableSingletonClass Ω
x : Ω
⊢ ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂Measure.dirac x) ^ 2 ∂Measure.dirac x = 0

Tactic:
simp

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

Goal state before:
pp: case empty
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
hX : ∀ i ∈ ∅, MemLp (X i) 2 μ
⊢ cov[∑ i ∈ ∅, X i, Y; μ] = ∑ i ∈ ∅, cov[X i, Y; μ]

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ i ∈ insert i s

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (fun a ↦ (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
A : MemLp (X - fun ω ↦ ∫ (x : Ω), X x ∂μ) 2 μ
B : MemLp (fun x ↦ ∫ (x : Ω), X x ∂μ) 2 μ
⊢ X = (X - fun ω ↦ ∫ (x : Ω), X x ∂μ) + fun x ↦ ∫ (x : Ω), X x ∂μ

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : MemLp Y 2 μ
x✝ : Ω
⊢ ∑ i ∈ s, X i x✝ = (∑ i ∈ s, X i) x✝

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : MemLp Y 2 μ
x✝ : Ω
⊢ ∑ i, X i x✝ = (∑ i, X i) x✝

Tactic:
simp

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

Goal state before:
pp: case pos.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) = ENNReal.ofReal (∫ (a : Ω), ↑‖X a ^ 2‖₊ ∂μ)

Tactic:
simp

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

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
x✝ : Ω
⊢ ∑ i ∈ s, X i x✝ = (∑ i ∈ s, X i) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
x✝ : Ω
⊢ ∑ j ∈ t, Y j x✝ = (∑ j ∈ t, Y j) x✝

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ ↑c = ∞ → μ {x | ‖(X - fun x ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ = ∞} = 0

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X Y : Ω → ℝ
Z : Ω' ≃ᵐ Ω
⊢ cov[X, Y; Measure.map (⇑Z) μ] = cov[X ∘ ⇑Z, Y ∘ ⇑Z; μ]

Tactic:
simp_rw [covariance, integral_map_equiv, Function.comp_apply]

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

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ μ {ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = μ {ω | ↑c.toNNReal ≤ |X ω - ∫ (x : Ω), X x ∂μ|}

Tactic:
simp

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

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : X =ᵐ[μ] 0
⊢ Var[0 + Y; μ] = Var[0; μ] + Var[Y; μ]

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᵐ[μ] 0
⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᵐ[μ] 0
⊢ 2 ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᵐ[μ] 0
this : IsProbabilityMeasure μ
⊢ Var[X; μ] + 2 * 0 + Var[Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
simp

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

Goal state before:
pp: case pos
Ω : 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
⊢ Var[0; μ] = ∑ i ∈ s, Var[X i; μ]

pp: case pos
Ω : 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
⊢ ∑ i ∈ s, X i =ᵐ[μ] 0

Tactic:
variance_zero

Goal state after:
case pos
Ω : 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
⊢ 0 = ∑ i ∈ s, Var[X i; μ]

case pos
Ω : 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
⊢ ∑ i ∈ s, X i =ᵐ[μ] 0
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ 2 ≠ ⊤

Tactic:
simp

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

Goal state before:
pp: case neg.inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
j : ι
hj2 : ¬X j =ᵐ[μ] 0
hs : ∀ i ∈ {j}, MemLp (X i) 2 μ
h : (↑{j}).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ {j}, X i =ᵐ[μ] 0
hj1 : j ∈ {j}
⊢ Var[∑ i ∈ {j}, X i; μ] = ∑ i ∈ {j}, Var[X i; μ]

Tactic:
simp

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

Goal state before:
pp: Ω : 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
⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: Ω : 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
⊢ 2 ≠ ∞

Tactic:
simp

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
p : 𝓧 → Prop
hp : MeasurableSet {x | p x}
⊢ P {ω | p (X ω)} = P (X ⁻¹' {x | p x})

Tactic:
simp

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
p : 𝓧 → Prop
hp : MeasurableSet {x | p x}
⊢ P.real {ω | p (X ω)} = P.real (X ⁻¹' {x | p x})

Tactic:
simp

Goal state after:
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:
simp

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 ω) μ
⊢ 0 ≤ ∫ (ω : Ω), (b - X ω) * (X ω - a) ∂μ

Tactic:
by
        apply integral_nonneg_of_ae
        filter_upwards [ha, hb] with ω ha' hb'
        exact mul_nonneg (by linarith : 0 ≤ b - X ω) (by linarith : 0 ≤ X ω - a)

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
⊢ ∀ᵐ (x_1 : 𝓧) ∂dirac x, x_1 = x

Tactic:
simp

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 ω) μ
⊢ ∫ (ω : Ω), -X ω ^ 2 + (a + b) * X ω ∂μ - ∫ (x : Ω), a * b ∂μ = ∫ (ω : Ω), -X ω ^ 2 + (a + b) * X ω ∂μ - a * b

Tactic:
simp

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:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst✝⁴ : MeasurableSpace 𝓧
inst✝³ : MeasurableSpace 𝓨
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable f (Measure.map X μ)
hg : AEStronglyMeasurable g (Measure.map Y μ)
hE : CompleteSpace E
⊢ 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
hE : CompleteSpace E
⊢ 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case h_fin
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝³ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝² : TopologicalSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : OpensMeasurableSpace E
X : ι → Ω' → E
hX₁ : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
hX₂ : ∀ᵐ (ω : Ω') ∂μ', Tendsto (fun i ↦ X i ω) l (𝓝 (Z ω))
f : BoundedContinuousFunction E NNReal
⊢ ∫⁻ (a : Ω'), edist 0 f ∂μ' ≠ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case inl
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : IsEmpty E
⊢ TendstoInDistribution Y l Z (fun x ↦ μ'') μ'

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case e'_2
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
x✝ : Ω
⊢ (∏ i, f i ∘ X i) x✝ = ∏ i, f i (X i x✝)

Tactic:
simp

Goal state after:
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 : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
⊢ (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) =ᵐ[κ a] fun a i ↦ f (↑i) a

Tactic:
filter_upwards [ae_all_iff.2 ha] with b hb

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 : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
b : Ω
hb : ∀ (i : ↥S), f (↑i) b = AEMeasurable.mk (f ↑i) ⋯ b
⊢ (fun i ↦ AEMeasurable.mk (f ↑i) ⋯ b) = fun i ↦ f (↑i) b
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 : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
⊢ (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) =ᵐ[κ a] fun a i ↦ f (↑i) a

Tactic:
filter_upwards [ae_all_iff.2 ha] with b hb

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 : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
b : Ω
hb : ∀ (i : ↥T), f (↑i) b = AEMeasurable.mk (f ↑i) ⋯ b
⊢ (fun i ↦ AEMeasurable.mk (f ↑i) ⋯ b) = fun i ↦ f (↑i) b
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
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 : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
x✝ : Ω
⊢ x✝ ∈ (fun ω ↦ (X i ω, Y i ω)) ⁻¹' univ ×ˢ t i ↔ x✝ ∈ Y i ⁻¹' t i

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ 0 < ↑‖1 x‖₊

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝³ : (i : ι) → TopologicalSpace (β i)
inst✝² : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝¹ : ∀ (i : ι), BorelSpace (β i)
inst✝ : Preorder ι
u : (i : ι) → Ω → β i
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ ↑(natural u hum) i = MeasurableSpace.comap (fun ω j ↦ u (↑j) ω) inferInstance

Tactic:
simp_rw [natural, MeasurableSpace.comap_process_pi, iSup_subtype']

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝³ : (i : ι) → TopologicalSpace (β i)
inst✝² : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝¹ : ∀ (i : ι), BorelSpace (β i)
inst✝ : Preorder ι
u : (i : ι) → Ω → β i
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ ⨆ x, MeasurableSpace.comap (u ↑x) (mβ ↑x) = ⨆ a, MeasurableSpace.comap (u ↑a) inferInstance
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
x : Ω
⊢ x ∈ ((s j).indicator fun x ↦ 1) ⁻¹' {1} ↔ x ∈ s j

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
n : ℕ
⊢ ↑(n + 1) ≠ 0 ∨ ∑ x ∈ Finset.range (n + 1), μ (s x) ≠ 0

Tactic:
simp

Goal state after: