awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
neg :
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
suffices ‖L.toLpₗ μ p‖
      ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ by
    refine this.trans_eq ?_
    simp only [ENNReal.toReal_mul]
    rw [← ENNReal.toReal_rpow, Real.mul_rpow (by positivity) (by positivity),
      ← Real.rpow_mul (by positivity), mul_inv_cancel₀ h0.ne', Real.rpow_one, toReal_enorm]
    rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top, ENNReal.toReal_rpow]
    simp
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
⊢ p ≠ 0

Tactic:
simp [hp]
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
neg :
  ((∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ) ^ (1 / p.toReal)).toReal ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹

Tactic:
rw [StrongDual.toLpₗ_apply h_Lp, Lp.norm_toLp,
    eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top]

Premises used: MeasureTheory.Lp.norm_toLp, StrongDual.toLpₗ_apply, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
neg :
  ((∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ) ^ p.toReal⁻¹).toReal ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ ((∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ) ^ (1 / p.toReal)).toReal ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹

Tactic:
simp only [one_div]

Premises used: one_div
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
⊢ 0 ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹

Tactic:
positivity
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
neg :
  (∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤
    ENNReal.ofReal ((‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹)
⊢ ((∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ) ^ p.toReal⁻¹).toReal ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹

Tactic:
refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_

Premises used: ENNReal.toReal_le_of_le_ofReal
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
⊢ 0 ≤ p.toReal⁻¹

Tactic:
positivity
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
rw :
  (∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤
    ENNReal.ofReal (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ (∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤
    ENNReal.ofReal ((‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹)

Tactic:
rw [← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]

Premises used: ENNReal.ofReal_rpow_of_nonneg
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h₁ :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ENNReal.ofReal (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal
⊢ (∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤
    ENNReal.ofReal (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h₁ : ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞
⊢ ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ENNReal.ofReal (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal

Tactic:
rwa [ENNReal.ofReal_toReal]

Premises used: ENNReal.ofReal_toReal
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
⊢ ‖L‖ₑ ^ p.toReal ≠ ∞

Tactic:
simp
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h₁ : ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞
⊢ ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞

Tactic:
refine ENNReal.mul_ne_top (by simp) ?_

Premises used: ENNReal.mul_ne_top
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
⊢ eLpNorm id p μ ≠ ∞

Tactic:
have h := h_Lp.eLpNorm_ne_top
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h : eLpNorm id p μ ≠ ∞
⊢ p ≠ 0

Tactic:
simp [hp]
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h : eLpNorm id p μ ≠ ∞
⊢ (∫⁻ (x : E), ‖id x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≠ ∞

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top] at h

Premises used: MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h : (∫⁻ (x : E), ‖id x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≠ ∞
⊢ ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞

Tactic:
simpa [h0] using h
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
neg :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤
    ENNReal.ofReal ((‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹)

Tactic:
suffices ∫⁻ x, ‖L x‖ₑ ^ p.toReal ∂μ ≤ ‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ by
    rw [← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]
    gcongr
    rwa [ENNReal.ofReal_toReal]
    refine ENNReal.mul_ne_top (by simp) ?_
    have h := h_Lp.eLpNorm_ne_top
    rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top] at h
    simpa [h0] using h
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
⊢ ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ∫⁻ (x : E), ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ

Tactic:
lintegral_mono fun x ↦ ?_

Premises used: MeasureTheory.lintegral_mono
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
rw : enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal
hz : 0 ≤ p.toReal
⊢ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ≤ ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal

Tactic:
rw [← ENNReal.mul_rpow_of_nonneg]

Premises used: ENNReal.mul_rpow_of_nonneg
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ 0 ≤ p.toReal

Tactic:
positivity
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
h₁ : enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ≤ ‖L‖ₑ * ‖x‖ₑ
⊢ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ≤ ‖L‖ₑ * ‖x‖ₑ

Tactic:
L.le_opNorm_enorm x

Premises used: ContinuousLinearMap.le_opNorm_enorm
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
x : E
⊢ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ≤ ‖L‖ₑ * ‖x‖ₑ

Tactic:
exact L.le_opNorm_enorm x

Premises used: ContinuousLinearMap.le_opNorm_enorm
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
hf : Measurable (β := ℝ≥0∞) fun (x : E) ↦ ‖x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : E), ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ = ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ

Tactic:
rw [lintegral_const_mul]

Premises used: MeasureTheory.lintegral_const_mul
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
⊢ Measurable (β := ℝ≥0∞) fun (x : E) ↦ ‖x‖ₑ ^ p.toReal

Tactic:
fun_prop
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
calc :
  ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ∫⁻ (x : E), ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ
calc₁ : ∫⁻ (x : E), ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ = ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
⊢ ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ

Tactic:
calc ∫⁻ x, ‖L x‖ₑ ^ p.toReal ∂μ
  _ ≤ ∫⁻ x, ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ := by
    refine lintegral_mono fun x ↦ ?_
    rw [← ENNReal.mul_rpow_of_nonneg]
    swap; · positivity
    gcongr
    exact L.le_opNorm_enorm x
  _ = ‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ := by rw [lintegral_const_mul]; fun_prop

Premises used: ENNReal.toReal
-- 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)
⊢ Continuous[ContinuousLinearMap.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (AddHom.toFun (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜) (toLpₗ μ p)) : StrongDual 𝕜 E → ↥(Lp 𝕜 p μ))

Tactic:
LinearMap.continuous_of_locally_bounded _ fun s hs ↦ ?_

Premises used: LinearMap.continuous_of_locally_bounded
-- 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)
refine :
  ∀ (s : Set (StrongDual 𝕜 E)) (hs : Bornology.IsVonNBounded 𝕜 s),
    Bornology.IsVonNBounded 𝕜 (E := ↥(Lp 𝕜 p μ))
      ((⇑(toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) '' s)
⊢ Continuous[ContinuousLinearMap.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (AddHom.toFun (LinearMap.toAddHom (R := 𝕜) (S := 𝕜) (σ := RingHom.id 𝕜) (toLpₗ μ p)) : StrongDual 𝕜 E → ↥(Lp 𝕜 p μ))

Tactic:
refine LinearMap.continuous_of_locally_bounded _ fun s hs ↦ ?_

Premises used: LinearMap.continuous_of_locally_bounded
-- 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)
hs : Bornology.IsVonNBounded 𝕜 s
rw :
  ∃ (r : ℝ),
    ∀ x ∈ s,
      norm (E := ↥(Lp 𝕜 p μ))
          (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) x : ↥(Lp 𝕜 p μ)) ≤
        r
⊢ Bornology.IsVonNBounded 𝕜 (E := ↥(Lp 𝕜 p μ))
    ((⇑(toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) '' s)

Tactic:
rw [image_isVonNBounded_iff]

Premises used: NormedSpace.image_isVonNBounded_iff
-- 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)
hs : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r

Tactic:
simp_rw [isVonNBounded_iff'] at hs

Premises used: NormedSpace.isVonNBounded_iff'
-- 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)
hs : ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
obtain :
  ∀ (r : ℝ) (hxr : ∀ x ∈ s, ‖x‖ ≤ r),
    ∃ (r : ℝ),
      ∀ x ∈ s,
        norm (E := ↥(Lp 𝕜 p μ))
            (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) x : ↥(Lp 𝕜 p μ)) ≤
          r
⊢ ∃ (r : ℝ),
    ∀ x ∈ s,
      norm (E := ↥(Lp 𝕜 p μ))
          (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) x : ↥(Lp 𝕜 p μ)) ≤
        r

Tactic:
obtain ⟨r, hxr⟩ := hs
-- 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 : ℝ
hxr : ∀ x ∈ s, ‖x‖ ≤ r
⊢ ∃ (r : ℝ),
    ∀ x ∈ s,
      norm (E := ↥(Lp 𝕜 p μ))
          (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) x : ↥(Lp 𝕜 p μ)) ≤
        r

Tactic:
⟨r * (eLpNorm id p μ).toReal, fun L hLs ↦ ?_⟩

Premises used: HMul.hMul, id, ENNReal.toReal, Exists.intro, MeasureTheory.eLpNorm
-- 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 : ℝ
hxr : ∀ x ∈ s, ‖x‖ ≤ r
refine :
  ∀ (L : StrongDual 𝕜 E) (hLs : L ∈ s),
    norm (E := ↥(Lp 𝕜 p μ))
        (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      r * (eLpNorm id p μ).toReal
⊢ ∃ (r : ℝ),
    ∀ x ∈ s,
      norm (E := ↥(Lp 𝕜 p μ))
          (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) x : ↥(Lp 𝕜 p μ)) ≤
        r

Tactic:
refine ⟨r * (eLpNorm id p μ).toReal, fun L hLs ↦ ?_⟩
-- 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 : ℝ
hxr : ∀ x ∈ s, ‖x‖ ≤ r
L : StrongDual 𝕜 E
hLs : L ∈ s
⊢ ‖L‖ ≤ r

Tactic:
specialize hxr L hLs
-- 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
⊢ norm (E := ↥(Lp 𝕜 p μ))
      (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    r * (eLpNorm id p μ).toReal

Tactic:
(StrongDual.norm_toLpₗ_le L).trans ?_

Premises used: ENNReal.toReal, StrongDual.norm_toLpₗ_le, LE.le.trans, NNReal.toReal
-- 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
refine : ‖L‖ * (eLpNorm id p μ).toReal ≤ r * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ))
      (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    r * (eLpNorm id p μ).toReal

Tactic:
refine (StrongDual.norm_toLpₗ_le L).trans ?_

Premises used: StrongDual.norm_toLpₗ_le, LE.le.trans