awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ_1 : Measure E
p_1 : ℝ≥0∞
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
s : Set (StrongDual 𝕜 E)
r : ℝ
L : StrongDual 𝕜 E
hLs : L ∈ s
hxr : ‖L‖ ≤ r
ha : 0 ≤ (eLpNorm id p μ).toReal
⊢ ‖L‖ * (eLpNorm id p μ).toReal ≤ r * (eLpNorm id p μ).toReal

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
inst_4 : Fact (1 ≤ p)
h_Lp : MemLp id p μ
L : StrongDual 𝕜 E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [toLp, h_Lp]

Premises used: StrongDual.toLp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
inst_4 : Fact (1 ≤ p)
h_Lp : ¬MemLp id p μ
L : StrongDual 𝕜 E
⊢ Eq (α := ↥(Lp 𝕜 p μ)) ((toLp μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) (0 : ↥(Lp 𝕜 p μ))

Tactic:
simp [toLp, h_Lp]

Premises used: StrongDual.toLp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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
simp :
  Eq (α := ℝ)
    ((((IsBoundedBilinearMap.toContinuousLinearMap (f := fun (p : ↥(Lp ℝ 2 μ) × ↥(Lp ℝ 2 μ)) ↦
                  ∫ (a : E), (↑(↑p.2 : E →ₘ[μ] ℝ) : E → ℝ) a * (↑(↑p.1 : E →ₘ[μ] ℝ) : E → ℝ) a ∂μ) ⋯ :
                (a : ↥(Lp ℝ 2 μ)) → ↥(Lp ℝ 2 μ) →L[ℝ] ℝ)
              (MemLp.toLp (⇑L₁ : (a : E) → ℝ) ⋯) :
            ↥(Lp ℝ 2 μ) →L[ℝ] ℝ) :
          (a : ↥(Lp ℝ 2 μ)) → ℝ)
        (MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯) :
      ℝ)
    (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ : ℝ)
⊢ Eq (α := ℝ)
    ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ : ℝ)

Tactic:
simp only [uncenteredCovarianceBilinDual, ContinuousLinearMap.bilinearComp_apply,
    StrongDual.toLp_apply h, L2.inner_def, RCLike.inner_apply, conj_trivial]

Premises used: MeasureTheory.L2.inner_def, conj_trivial, ContinuousLinearMap.bilinearComp_apply, RCLike.inner_apply, StrongDual.toLp_apply, ProbabilityTheory.uncenteredCovarianceBilinDual
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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
⊢ Eq (α := ℝ)
    ((((IsBoundedBilinearMap.toContinuousLinearMap (f := fun (p : ↥(Lp ℝ 2 μ) × ↥(Lp ℝ 2 μ)) ↦
                  ∫ (a : E), (↑(↑p.2 : E →ₘ[μ] ℝ) : E → ℝ) a * (↑(↑p.1 : E →ₘ[μ] ℝ) : E → ℝ) a ∂μ) ⋯ :
                (a : ↥(Lp ℝ 2 μ)) → ↥(Lp ℝ 2 μ) →L[ℝ] ℝ)
              (MemLp.toLp (⇑L₁ : (a : E) → ℝ) ⋯) :
            ↥(Lp ℝ 2 μ) →L[ℝ] ℝ) :
          (a : ↥(Lp ℝ 2 μ)) → ℝ)
        (MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯) :
      ℝ)
    (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ : ℝ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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
refine :
  (ae μ).EventuallyEq (β := ℝ)
    (fun (a : E) ↦
      (↑(↑(MemLp.toLp (⇑L₁ : (a : E) → ℝ) ⋯, MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯).2 : E →ₘ[μ] ℝ) : E → ℝ) a *
        (↑(↑(MemLp.toLp (⇑L₁ : (a : E) → ℝ) ⋯, MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯).1 : E →ₘ[μ] ℝ) : E → ℝ) a)
    fun (x : E) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    ((((IsBoundedBilinearMap.toContinuousLinearMap (f := fun (p : ↥(Lp ℝ 2 μ) × ↥(Lp ℝ 2 μ)) ↦
                  ∫ (a : E), (↑(↑p.2 : E →ₘ[μ] ℝ) : E → ℝ) a * (↑(↑p.1 : E →ₘ[μ] ℝ) : E → ℝ) a ∂μ) ⋯ :
                (a : ↥(Lp ℝ 2 μ)) → ↥(Lp ℝ 2 μ) →L[ℝ] ℝ)
              (MemLp.toLp (⇑L₁ : (a : E) → ℝ) ⋯) :
            ↥(Lp ℝ 2 μ) →L[ℝ] ℝ) :
          (a : ↥(Lp ℝ 2 μ)) → ℝ)
        (MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯) :
      ℝ)
    (∫ (x : E), HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ : ℝ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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
h₁ :
  ∀ (x : E)
    (hxL₁ :
      (↑(↑(MemLp.toLp (fun (x : E) ↦ (L₁ : (a : E) → ℝ) (id x)) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x = (L₁ : (a : E) → ℝ) (id x))
    (hxL₂ :
      (↑(↑(MemLp.toLp (fun (x : E) ↦ (L₂ : (a : E) → ℝ) (id x)) ⋯) : E →ₘ[μ] ℝ) : E → ℝ) x = (L₂ : (a : E) → ℝ) (id 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 : ℝ)
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (a : E) ↦
      (↑(↑(MemLp.toLp (⇑L₁ : (a : E) → ℝ) ⋯, MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯).2 : E →ₘ[μ] ℝ) : E → ℝ) a *
        (↑(↑(MemLp.toLp (⇑L₁ : (a : E) → ℝ) ⋯, MemLp.toLp (⇑L₂ : (a : E) → ℝ) ⋯).1 : E →ₘ[μ] ℝ) : E → ℝ) a)
    fun (x : E) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)

Tactic:
filter_upwards [MemLp.coeFn_toLp (h.continuousLinearMap_comp L₁),
    MemLp.coeFn_toLp (h.continuousLinearMap_comp L₂)] with x hxL₁ hxL₂

Premises used: MeasureTheory.MemLp.continuousLinearMap_comp, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 : ℝ)
h₃ 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 : ℝ)

Tactic:
rw [hxL₁, hxL₂, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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
⊢ Eq (α := ℝ)
    ((((uncenteredCovarianceBilinDual μ : (a : StrongDual ℝ E) → StrongDual ℝ E →L[ℝ] ℝ) L₁ : StrongDual ℝ E →L[ℝ] ℝ) :
          (a : StrongDual ℝ E) → ℝ)
        L₂ :
      ℝ)
    (0 : ℝ)

Tactic:
simp [uncenteredCovarianceBilinDual, StrongDual.toLp_of_not_memLp h]

Premises used: StrongDual.toLp_of_not_memLp, ProbabilityTheory.uncenteredCovarianceBilinDual
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
inst_1 : NormedSpace ℝ E
inst_2 : OpensMeasurableSpace E
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 :
        ℝ)
⊢ Eq.{u_1 + 1} (α := StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ) (uncenteredCovarianceBilinDual (mE := mE) 0) 0

Tactic:
ext
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
inst_1 : NormedSpace ℝ E
inst_2 : OpensMeasurableSpace E
x x_1 : StrongDual ℝ E
⊢ Subsingleton.{u_1 + 1} ↥(Lp ℝ 2 0)

Tactic:
have : Subsingleton (Lp ℝ 2 (0 : Measure E)) := ⟨fun x y ↦ Lp.ext_iff.2 rfl⟩
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
Goal:
E : Type u_1
inst : NormedAddCommGroup E
mE : MeasurableSpace E
inst_1 : NormedSpace ℝ E
inst_2 : OpensMeasurableSpace E
x x_1 : StrongDual ℝ E
this : Subsingleton.{u_1 + 1} ↥(Lp ℝ 2 0)
⊢ 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:
simp [uncenteredCovarianceBilinDual, Subsingleton.eq_zero (StrongDual.toLp 0 2)]

Premises used: StrongDual.toLp, Subsingleton.eq_zero, OfNat.ofNat, ProbabilityTheory.uncenteredCovarianceBilinDual
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 ∂μ
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 ∂μ
⊢ 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 μ

Premises used: id, MeasureTheory.MemLp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 μ
neg : 0 ≤ ‖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 ∂μ

Tactic:
simp only [uncenteredCovarianceBilinDual_of_not_memLp h, norm_zero]

Premises used: ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, norm_zero
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 μ
⊢ 0 ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 μ
rw 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 : ℝ) ∂μ)
⊢ 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:
rw [uncenteredCovarianceBilinDual_apply h]

Premises used: ProbabilityTheory.uncenteredCovarianceBilinDual_apply
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 (α := ℝ) (∫ (a : E), ‖HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) a : ℝ) ((L₂ : (a : E) → ℝ) a : ℝ)‖ ∂μ)
    (∫ (x : E), norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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‖ ∂μ)

Tactic:
integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)

Premises used: MeasureTheory.integral_mono_ae, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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‖) μ
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)
⊢ LE.le (α := ℝ) (∫ (x : E), norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ∂μ)
    (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ)

Tactic:
refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)

Premises used: MeasureTheory.integral_mono_ae, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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) ↦ ‖HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)‖) μ
⊢ Integrable (ε := ℝ)
    (fun (x : E) ↦ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)) μ

Tactic:
simp_rw [← norm_mul]

Premises used: norm_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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) ↦ ‖HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)‖) μ

Tactic:
(MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm

Premises used: MeasureTheory.MemLp.integrable_mul, MeasureTheory.MemLp.continuousLinearMap_comp, MeasureTheory.Integrable.norm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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) ↦ ‖HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)‖) μ

Tactic:
exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm

Premises used: MeasureTheory.MemLp.integrable_mul, MeasureTheory.MemLp.continuousLinearMap_comp, MeasureTheory.Integrable.norm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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_2 : Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₁‖ * (‖x‖ * (‖L₂‖ * ‖x‖))) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) μ

Tactic:
simp_rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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‖))) μ

Tactic:
Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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_2 : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ * (‖L₂‖ * ‖x‖)) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₁‖ * (‖x‖ * (‖L₂‖ * ‖x‖))) μ

Tactic:
refine Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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_2 : Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₂‖ * HPow.hPow (β := ℕ) ‖x‖ 2) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ * (‖L₂‖ * ‖x‖)) μ

Tactic:
simp_rw [← mul_assoc, mul_comm _ (‖L₂‖), mul_assoc, ← pow_two]

Premises used: Norm.norm, pow_two, mul_assoc, mul_comm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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) μ

Tactic:
Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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_2 : Integrable (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖L₂‖ * HPow.hPow (β := ℕ) ‖x‖ 2) μ

Tactic:
refine Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 μ
⊢ 2 ≠ 0

Tactic:
simp
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) μ

Tactic:
exact h.integrable_norm_pow (by simp)

Premises used: MeasureTheory.MemLp.integrable_norm_pow
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ≤ ‖L₁‖ * ‖x‖ * (‖L₂‖ * ‖x‖)
⊢ norm (E := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) * norm (E := ℝ) ((L₂ : (a : E) → ℝ) x : ℝ) ≤ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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‖
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‖)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 : ℝ) ≤ ‖L₁‖ * ‖x‖

Tactic:
ContinuousLinearMap.le_opNorm L₁ x

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 : ℝ) ≤ ‖L₁‖ * ‖x‖

Tactic:
exact ContinuousLinearMap.le_opNorm L₁ x

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 : ℝ) ≤ ‖L₂‖ * ‖x‖

Tactic:
ContinuousLinearMap.le_opNorm L₂ x

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 : ℝ) ≤ ‖L₂‖ * ‖x‖

Tactic:
exact ContinuousLinearMap.le_opNorm L₂ x

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 μ
rw : Eq (α := ℝ) (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ) (∫ (a : E), ‖L₁‖ * ‖L₂‖ * HPow.hPow (β := ℕ) ‖a‖ 2 ∂μ)
⊢ ∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ = ‖L₁‖ * ‖L₂‖ * ∫ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 ∂μ

Tactic:
rw [← integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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 μ
e_f : ∀ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ = ‖L₁‖ * ‖L₂‖ * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ Eq (α := ℝ) (∫ (x : E), ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ) (∫ (a : E), ‖L₁‖ * ‖L₂‖ * HPow.hPow (β := ℕ) ‖a‖ 2 ∂μ)

Tactic:
congr with x
-- Module: Mathlib.Probability.Moments.CovarianceBilinDual
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₂‖ * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
ring