awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
neg : Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ))
⊢ Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ)) ∧
    ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℂ) {(↑t : ℂ)}ᶜ (↑(xs n) : ℂ)
have neg₁ : ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℂ) {(↑t : ℂ)}ᶜ (↑(xs n) : ℂ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ))
have neg : Tendsto xs atTop (𝓝 t)
Tactic: rw [tendsto_ofReal_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
have refine : μ = 0 ↔ μ' = 0
Tactic: refine eqOn_complexMGF_of_mgf' hXY ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : complexMGF X μ = complexMGF Y μ'
⊢ Eq (α := Measure ℝ) (Measure.map X μ) (Measure.map Y μ')
have inner_ne_zero : ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
Tactic: have inner_ne_zero (x : ℝ) (h : x ≠ 0) : innerₗ ℝ x ≠ 0 :=
    DFunLike.ne_iff.mpr ⟨x, inner_self_ne_zero.mpr h⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : complexMGF X μ = complexMGF Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
⊢ Eq (α := Measure ℝ) (Measure.map X μ) (Measure.map Y μ')
have apply : ∀ (w : ℝ),
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar sorry w : (a : ℝ) → ℂ) v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar sorry w : (a : ℝ) → ℂ) v)
Tactic: apply MeasureTheory.ext_of_integral_char_eq continuous_probChar probChar_ne_one inner_ne_zero
    continuous_inner (fun w ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : complexMGF X μ = complexMGF Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
have rw : ∀ (h : ∀ (x : ℂ), complexMGF X μ x = complexMGF Y μ' x)
  (inner_ne_zero :
    ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ))
  (w : ℝ),
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar sorry w : (a : ℝ) → ℂ) v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar sorry w : (a : ℝ) → ℂ) v)
Tactic: rw [funext_iff] at h
Cleared hypotheses: h, inner_ne_zero, w
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : ∀ (x : ℂ), complexMGF X μ x = complexMGF Y μ' x
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
have h₁ : complexMGF X μ ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * I) =
  complexMGF Y μ' ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * I)
Tactic: specialize h (Multiplicative.toAdd w * I)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
h :
  complexMGF X μ ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * I) =
    complexMGF Y μ' ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * I)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
have h₁ : Eq (α := ℂ) (∫ (ω : Ω), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(X ω) : ℂ) * I) ∂μ)
  (∫ (ω : Ω'), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(Y ω) : ℂ) * I) ∂μ')
Tactic: simp_rw [complexMGF, mul_assoc, mul_comm I, ← mul_assoc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
h :
  Eq (α := ℂ) (∫ (ω : Ω), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(X ω) : ℂ) * I) ∂μ)
    (∫ (ω : Ω'), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(Y ω) : ℂ) * I) ∂μ')
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
have simp : Eq (α := ℂ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
  (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
Tactic: simp only [BoundedContinuousFunction.char_apply, innerₗ_apply_apply,
    RCLike.inner_apply, conj_trivial, probChar_apply, ofReal_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
h :
  Eq (α := ℂ) (∫ (ω : Ω), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(X ω) : ℂ) * I) ∂μ)
    (∫ (ω : Ω'), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(Y ω) : ℂ) * I) ∂μ')
⊢ Eq (α := ℂ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
have rwa : Eq (α := ℂ) (∫ (x : Ω), cexp ((↑w : ℂ) * (↑(X x) : ℂ) * I) ∂μ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
Tactic: rwa [integral_map hX (by fun_prop), integral_map hY (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
h :
  Eq (α := ℂ) (∫ (ω : Ω), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(X ω) : ℂ) * I) ∂μ)
    (∫ (ω : Ω'), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(Y ω) : ℂ) * I) ∂μ')
rwa :
  Eq (α := ℂ) (∫ (x : Ω), cexp ((↑w : ℂ) * (↑(X x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
⊢ Eq (α := ℂ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
have rwa₁ : Eq (α := ℂ) (∫ (x : Ω), cexp ((↑w : ℂ) * (↑(X x) : ℂ) * I) ∂μ) (∫ (x : Ω'), cexp ((↑w : ℂ) * (↑(Y x) : ℂ) * I) ∂μ')
Tactic: rwa [integral_map hX (by fun_prop), integral_map hY (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ cov[X, Y; μ] = ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have simp_rw : ∫ (ω : Ω),
    X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
      ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
  ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
Tactic: simp_rw [covariance, sub_mul, mul_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have rw : HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ)
    (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
  ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
Tactic: rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ)
      (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hf : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ
Tactic: rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ)
      (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hg : Integrable (ε := ℝ)
  (fun (ω : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
Tactic: rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ)
      (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have rw : HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
    ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ =
  ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
Tactic: rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ)
      (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ
Tactic: rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ)
      (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * ∫ (x : Ω), Y x ∂μ) μ
Tactic: rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have rw : HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
    HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
      (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
  ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
Tactic: rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
Tactic: rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
Tactic: rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have repeat : HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
    HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
      (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
  ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
Tactic: repeat rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
repeat :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
Tactic: repeat rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
repeat :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
Tactic: repeat rw [integral_sub]
-- Lean 4 proof step from Mathlib.Probability.Moments.Covariance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
repeat :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have hf₁ : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ
Tactic: repeat rw [integral_sub]