awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ≤ 2 * ‖y‖
have linarith : 2 * ‖y‖ < ‖c‖ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
linarith : 2 * ‖y‖ < ‖c‖ → 2 / 2 = 1
⊢ ‖c‖ ≤ 2 * ‖y‖
have linarith₁ : 2 * ‖y‖ < ‖c‖ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
linarith : 2 * ‖y‖ < ‖c‖ → 2 / 2 = 1
linarith₁ : 2 * ‖y‖ < ‖c‖ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ‖c‖ ≤ 2 * ‖y‖
have linarith₂ : 2 * ‖y‖ < ‖c‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
linarith : 2 * ‖y‖ < ‖c‖ → 2 / 2 = 1
linarith₁ : 2 * ‖y‖ < ‖c‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * ‖y‖ < ‖c‖ → GT.gt (α := ℝ) 2 0
⊢ ‖c‖ ≤ 2 * ‖y‖
have linarith₃ : 2 * ‖y‖ < ‖c‖ → 1 * ‖c‖ - 2 * ‖y‖ + (2 * ‖y‖ - ‖c‖) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
⊢ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + 0 ≤
    2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have bc : 0 ≤ HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have calc : ‖c‖ ^ (↑p : ℝ) = ‖c‖ ^ ((↑p : ℝ) - 1 + 1)
Tactic: calc ‖c‖ ^ (p : ℝ)
    _ = ‖c‖ ^ ((p - 1) + 1 : ℝ) := by abel_nf
    _ = ‖c‖ ^ (p - 1 : ℝ) * ‖c‖ := by rw [Real.rpow_add (by positivity), Real.rpow_one]
    _ ≤ ‖c‖ ^ (p - 1 : ℝ) * (2 * ‖y‖) := by gcongr; linarith
    _ = 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 0 := by ring
    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by gcongr; positivity
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
calc : ‖c‖ ^ (↑p : ℝ) = ‖c‖ ^ ((↑p : ℝ) - 1 + 1)
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have calc₁ : ‖c‖ ^ ((↑p : ℝ) - 1 + 1) = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
Tactic: calc ‖c‖ ^ (p : ℝ)
    _ = ‖c‖ ^ ((p - 1) + 1 : ℝ) := by abel_nf
    _ = ‖c‖ ^ (p - 1 : ℝ) * ‖c‖ := by rw [Real.rpow_add (by positivity), Real.rpow_one]
    _ ≤ ‖c‖ ^ (p - 1 : ℝ) * (2 * ‖y‖) := by gcongr; linarith
    _ = 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 0 := by ring
    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by gcongr; positivity
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
calc : ‖c‖ ^ (↑p : ℝ) = ‖c‖ ^ ((↑p : ℝ) - 1 + 1)
calc₁ : ‖c‖ ^ ((↑p : ℝ) - 1 + 1) = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have calc₂ : ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖ ≤ ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖)
Tactic: calc ‖c‖ ^ (p : ℝ)
    _ = ‖c‖ ^ ((p - 1) + 1 : ℝ) := by abel_nf
    _ = ‖c‖ ^ (p - 1 : ℝ) * ‖c‖ := by rw [Real.rpow_add (by positivity), Real.rpow_one]
    _ ≤ ‖c‖ ^ (p - 1 : ℝ) * (2 * ‖y‖) := by gcongr; linarith
    _ = 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 0 := by ring
    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by gcongr; positivity
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
calc : ‖c‖ ^ (↑p : ℝ) = ‖c‖ ^ ((↑p : ℝ) - 1 + 1)
calc₁ : ‖c‖ ^ ((↑p : ℝ) - 1 + 1) = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
calc₂ : ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖ ≤ ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖)
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have calc₃ : ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖) = 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + 0
Tactic: calc ‖c‖ ^ (p : ℝ)
    _ = ‖c‖ ^ ((p - 1) + 1 : ℝ) := by abel_nf
    _ = ‖c‖ ^ (p - 1 : ℝ) * ‖c‖ := by rw [Real.rpow_add (by positivity), Real.rpow_one]
    _ ≤ ‖c‖ ^ (p - 1 : ℝ) * (2 * ‖y‖) := by gcongr; linarith
    _ = 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 0 := by ring
    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by gcongr; positivity
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this_1 : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
hx : ¬c = 0
I : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) (↑p : ℝ≥0∞) μ
hp0 : (↑p : ℝ≥0∞) ≠ 0
this : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (α := ℝ) 2 (↑p : ℝ≥0∞).toReal * ‖x - c‖ ^ (↑p : ℝ≥0∞).toReal) μ
h : ‖c‖ / 2 ≤ ‖y‖
calc : ‖c‖ ^ (↑p : ℝ) = ‖c‖ ^ ((↑p : ℝ) - 1 + 1)
calc₁ : ‖c‖ ^ ((↑p : ℝ) - 1 + 1) = ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖
calc₂ : ‖c‖ ^ ((↑p : ℝ) - 1) * ‖c‖ ≤ ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖)
calc₃ : ‖c‖ ^ ((↑p : ℝ) - 1) * (2 * ‖y‖) = 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + 0
⊢ ‖c‖ ^ (↑p : ℝ) ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
have calc₄ : 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + 0 ≤ 2 * ‖c‖ ^ ((↑p : ℝ) - 1) * ‖y‖ + HPow.hPow (α := ℝ) 2 (↑p : ℝ) * ‖y - c‖ ^ (↑p : ℝ)
Tactic: calc ‖c‖ ^ (p : ℝ)
    _ = ‖c‖ ^ ((p - 1) + 1 : ℝ) := by abel_nf
    _ = ‖c‖ ^ (p - 1 : ℝ) * ‖c‖ := by rw [Real.rpow_add (by positivity), Real.rpow_one]
    _ ≤ ‖c‖ ^ (p - 1 : ℝ) * (2 * ‖y‖) := by gcongr; linarith
    _ = 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 0 := by ring
    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by gcongr; positivity
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    (0 : ℝ)
have h₁ : ¬MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)
Tactic: rw [covarianceBilinDual, uncenteredCovarianceBilinDual_of_not_memLp]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ¬MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)
have h₁ : ¬MemLp (ε := E) (id ∘ fun (x : E) ↦ x - ∫ (x : E), x ∂μ) 2 μ
Tactic: rw [(measurableEmbedding_subRight _).memLp_map_measure_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    (0 : ℝ)
have h₁ : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
Tactic: apply covarianceBilinDual_of_not_memLp'
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
h : ¬MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
have h₁ : ∀ (h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ), MemLp id 2 μ
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
⊢ Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (covarianceBilinDual (mE := mE) 0) 0
have rw : Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ)
  (uncenteredCovarianceBilinDual (mE := mE) (Measure.map (fun (x : E) ↦ x - @integral _ _ _ _ mE 0 fun (x : E) ↦ x) 0))
  0
Tactic: rw [covarianceBilinDual, Measure.map_zero, uncenteredCovarianceBilinDual_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
rw :
  Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ)
    (uncenteredCovarianceBilinDual (mE := mE)
      (Measure.map (fun (x : E) ↦ x - @integral _ _ _ _ mE 0 fun (x : E) ↦ x) 0))
    0
⊢ Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (covarianceBilinDual (mE := mE) 0) 0
have rw₁ : Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (uncenteredCovarianceBilinDual (mE := mE) 0) 0
Tactic: rw [covarianceBilinDual, Measure.map_zero, uncenteredCovarianceBilinDual_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
rw :
  Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ)
    (uncenteredCovarianceBilinDual (mE := mE)
      (Measure.map (fun (x : E) ↦ x - @integral _ _ _ _ mE 0 fun (x : E) ↦ x) 0))
    0
rw₁ : Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (uncenteredCovarianceBilinDual (mE := mE) 0) 0
⊢ Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (covarianceBilinDual (mE := mE) 0) 0
have rw₂ : Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) 0 0
Tactic: rw [covarianceBilinDual, Measure.map_zero, uncenteredCovarianceBilinDual_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)
have pos : ∀ (h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ),
  Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)
Tactic: by_cases h : MemLp (fun x ↦ x - ∫ y, y ∂μ) 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
pos :
  ∀ (h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ),
    Eq (α := ℝ)
      ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ)
      ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₁ :
        ℝ)
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)
have neg : ∀ (h : ¬MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ),
  Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)
Tactic: by_cases h : MemLp (fun x ↦ x - ∫ y, y ∂μ) 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)
have h' : MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)
Tactic: have h' : MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ) :=
      (measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
h' : MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)
have pos : Eq (α := ℝ)
  ((((uncenteredCovarianceBilinDual (mE := mE) (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) :
              (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
            L₁ :
          StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      L₂ :
    ℝ)
  ((((uncenteredCovarianceBilinDual (mE := mE) (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) :
              (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
            L₂ :
          StrongDual ℝ E →L[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      L₁ :
    ℝ)
Tactic: simp_rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply h', mul_comm (L₁ _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) 2 μ
h' : MemLp (α := E) (m0 := mE) id 2 (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ)
pos :
  Eq (α := ℝ)
    ((((uncenteredCovarianceBilinDual (mE := mE) (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) :
                (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              L₁ :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((uncenteredCovarianceBilinDual (mE := mE) (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) :
                (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ)
              L₂ :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₂ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₁ :
      ℝ)
have pos₁ : Eq (α := ℝ)
  (@integral _ _ _ _ mE (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) fun (x : E) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ))
  (@integral _ _ _ _ mE (Measure.map (fun (x : E) ↦ x - ∫ (x : E), x ∂μ) μ) fun (x : E) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ((L₁ : (a : E) → ℝ) x : ℝ))
Tactic: simp_rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply h', mul_comm (L₁ _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L : StrongDual ℝ E
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L :
      ℝ)
have pos : ∀ (h : MemLp id 2 μ),
  LE.le (α := ℝ) (0 : ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L :
      ℝ)
Tactic: by_cases h : MemLp id 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
L : StrongDual ℝ E
pos :
  ∀ (h : MemLp id 2 μ),
    LE.le (α := ℝ) (0 : ℝ)
      ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L :
        ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L :
      ℝ)
have neg : ∀ (h : ¬MemLp id 2 μ),
  LE.le (α := ℝ) (0 : ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L :
      ℝ)
Tactic: by_cases h : MemLp id 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst_1 : NormedSpace ℝ E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ Eq (α := ℝ)
    ((((covarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    (∫ (x : E),
        HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
          HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ :
      ℝ)
have rw : Eq (α := ℝ)
  (∫ (x : E),
    HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) (x - ∫ (x : E), x ∂μ) : ℝ)
      ((L₂ : (a : E) → ℝ) (x - ∫ (x : E), x ∂μ) : ℝ) ∂μ)
  (∫ (x : E),
    HSub.hSub (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₁ : (a : E) → ℝ) x ∂μ : ℝ) *
      HSub.hSub (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) (∫ (x : E), (L₂ : (a : E) → ℝ) x ∂μ : ℝ) ∂μ)
Tactic: rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply,
    integral_map (by fun_prop) (by fun_prop)]