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

Goal state before:
pp: case inr.refine_2.refine_1
α : 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 ∈ S, f n ∈ {s | MeasurableSet s}

Tactic:
·

Goal state after:
case inr.refine_2.refine_1
α : 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 ∈ S, f n ∈ {s | MeasurableSet s}
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case iSup
Ω : 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 : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ),
            ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ =
              (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ) →
          ∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω * T.indicator (fun x ↦ c) ω ∂μ =
            (∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
·

Goal state after:
case iSup
Ω : 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 : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ),
            ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ =
              (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ) →
          ∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω * T.indicator (fun x ↦ c) ω ∂μ =
            (∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f n x) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ s' ∈ {s | MeasurableSet s}

pp: case refine_2
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ t' ∈ {s | MeasurableSet s}

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ s' ∈ {s | MeasurableSet s}
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ s' ∈ {s | MeasurableSet s}

Tactic:
induction s', hs' using generateFrom_induction with

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

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ t' ∈ {s | MeasurableSet s}

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ t' ∈ {s | MeasurableSet s}
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ IndepSet s t κ μ

Tactic:
by
  refine fun s' t' hs' ht' => h_indep s' t' ?_ ?_
  · induction s', hs' using generateFrom_induction with
    | hC t ht => exact ht ▸ hs
    | empty => exact @MeasurableSet.empty _ m₁
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf
  · induction t', ht' using generateFrom_induction with
    | hC s hs => exact hs ▸ ht
    | empty => exact @MeasurableSet.empty _ m₂
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf

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

Goal state before:
pp: case iSup
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ⨆ n, ∫⁻ (a : Ω), f n a * T.indicator (fun x ↦ c) a ∂μ =
    ⨆ i, (∫⁻ (a : Ω), f i a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

pp: case iSup.hf
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ∀ (n : ℕ), Measurable fun ω ↦ f n ω * T.indicator (fun x ↦ c) ω

pp: case iSup.h_mono
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ Monotone fun i ω ↦ f i ω * T.indicator (fun x ↦ c) ω

Tactic:
·

Goal state after:
case iSup
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ⨆ n, ∫⁻ (a : Ω), f n a * T.indicator (fun x ↦ c) a ∂μ =
    ⨆ i, (∫⁻ (a : Ω), f i a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case iSup.hf
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ∀ (n : ℕ), Measurable fun ω ↦ f n ω * T.indicator (fun x ↦ c) ω

pp: case iSup.h_mono
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ Monotone fun i ω ↦ f i ω * T.indicator (fun x ↦ c) ω

Tactic:
·

Goal state after:
case iSup.hf
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ∀ (n : ℕ), Measurable fun ω ↦ f n ω * T.indicator (fun x ↦ c) ω
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 ∂μ - ∫ (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 : Ω), X x ∂μ) * 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 : Ω), 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 ∂μ - ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case iSup.h_mono
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ Monotone fun i ω ↦ f i ω * T.indicator (fun x ↦ c) ω

Tactic:
·

Goal state after:
case iSup.h_mono
Ω : 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 : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ Monotone fun i ω ↦ f i ω * T.indicator (fun x ↦ c) ω
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case indicator
Ω : 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 Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), f ω * s.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), s.indicator (fun x ↦ c) ω ∂μ

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_1 g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * f_1 ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 ω ∂μ →
            ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
              ∫⁻ (ω : Ω), f ω * (f_1 + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f_1 + g) ω ∂μ

pp: case iSup
Ω : 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_1 : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f_1 n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 n ω ∂μ) →
          ∫⁻ (ω : Ω), f ω * (fun x ↦ ⨆ n, f_1 n x) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f_1 n x) ω ∂μ

Tactic:
·

Goal state after:
case indicator
Ω : 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 Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), f ω * s.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), s.indicator (fun x ↦ c) ω ∂μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
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 : Ω), X x ∂μ) * 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 : Ω), 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:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
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_1 g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * f_1 ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 ω ∂μ →
            ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
              ∫⁻ (ω : Ω), f ω * (f_1 + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f_1 + g) ω ∂μ

pp: case iSup
Ω : 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_1 : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f_1 n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 n ω ∂μ) →
          ∫⁻ (ω : Ω), f ω * (fun x ↦ ⨆ n, f_1 n x) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun x ↦ ⨆ n, f_1 n x) ω ∂μ

Tactic:
·

Goal state after:
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_1 g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * f_1 ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 ω ∂μ →
            ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
              ∫⁻ (ω : Ω), f ω * (f_1 + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f_1 + g) ω ∂μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
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 : Ω), 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:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
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:
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) μ
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 ∂μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
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:
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
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
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:
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 ∂μ) μ