awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.CovarianceBilin (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : CompleteSpace E
hμ : MemLp id 2 μ
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((RCLike.re : (a : ℝ) → ℝ) ⟪((↑(covarianceOperator μ) : E →ₗ[ℝ] E) : (a : E) → E) x, x⟫ : ℝ)
have pos : LE.le (α := ℝ) 0 (∫ (z : E), HPow.hPow (β := ℕ) ⟪x, z⟫ 2 ∂μ)
Tactic: simp only [ContinuousLinearMap.coe_coe, covarianceOperator_inner hμ, ← pow_two,
      RCLike.re_to_real]
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp.toLp (⇑(u + v) : (a : E) → 𝕜) ⋯ =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)
have push_cast : MemLp.toLp (HAdd.hAdd (α := (a : E) → 𝕜) (⇑u : (a : E) → 𝕜) (⇑v : (a : E) → 𝕜)) sorry =
  HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) sorry) (MemLp.toLp (⇑v : (a : E) → 𝕜) sorry)
Tactic: push_cast
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp.toLp (HAdd.hAdd (α := (a : E) → 𝕜) (⇑u : (a : E) → 𝕜) (⇑v : (a : E) → 𝕜)) ⋯ =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)
have rw : HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) sorry) (MemLp.toLp (⇑v : (a : E) → 𝕜) sorry) =
  HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) sorry) (MemLp.toLp (⇑v : (a : E) → 𝕜) sorry)
Tactic: rw [MemLp.toLp_add]
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
rw :
  HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯) =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)
⊢ MemLp.toLp (HAdd.hAdd (α := (a : E) → 𝕜) (⇑u : (a : E) → 𝕜) (⇑v : (a : E) → 𝕜)) ⋯ =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)
have hf : MemLp.{u_1, u_2} (ε := 𝕜) (⇑u : (a : E) → 𝕜) p μ
Tactic: rw [MemLp.toLp_add]
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
rw :
  HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯) =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)
hf : MemLp.{u_1, u_2} (ε := 𝕜) (⇑u : (a : E) → 𝕜) p μ
⊢ MemLp.toLp (HAdd.hAdd (α := (a : E) → 𝕜) (⇑u : (a : E) → 𝕜) (⇑v : (a : E) → 𝕜)) ⋯ =
    HAdd.hAdd (α := ↥(Lp 𝕜 p μ)) (MemLp.toLp (⇑u : (a : E) → 𝕜) ⋯) (MemLp.toLp (⇑v : (a : E) → 𝕜) ⋯)
have hg : MemLp.{u_1, u_2} (ε := 𝕜) (⇑v : (a : E) → 𝕜) p μ
Tactic: rw [MemLp.toLp_add]
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp.toLp (⇑(c • L) : (a : E) → 𝕜) ⋯ =
    HSMul.hSMul (α := 𝕜) (β := ↥(Lp 𝕜 p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯)
have push_cast : MemLp.toLp (HSMul.hSMul (β := (a : E) → 𝕜) c (⇑L : (a : E) → 𝕜)) sorry =
  HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) (id c) (MemLp.toLp (⇑L : (a : E) → 𝕜) sorry)
Tactic: push_cast
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp.toLp (HSMul.hSMul (β := (a : E) → 𝕜) c (⇑L : (a : E) → 𝕜)) ⋯ =
    HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) (id c) (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯)
have rw : HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) c (MemLp.toLp (⇑L : (a : E) → 𝕜) sorry) =
  HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) (id c) (MemLp.toLp (⇑L : (a : E) → 𝕜) sorry)
Tactic: rw [MemLp.toLp_const_smul]
-- 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 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
rw :
  HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) c (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯) =
    HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) (id c) (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯)
⊢ MemLp.toLp (HSMul.hSMul (β := (a : E) → 𝕜) c (⇑L : (a : E) → 𝕜)) ⋯ =
    HSMul.hSMul (β := ↥(Lp 𝕜 p μ)) (id c) (MemLp.toLp (⇑L : (a : E) → 𝕜) ⋯)
have hf : MemLp.{u_1, u_2} (ε := 𝕜) (⇑L : (a : E) → 𝕜) p μ
Tactic: rw [MemLp.toLp_const_smul]
-- 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
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have pos : ∀ (h_Lp : MemLp id p μ),
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
Tactic: by_cases h_Lp : MemLp id p μ
-- 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
pos :
  ∀ (h_Lp : MemLp id p μ),
    norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      ‖L‖ * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have neg : ∀ (h_Lp : ¬MemLp id p μ),
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
Tactic: by_cases h_Lp : MemLp id p μ
-- 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 μ
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have neg : 0 ≤ ‖L‖ * (eLpNorm id p μ).toReal
Tactic: simp only [h_Lp, not_false_eq_true, toLpₗ_of_not_memLp, Lp.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
p : ℝ≥0∞
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
inst_3 : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have pos : ∀ (hp : p = 0),
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
Tactic: by_cases hp : p = 0
-- 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 μ
pos :
  ∀ (hp : p = 0),
    norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      ‖L‖ * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have neg : ∀ (hp : ¬p = 0),
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
Tactic: by_cases hp : p = 0
-- 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
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have pos : (eLpNorm.{u_1, u_2} (ε := 𝕜) (⇑L : (a : E) → 𝕜) p μ).toReal ≤ ‖L‖ * (eLpNorm id p μ).toReal
Tactic: simp only [h_Lp, toLpₗ_apply, Lp.norm_toLp]
-- 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
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have pos : ∀ (hp_top : p = ∞),
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
Tactic: by_cases hp_top : p = ∞
-- 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
pos :
  ∀ (hp_top : p = ∞),
    norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
      ‖L‖ * (eLpNorm id p μ).toReal
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have neg : ∀ (hp_top : ¬p = ∞),
  norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
Tactic: by_cases hp_top : p = ∞
-- 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 = ∞
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have pos : ∀ (h_Lp : MemLp id ∞ μ),
  (eLpNormEssSup.{u_1, u_2} (ε := 𝕜) (⇑L : (a : E) → 𝕜) μ).toReal ≤ ‖L‖ * (eLpNormEssSup id μ).toReal
Tactic: simp only [hp_top, StrongDual.toLpₗ_apply h_Lp, Lp.norm_toLp, eLpNorm_exponent_top] at h_Lp ⊢
Cleared hypotheses: h_Lp
-- 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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ (eLpNormEssSup.{u_1, u_2} (ε := 𝕜) (⇑L : (a : E) → 𝕜) μ).toReal ≤ ‖L‖ * (eLpNormEssSup id μ).toReal
have pos : ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
  ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
Tactic: simp only [eLpNormEssSup, id_eq]
-- 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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
this :
  ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ENNReal.toReal (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)
⊢ ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
have rwa : ∀
  (this :
    ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
      (‖L‖ₑ * essSup enorm μ).toReal),
  ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
Tactic: rwa [ENNReal.essSup_const_mul, ENNReal.toReal_mul, toReal_enorm] at this
Cleared hypotheses: this
-- 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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
this :
  ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ENNReal.toReal (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)
rwa :
  ∀
    (this :
      ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
        (‖L‖ₑ * essSup enorm μ).toReal),
    ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
      ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
⊢ ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
have rwa₁ : ∀
  (this :
    ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
      ‖L‖ₑ.toReal * (essSup enorm μ).toReal),
  ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
Tactic: rwa [ENNReal.essSup_const_mul, ENNReal.toReal_mul, toReal_enorm] at this
Cleared hypotheses: this
-- 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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
this :
  ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ENNReal.toReal (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)
rwa :
  ∀
    (this :
      ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
        (‖L‖ₑ * essSup enorm μ).toReal),
    ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
      ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
rwa₁ :
  ∀
    (this :
      ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
        ‖L‖ₑ.toReal * (essSup enorm μ).toReal),
    ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
      ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
⊢ ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
have rwa₂ : ∀
  (this :
    ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
      ‖L‖ * (essSup enorm μ).toReal),
  ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
Tactic: rwa [ENNReal.essSup_const_mul, ENNReal.toReal_mul, toReal_enorm] at this
Cleared hypotheses: this
-- 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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ‖L‖ * ENNReal.toReal (essSup (fun (x : E) ↦ ‖x‖ₑ) μ)
have pos : ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
  ENNReal.toReal (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)
Tactic: suffices (essSup (fun x ↦ ‖L x‖ₑ) μ).toReal ≤ (essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ).toReal by
      rwa [ENNReal.essSup_const_mul, ENNReal.toReal_mul, toReal_enorm] at this
-- 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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ENNReal.toReal (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)
have pos : Ne (α := ℝ≥0∞) (essSup (fun (x : E) ↦ ‖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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
pos : Ne (α := ℝ≥0∞) (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ) ∞
⊢ ENNReal.toReal (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ) ≤
    ENNReal.toReal (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ)
have pos₁ : LE.le (α := ℝ≥0∞) (essSup (fun (x : E) ↦ enorm.{u_2} (E := 𝕜) ((L : (a : E) → 𝕜) x : 𝕜)) μ)
  (essSup (fun (x : E) ↦ ‖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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ Ne (α := ℝ≥0∞) (essSup (fun (x : E) ↦ ‖L‖ₑ * ‖x‖ₑ) μ) ∞
have pos : ‖L‖ₑ * essSup enorm μ ≠ ∞
Tactic: rw [ENNReal.essSup_const_mul]
-- 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 = ∞
⊢ norm (E := ↥(Lp 𝕜 p μ)) ((toLpₗ μ p : (a : StrongDual 𝕜 E) → ↥(Lp 𝕜 p μ)) L : ↥(Lp 𝕜 p μ)) ≤
    ‖L‖ * (eLpNorm id p μ).toReal
have h0 : 0 < p.toReal
Tactic: have h0 : 0 < p.toReal := by simp [ENNReal.toReal_pos_iff, pos_iff_ne_zero, hp, Ne.lt_top 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
this :
  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
have refine : (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
Tactic: refine this.trans_eq ?_
-- 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 :
  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⁻¹
⊢ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
have simp : ((‖L‖ₑ ^ p.toReal).toReal * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal) ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
Tactic: simp only [ENNReal.toReal_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
this :
  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⁻¹
⊢ ((‖L‖ₑ ^ p.toReal).toReal * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal) ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
have rw : ‖L‖ * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
Tactic: 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]
-- 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 :
  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⁻¹
⊢ ‖L‖ * (∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹ = ‖L‖ * (eLpNorm id p μ).toReal
have rw : ‖L‖ * ((∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹).toReal =
  ‖L‖ * ((∫⁻ (x : E), ‖id x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)).toReal
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by simp [hp]) hp_top, ENNReal.toReal_rpow]