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
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
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have 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⁻¹
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
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ 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⁻¹
have 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⁻¹
Tactic: rw [StrongDual.toLpₗ_apply h_Lp, Lp.norm_toLp,
    eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 ∂μ) ^ (1 / p.toReal)).toReal ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
have 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⁻¹
Tactic: simp only [one_div]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 ∂μ) ^ p.toReal⁻¹).toReal ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
have 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⁻¹)
Tactic: refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 ∂μ
⊢ (∫⁻ (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⁻¹)
have 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⁻¹
Tactic: rw [← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 ∂μ
⊢ (∫⁻ (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⁻¹
have h₁ : ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
  ENNReal.ofReal (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal
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
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 ∂μ
⊢ ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ENNReal.ofReal (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal
have h₁ : ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞
Tactic: rwa [ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞
have h₁ : ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞
Tactic: refine ENNReal.mul_ne_top (by simp) ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
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 ∂μ
⊢ ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞
have h : eLpNorm id p μ ≠ ∞
Tactic: have h := h_Lp.eLpNorm_ne_top
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
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), ‖x‖ₑ ^ p.toReal ∂μ ≠ ∞
have h₁ : (∫⁻ (x : E), ‖id x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≠ ∞
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top] at 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
μ : 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 ∂μ) ^ p.toReal⁻¹ ≤
    ENNReal.ofReal ((‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹)
have neg : ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
  ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ 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
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 ≤ ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal
have rw : enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal
Tactic: rw [← ENNReal.mul_rpow_of_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ≤ ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal
have hz : 0 ≤ p.toReal
Tactic: rw [← ENNReal.mul_rpow_of_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal
have h₁ : enorm.{u_2} (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
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), ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ = ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
have hf : Measurable (β := ℝ≥0∞) fun (x : E) ↦ ‖x‖ₑ ^ p.toReal
Tactic: rw [lintegral_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
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 ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
have calc : ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
  ∫⁻ (x : E), ‖L‖ₑ ^ p.toReal * ‖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
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 ∂μ
⊢ ∫⁻ (x : E), enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜) ^ p.toReal ∂μ ≤
    ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
have calc₁ : ∫⁻ (x : E), ‖L‖ₑ ^ p.toReal * ‖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
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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 μ))
have 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)
Tactic: refine LinearMap.continuous_of_locally_bounded _ fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ Bornology.IsVonNBounded 𝕜 (E := ↥(Lp 𝕜 p μ))
    ((⇑(toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) '' s)
have rw : ∃ (r : ℝ),
  ∀ x ∈ s,
    norm (E := ↥(Lp 𝕜 p μ))
        (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) x : ↥(Lp 𝕜 p μ)) ≤
      r
Tactic: rw [image_isVonNBounded_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
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,
      norm (E := ↥(Lp 𝕜 p μ))
          (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) x : ↥(Lp 𝕜 p μ)) ≤
        r
have hs₁ : ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
Tactic: simp_rw [isVonNBounded_iff'] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ ∃ (r : ℝ),
    ∀ x ∈ s,
      norm (E := ↥(Lp 𝕜 p μ))
          (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) x : ↥(Lp 𝕜 p μ)) ≤
        r
have 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
Tactic: obtain ⟨r, hxr⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
have 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
Tactic: refine ⟨r * (eLpNorm id p μ).toReal, fun L hLs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (hypothesis)
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
⊢ norm (E := ↥(Lp 𝕜 p μ))
      (((toLpₗ μ p : StrongDual 𝕜 E →ₗ[𝕜] ↥(Lp 𝕜 p μ)) : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    r * (eLpNorm id p μ).toReal
have hxr₁ : ‖L‖ ≤ r
Tactic: specialize hxr L hLs
Cleared hypotheses: hxr
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
have refine : ‖L‖ * (eLpNorm id p μ).toReal ≤ r * (eLpNorm id p μ).toReal
Tactic: refine (StrongDual.norm_toLpₗ_le L).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilinDual (goal)
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
⊢ ‖L‖ * (eLpNorm id p μ).toReal ≤ r * (eLpNorm id p μ).toReal
have ha : 0 ≤ (eLpNorm id p μ).toReal
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
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ 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 : ℝ) ∂μ : ℝ)
have simp : Eq (α := ℝ)
  ((((IsBoundedBilinearMap.toContinuousLinearMap (f := fun (p : ↥(Lp ℝ 2 μ) × ↥(Lp ℝ 2 μ)) ↦
                ∫ (a : E), (↑(↑p.2 : E →ₘ[μ] ℝ) : E → ℝ) a * (↑(↑p.1 : E →ₘ[μ] ℝ) : E → ℝ) a ∂μ) sorry :
              (a : ↥(Lp ℝ 2 μ)) → ↥(Lp ℝ 2 μ) →L[ℝ] ℝ)
            (MemLp.toLp (⇑L₁ : (a : E) → ℝ) sorry) :
          ↥(Lp ℝ 2 μ) →L[ℝ] ℝ) :
        (a : ↥(Lp ℝ 2 μ)) → ℝ)
      (MemLp.toLp (⇑L₂ : (a : E) → ℝ) sorry) :
    ℝ)
  (∫ (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]
-- 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
⊢ 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 : ℝ) ∂μ : ℝ)
have refine : (ae μ).EventuallyEq (β := ℝ)
  (fun (a : E) ↦
    (↑(↑(MemLp.toLp (⇑L₁ : (a : E) → ℝ) sorry, MemLp.toLp (⇑L₂ : (a : E) → ℝ) sorry).2 : E →ₘ[μ] ℝ) : E → ℝ) a *
      (↑(↑(MemLp.toLp (⇑L₁ : (a : E) → ℝ) sorry, MemLp.toLp (⇑L₂ : (a : E) → ℝ) sorry).1 : E →ₘ[μ] ℝ) : E → ℝ) a)
  fun (x : E) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
Tactic: refine integral_congr_ae ?_
-- 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
⊢ (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 : ℝ)
have h₁ : ∀ (x : E)
  (hxL₁ :
    (↑(↑(MemLp.toLp (fun (x : E) ↦ (L₁ : (a : E) → ℝ) (id x)) sorry) : E →ₘ[μ] ℝ) : E → ℝ) x = (L₁ : (a : E) → ℝ) (id x))
  (hxL₂ :
    (↑(↑(MemLp.toLp (fun (x : E) ↦ (L₂ : (a : E) → ℝ) (id x)) sorry) : E →ₘ[μ] ℝ) : E → ℝ) x = (L₂ : (a : E) → ℝ) (id x)),
  (↑(↑(MemLp.toLp (⇑L₂ : (a : E) → ℝ) sorry) : E →ₘ[μ] ℝ) : E → ℝ) x *
      (↑(↑(MemLp.toLp (⇑L₁ : (a : E) → ℝ) sorry) : E →ₘ[μ] ℝ) : E → ℝ) x =
    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₂
-- 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
⊢ (↑(↑(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 (β := ℝ) ((↑(↑(MemLp.toLp (⇑L₂ : (a : E) → ℝ) sorry) : E →ₘ[μ] ℝ) : E → ℝ) x) ((L₁ : (a : E) → ℝ) x : ℝ) =
  HMul.hMul (α := ℝ) (β := ℝ) ((L₁ : (a : E) → ℝ) x : ℝ) ((L₂ : (a : E) → ℝ) x : ℝ)
Tactic: rw [hxL₁, hxL₂, mul_comm]