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
inst_2 : OpensMeasurableSpace E
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
x : E
hxL₁ : (↑(↑(MemLp.toLp (fun (x : E) ↦ (L₁ : (a : E) → ℝ) x) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x = (L₁ : (a : E) → ℝ) x
hxL₂ : (↑(↑(MemLp.toLp (fun (x : E) ↦ (L₂ : (a : E) → ℝ) x) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x = (L₂ : (a : E) → ℝ) x
h₁ :
  HMul.hMul (β := ℝ) ((↑(↑(MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x) ((L₁ : (a : E) → ℝ) x : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
⊢ (↑(↑(MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x *
      (↑(↑(MemLp.toLp (⇑L₁ : (a : E) → ℝ) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x =
    HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
have h₂ : HMul.hMul (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) =
  HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
Tactic: rw [hxL₁, hxL₂, mul_comm]
-- 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 : OpensMeasurableSpace E
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
x : E
hxL₁ : (↑(↑(MemLp.toLp (fun (x : E) ↦ (L₁ : (a : E) → ℝ) x) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x = (L₁ : (a : E) → ℝ) x
hxL₂ : (↑(↑(MemLp.toLp (fun (x : E) ↦ (L₂ : (a : E) → ℝ) x) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x = (L₂ : (a : E) → ℝ) x
h₁ :
  HMul.hMul (β := ℝ) ((↑(↑(MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x) ((L₁ : (a : E) → ℝ) x : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
h₂ :
  HMul.hMul (α := ℝ) (β := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
⊢ (↑(↑(MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x *
      (↑(↑(MemLp.toLp (⇑L₁ : (a : E) → ℝ) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x =
    HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
have h₃ : HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) =
  HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
Tactic: rw [hxL₁, hxL₂, mul_comm]
-- 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 : OpensMeasurableSpace E
⊢ Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (uncenteredCovarianceBilinDual (mE := mE) 0) 0
have h : ∀ (x x_1 : StrongDual ℝ E),
  Eq (α := ℝ)
    ((((uncenteredCovarianceBilinDual (mE := mE) 0 : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) x :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        x_1 :
      ℝ)
    ((((0 : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) x : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ) x_1 :
      ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
inst_1 : NormedSpace ℝ E
inst_2 : OpensMeasurableSpace E
x x_1 : StrongDual ℝ E
⊢ Eq (α := ℝ)
    ((((uncenteredCovarianceBilinDual (mE := mE) 0 : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) x :
            StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        x_1 :
      ℝ)
    ((((0 : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) x : StrongDual ℝ E →L[ℝ] ℝ) : (a : StrongDual ℝ E) → ℝ) x_1 :
      ℝ)
have this : Subsingleton.{u_1 + 1} ↥(Lp ℝ 2 0)
Tactic: have : Subsingleton (Lp ℝ 2 (0 : Measure E)) := ⟨fun x y ↦ Lp.ext_iff.2 rfl⟩
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
⊢ norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) ≤
    ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
have pos : ∀ (h : MemLp id 2 μ),
  norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) ≤
    ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
pos :
  ∀ (h : MemLp id 2 μ),
    norm (E := ℝ)
        ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
                StrongDual ℝ E →L[ℝ] ℝ) :
              (a : StrongDual ℝ E) → ℝ)
            L₂ :
          ℝ) ≤
      ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
⊢ norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) ≤
    ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
have neg : ∀ (h : ¬MemLp id 2 μ),
  norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) ≤
    ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : ¬MemLp id 2 μ
⊢ norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) ≤
    ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
have neg : 0 ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
Tactic: simp only [uncenteredCovarianceBilinDual_of_not_memLp h, norm_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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) =
    norm (E := ℝ) (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
have rw : norm (E := ℝ) (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ) =
  norm (E := ℝ) (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
Tactic: rw [uncenteredCovarianceBilinDual_apply 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ LE.le (α := ℝ) (∫ (x : E), norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
    (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ)
have refine_1 : Integrable (ε := ℝ) (fun (x : E) ↦ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ))
  μ
Tactic: refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
refine_1 :
  Integrable (ε := ℝ)
    (fun (x : E) ↦ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)) μ
⊢ LE.le (α := ℝ) (∫ (x : E), norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
    (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ)
have refine_2 : Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) μ
Tactic: refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
refine_1 :
  Integrable (ε := ℝ)
    (fun (x : E) ↦ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)) μ
refine_2 : Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) μ
⊢ LE.le (α := ℝ) (∫ (x : E), norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
    (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ)
have refine_3 : ∀ (x : E),
  LE.le (α := ℝ) ((fun (x : E) ↦ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)) x)
    ((fun (x : E) ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) x)
Tactic: refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (ε := ℝ)
    (fun (x : E) ↦ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)) μ
have refine_1 : Integrable (ε := ℝ) (fun (x : E) ↦ ‖HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)‖)
  μ
Tactic: simp_rw [← norm_mul]
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) μ
have refine_2 : Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₁‖ * (‖x‖ * (‖L₂‖ * ‖x‖))) μ
Tactic: simp_rw [mul_assoc]
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₁‖ * (‖x‖ * (‖L₂‖ * ‖x‖))) μ
have refine_2 : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ * (‖L₂‖ * ‖x‖)) μ
Tactic: refine Integrable.const_mul ?_ _
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ * (‖L₂‖ * ‖x‖)) μ
have refine_2 : Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₂‖ * HPow.hPow (β := ℕ) ‖x‖ 2) μ
Tactic: simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₂‖ * HPow.hPow (β := ℕ) ‖x‖ 2) μ
have refine_2 : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ
Tactic: refine Integrable.const_mul ?_ _
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ≤ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖
have refine_3 : norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ≤ ‖L₁‖ * ‖x‖ * (‖L₂‖ * ‖x‖)
Tactic: rw [mul_assoc]
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
⊢ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ≤ ‖L₁‖ * ‖x‖ * (‖L₂‖ * ‖x‖)
have refine_3 : norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ≤ ‖L₁‖ * ‖x‖
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
inst_2 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
x : E
refine_3 : norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ≤ ‖L₁‖ * ‖x‖
⊢ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ≤ ‖L₁‖ * ‖x‖ * (‖L₂‖ * ‖x‖)
have refine_3₁ : norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ≤ ‖L₂‖ * ‖x‖
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
inst_2 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ ∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ = ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
have rw : Eq (α := ℝ) (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ) (∫ (a : E), ‖L₁‖ * ‖L₂‖ * HPow.hPow (β := ℕ) ‖a‖ 2 ∂μ)
Tactic: rw [← integral_const_mul]
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Eq (α := ℝ) (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ) (∫ (a : E), ‖L₁‖ * ‖L₂‖ * HPow.hPow (β := ℕ) ‖a‖ 2 ∂μ)
have e_f : ∀ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ = ‖L₁‖ * ‖L₂‖ * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: congr with x
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) ≤
    ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
have calc : norm (E := ℝ)
    ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ) =
  norm (E := ℝ) (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
Tactic: calc ‖uncenteredCovarianceBilinDual μ L₁ L₂‖
  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredCovarianceBilinDual_apply h]
  _ ≤ ∫ x, ‖L₁ x‖ * ‖L₂ x‖ ∂μ := (norm_integral_le_integral_norm _).trans (by simp)
  _ ≤ ∫ x, ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ := by
    refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
    · simp_rw [← norm_mul]
      exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm
    · simp_rw [mul_assoc]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]
      refine Integrable.const_mul ?_ _
      exact h.integrable_norm_pow (by simp)
    · simp only
      rw [mul_assoc]
      gcongr
      · exact ContinuousLinearMap.le_opNorm L₁ x
      · exact ContinuousLinearMap.le_opNorm L₂ x
  _ = ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
    rw [← integral_const_mul]
    congr with x
    ring
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
calc :
  norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) =
    norm (E := ℝ) (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
⊢ norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) ≤
    ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
have calc₁ : LE.le (α := ℝ) (∫ (x : E), norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
  (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ)
Tactic: calc ‖uncenteredCovarianceBilinDual μ L₁ L₂‖
  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredCovarianceBilinDual_apply h]
  _ ≤ ∫ x, ‖L₁ x‖ * ‖L₂ x‖ ∂μ := (norm_integral_le_integral_norm _).trans (by simp)
  _ ≤ ∫ x, ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ := by
    refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
    · simp_rw [← norm_mul]
      exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm
    · simp_rw [mul_assoc]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]
      refine Integrable.const_mul ?_ _
      exact h.integrable_norm_pow (by simp)
    · simp only
      rw [mul_assoc]
      gcongr
      · exact ContinuousLinearMap.le_opNorm L₁ x
      · exact ContinuousLinearMap.le_opNorm L₂ x
  _ = ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
    rw [← integral_const_mul]
    congr with x
    ring
-- 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 : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
calc :
  norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) =
    norm (E := ℝ) (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
calc₁ :
  LE.le (α := ℝ) (∫ (x : E), norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
    (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ)
⊢ norm (E := ℝ)
      ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ :
              StrongDual ℝ E →L[ℝ] ℝ) :
            (a : StrongDual ℝ E) → ℝ)
          L₂ :
        ℝ) ≤
    ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
have calc₂ : ∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ = ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ
Tactic: calc ‖uncenteredCovarianceBilinDual μ L₁ L₂‖
  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredCovarianceBilinDual_apply h]
  _ ≤ ∫ x, ‖L₁ x‖ * ‖L₂ x‖ ∂μ := (norm_integral_le_integral_norm _).trans (by simp)
  _ ≤ ∫ x, ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ := by
    refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
    · simp_rw [← norm_mul]
      exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm
    · simp_rw [mul_assoc]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]
      refine Integrable.const_mul ?_ _
      exact h.integrable_norm_pow (by simp)
    · simp only
      rw [mul_assoc]
      gcongr
      · exact ContinuousLinearMap.le_opNorm L₁ x
      · exact ContinuousLinearMap.le_opNorm L₂ x
  _ = ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
    rw [← integral_const_mul]
    congr with x
    ring
-- 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
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
⊢ Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
have h : ∀ (x : E), id x = x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
Tactic: ext
-- 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
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
⊢ MemLp id p μ
have this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
Tactic: have : (id : E → E) = fun x ↦ x - ∫ x, x ∂μ + ∫ x, x ∂μ := by ext; simp
-- 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
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
⊢ MemLp id p μ
have rw : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ) p μ
Tactic: rw [this]
-- 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
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
⊢ MemLp (ε := E) (fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ) p μ
have apply : MemLp (ε := E) (fun (x : E) ↦ ∫ (x : E), x ∂μ) p μ
Tactic: apply h_Lp.add
-- 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
p : ℝ≥0∞
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - ∫ (y : E), y ∂μ) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
⊢ MemLp (ε := E) (fun (x : E) ↦ ∫ (x : E), x ∂μ) p μ
have set : let c : E := ∫ (x : E), x ∂μ;
∀ (h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ) (this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c),
  MemLp (ε := E) (fun (x : E) ↦ c) p μ
Tactic: set c := ∫ x, x ∂μ
Cleared hypotheses: h_Lp, this
-- 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
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ
have pos : ∀ (hx : c = 0), MemLp (ε := E) (fun (x : E) ↦ c) p μ
Tactic: by_cases hx : c = 0
-- 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
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (ε := E) (fun (x : E) ↦ x - c) p μ
this : Eq.{u_1 + 1} (α := (a : E) → E) id fun (x : E) ↦ x - c + c
pos : ∀ (hx : c = 0), MemLp (ε := E) (fun (x : E) ↦ c) p μ
⊢ MemLp (ε := E) (fun (x : E) ↦ c) p μ
have neg : ∀ (hx : ¬c = 0), MemLp (ε := E) (fun (x : E) ↦ c) p μ
Tactic: by_cases hx : c = 0