awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ)
    (fun (ω : Ω) ↦
      (X ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ X x) *
        (Y ω - @integral _ _ _ _ mΩ (Measure.map Z μ) fun (x : Ω) ↦ Y x))
    (Measure.map Z μ)

Tactic:
exact (hX.sub aestronglyMeasurable_const).mul (hY.sub aestronglyMeasurable_const)

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.sub, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Z : Ω' → Ω
hX : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Z μ)
hY : AEStronglyMeasurable (m₀ := mΩ) Y (Measure.map Z μ)
hZ : AEMeasurable Z μ
⊢ covariance (mΩ := mΩ) X Y (Measure.map Z μ) = cov[fun (ω : Ω') ↦ X (Z ω), fun (ω : Ω') ↦ Y (Z ω); μ]

Tactic:
covariance_map hX hY hZ

Premises used: ProbabilityTheory.covariance_map
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
pos : ∀ (h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0), cov[X, Y; μ] = 0
neg : ∀ (h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0), cov[X, Y; μ] = 0
⊢ cov[X, Y; μ] = 0

Tactic:
by_cases h' : ∀ᵐ ω ∂μ, X ω = 0
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ cov[X, Y; μ] = 0

Tactic:
integral_eq_zero_of_ae ?_

Premises used: ProbabilityTheory.covariance, MeasureTheory.integral_eq_zero_of_ae
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0
pos : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)) 0
⊢ cov[X, Y; μ] = 0

Tactic:
refine integral_eq_zero_of_ae ?_

Premises used: MeasureTheory.integral_eq_zero_of_ae
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0
h₁ : ∀ (ω : Ω) (hω : X ω = 0), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) = 0 ω
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ)) 0

Tactic:
filter_upwards [h'] with ω hω
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0
ω : Ω
hω : X ω = 0
⊢ (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) = 0 ω

Tactic:
simp [hω, integral_eq_zero_of_ae h']

Premises used: MeasureTheory.integral_eq_zero_of_ae
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ Ne (α := ENNReal) 2 0

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ Ne (α := ENNReal) 2 ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ IsProbabilityMeasure μ

Tactic:
have := hX.isProbabilityMeasure_of_indepFun X Y (by simp) (by simp) h' h
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
this : IsProbabilityMeasure μ
neg : ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) = 0
neg₁ :
  HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) -
      HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) =
    0
neg₂ neg₃ : Eq (α := ℝ) 0 0
⊢ cov[X, Y; μ] = 0

Tactic:
rw [covariance_eq_sub hX hY, h.integral_mul_eq_mul_integral
       hX.aestronglyMeasurable hY.aestronglyMeasurable, sub_self]

Premises used: sub_self, ProbabilityTheory.covariance_eq_sub, MeasureTheory.MemLp.aestronglyMeasurable, ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ cov[fun (p : Ω × Ω') ↦ X p.1, fun (p : Ω × Ω') ↦ Y p.2; μ.prod ν] = 0

Tactic:
(indepFun_prod₀ hfμ.aemeasurable hgν.aemeasurable).covariance_eq_zero
    (hfμ.comp_fst ν) (hgν.comp_snd μ)

Premises used: MeasureTheory.MemLp.comp_snd, MeasureTheory.MemLp.aemeasurable, ProbabilityTheory.IndepFun.covariance_eq_zero, MeasureTheory.MemLp.comp_fst, ProbabilityTheory.indepFun_prod₀
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ)
    (ContinuousLinearMap.bilinearComp (covarianceBilinDual (mE := inst_2) 0)
      (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E)) (LinearIsometry.toContinuousLinearMap (toDualMap ℝ E)))
    0

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
x y : E
⊢ Eq (α := ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
      ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
h : ¬MemLp id 2 μ
h₁ :
  ∀ (x x_1 : E),
    Eq (α := ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)
      ((((0 : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)
⊢ Eq (α := E →L[ℝ] E →L[ℝ] ℝ) (covarianceBilin μ) 0

Tactic:
ext
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
h : ¬MemLp id 2 μ
x x_1 : E
⊢ Eq (α := ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)
    ((((0 : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x_1 : ℝ)

Tactic:
simp [covarianceBilin_eq_covarianceBilinDual, h]

Premises used: ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ Eq (α := ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    (∫ (z : E), ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫ ∂μ : ℝ)

Tactic:
simp [covarianceBilin, covarianceBilinDual_apply' h]

Premises used: ProbabilityTheory.covarianceBilinDual_apply', ProbabilityTheory.covarianceBilin
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
x y : E
rw :
  Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
      ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
      ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
rw₂ rw₃ :
  Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        ((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) :
      ℝ)
⊢ Eq (α := ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) y : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)

Tactic:
rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_comm,
    covarianceBilin_eq_covarianceBilinDual]

Premises used: ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, ProbabilityTheory.covarianceBilinDual_comm
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsFiniteMeasure μ
h : MemLp id 2 μ
x : E
rw :
  Var[(⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ); μ] =
    Var[fun (u : E) ↦ ⟪x, u⟫; μ]
⊢ (((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x = Var[fun (u : E) ↦ ⟪x, u⟫; μ]

Tactic:
rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_self_eq_variance h]

Premises used: ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, ProbabilityTheory.covarianceBilinDual_self_eq_variance
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsFiniteMeasure μ
h : MemLp id 2 μ
x : E
⊢ Var[(⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ); μ] =
    Var[fun (u : E) ↦ ⟪x, u⟫; μ]

Tactic:
rfl
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
rw :
  cov[(⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ),
      (⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) : (a : E) → ℝ); μ] =
    cov[fun (u : E) ↦ ⟪x, u⟫, fun (u : E) ↦ ⟪y, u⟫; μ]
⊢ (((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) y =
    cov[fun (u : E) ↦ ⟪x, u⟫, fun (u : E) ↦ ⟪y, u⟫; μ]

Tactic:
rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_eq_covariance h]

Premises used: ProbabilityTheory.covarianceBilinDual_eq_covariance, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
inst_5 : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ cov[(⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) x : StrongDual ℝ E) : (a : E) → ℝ),
      (⇑((toDualMap ℝ E : (a : E) → StrongDual ℝ E) y : StrongDual ℝ E) : (a : E) → ℝ); μ] =
    cov[fun (u : E) ↦ ⟪x, u⟫, fun (u : E) ↦ ⟪y, u⟫; μ]

Tactic:
rfl
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
pos :
  ∀ (h : MemLp id 2 μ), (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]
neg :
  ∀ (h : ¬MemLp id 2 μ),
    (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]
⊢ (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]

Tactic:
by_cases h : MemLp id 2 μ

Premises used: id, MeasureTheory.MemLp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
pos : cov[fun (u : ℝ) ↦ x * u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
⊢ (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]

Tactic:
simp only [covarianceBilin_apply_eq_cov h, RCLike.inner_apply, conj_trivial, mul_comm]

Premises used: ProbabilityTheory.covarianceBilin_apply_eq_cov, conj_trivial, RCLike.inner_apply, mul_comm
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
pos : x * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]
pos₁ : x * (y * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ u; μ]) = x * y * Var[id; μ]
pos₂ : x * y * cov[fun (u : ℝ) ↦ u, fun (u : ℝ) ↦ u; μ] = x * y * Var[id; μ]
pos₃ : x * y * Var[fun (x : ℝ) ↦ x; μ] = x * y * Var[id; μ]
pos₄ pos₅ : x * y * Var[fun (x : ℝ) ↦ x; μ] = x * y * Var[fun (x : ℝ) ↦ x; μ]
⊢ cov[fun (u : ℝ) ↦ x * u, fun (u : ℝ) ↦ y * u; μ] = x * y * Var[id; μ]

Tactic:
rw [covariance_const_mul_left, covariance_const_mul_right, ← mul_assoc,
      covariance_self aemeasurable_id', Function.id_def]

Premises used: Function.id_def, mul_assoc, ProbabilityTheory.covariance_const_mul_right, aemeasurable_id', ProbabilityTheory.covariance_const_mul_left, ProbabilityTheory.covariance_self
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x y : ℝ
h : ¬MemLp id 2 μ
⊢ (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) y = x * y * Var[id; μ]

Tactic:
simp [h, variance_of_not_memLp, aestronglyMeasurable_id]

Premises used: aestronglyMeasurable_id, ProbabilityTheory.variance_of_not_memLp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
x : ℝ
rw : x * x * Var[id; μ] = HPow.hPow (β := ℕ) x 2 * Var[id; μ]
rw₁ rw₂ : x * x * Var[id; μ] = x * x * Var[id; μ]
⊢ (((covarianceBilin μ : (a : ℝ) → ℝ →L[ℝ] ℝ) x : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) x = HPow.hPow (β := ℕ) x 2 * Var[id; μ]

Tactic:
rw [covarianceBilin_real, pow_two]

Premises used: pow_two, ProbabilityTheory.covarianceBilin_real
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)

Tactic:
simp [covarianceBilin]

Premises used: ProbabilityTheory.covarianceBilin
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (z : F) ↦
      ⟪u, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫ *
        ⟪v, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), id x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), id x ∂μ⟫ ∂μ)
h₁ : MemLp.{u_2, u_2} (α := F) (m0 := inst_6) id 2 (Measure.map (⇑L : (a : E) → F) μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilin (Measure.map (⇑L : (a : E) → F) μ) : (a : F) → F →L[ℝ] ℝ) u : F →L[ℝ] ℝ) : (a : F) → ℝ) v : ℝ)
    ((((covarianceBilin μ : (a : E) → E →L[ℝ] ℝ)
              ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u : E) :
            E →L[ℝ] ℝ) :
          (a : E) → ℝ)
        ((((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v : E) :
      ℝ)

Tactic:
rw [covarianceBilin_apply, covarianceBilin_apply h]

Premises used: ProbabilityTheory.covarianceBilin_apply
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ LE.le (α := ENNReal) 1 2

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
simp_rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (z : F) ↦
      ⟪u, HSub.hSub (β := F) z ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
        ⟪v, HSub.hSub (β := F) z ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (z : F) ↦
      ⟪u, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫ *
        ⟪v, z - @integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (x : F) ↦ id x⟫)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), id x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), id x ∂μ⟫ ∂μ)

Tactic:
simp_rw [id, L.integral_id_map (h.integrable (by simp))]

Premises used: MeasureTheory.MemLp.integrable, id, ContinuousLinearMap.integral_id_map
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
rw :
  Eq (α := ℝ)
    (∫ (x : E),
      ⟪u, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
        ⟪v, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ ∂μ)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)
hφ : AEMeasurable.{u_1, u_2} (β := F) (⇑L : (a : E) → F) μ
hfm :
  AEStronglyMeasurable (β := ℝ) (m₀ := inst_6)
    (fun (z : F) ↦
      ⟪u, HSub.hSub (β := F) z ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
        ⟪v, HSub.hSub (β := F) z ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫)
    (Measure.map (⇑L : (a : E) → F) μ)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_6 (Measure.map (⇑L : (a : E) → F) μ) fun (z : F) ↦
      ⟪u, HSub.hSub (β := F) z ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
        ⟪v, HSub.hSub (β := F) z ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)

Tactic:
rw [integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
simp_rw :
  Eq (α := ℝ)
    (∫ (x : E), ⟪u, (L : (a : E) → F) (x - ∫ (x : E), x ∂μ)⟫ * ⟪v, (L : (a : E) → F) (x - ∫ (x : E), x ∂μ)⟫ ∂μ)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)
⊢ Eq (α := ℝ)
    (∫ (x : E),
      ⟪u, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ *
        ⟪v, HSub.hSub (α := F) (β := F) ((L : (a : E) → F) x : F) ((L : (a : E) → F) (∫ (x : E), x ∂μ) : F)⟫ ∂μ)
    (∫ (z : E),
      ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) u,
          z - ∫ (x : E), x ∂μ⟫ *
        ⟪(((ContinuousLinearMap.adjoint : (a : E →L[ℝ] F) → F →L[ℝ] E) L : F →L[ℝ] E) : (a : F) → E) v,
          z - ∫ (x : E), x ∂μ⟫ ∂μ)

Tactic:
simp_rw [← map_sub, ← L.adjoint_inner_left]

Premises used: map_sub, ContinuousLinearMap.adjoint_inner_left
-- Module: Mathlib.Probability.Moments.CovarianceBilin
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace F
inst_10 : CompleteSpace E
inst_11 : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEMeasurable.{u_1, u_2} (β := F) (⇑L : (a : E) → F) μ

Tactic:
fun_prop