awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g_1 : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
⊢ L.compLp (f + g) = L.compLp f + L.compLp g
have h : (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g_1 : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
⊢ (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F)
have h : ∀ (a : α),
  (↑(↑(f + g) : α →ₘ[μ] E) : α → E) a = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑g : α →ₘ[μ] E) : α → E)) a →
    (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑(f + g) : α →ₘ[μ] E) : α → E) a) →
      (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a) →
        (↑(↑(L.compLp g) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑g : α →ₘ[μ] E) : α → E) a) →
          (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F) a =
              ((↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) + (↑(↑(L.compLp g) : α →ₘ[μ] F) : α → F)) a →
            (↑(↑(L.compLp (f + g)) : α →ₘ[μ] F) : α → F) a = (↑(↑(L.compLp f + L.compLp g) : α →ₘ[μ] F) : α → F) a
Tactic: filter_upwards [Lp.coeFn_add f g, coeFn_compLp L (f + g), coeFn_compLp L f,
      coeFn_compLp L g, Lp.coeFn_add (L.compLp f) (L.compLp g)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
c : 𝕜
f : ↥(Lp E p μ)
⊢ L.compLp (c • f) = HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)
have h : (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
g : E → F
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
L : E →SL[σ] F
c : 𝕜
f : ↥(Lp E p μ)
⊢ (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F)
have h : ∀ (a : α) (ha1 : (↑(↑(c • f) : α →ₘ[μ] E) : α → E) a = (c • (↑(↑f : α →ₘ[μ] E) : α → E)) a)
  (ha2 : (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑(c • f) : α →ₘ[μ] E) : α → E) a))
  (ha3 :
    (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F) a =
      HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a)
  (ha4 : (↑(↑(L.compLp f) : α →ₘ[μ] F) : α → F) a = (L : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) a)),
  (↑(↑(L.compLp (c • f)) : α →ₘ[μ] F) : α → F) a =
    (↑(↑(HSMul.hSMul (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') c : 𝕜') (L.compLp f)) : α →ₘ[μ] F) : α → F) a
Tactic: filter_upwards [Lp.coeFn_smul c f, coeFn_compLp L (c • f), Lp.coeFn_smul (σ c) (L.compLp f),
      coeFn_compLp L f] with _ ha1 ha2 ha3 ha4
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
L L' : E →SL[σ] F
⊢ compLpL p μ (L + L') = HAdd.hAdd (α := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) (compLpL p μ L) (compLpL p μ L')
have h : ∀ (f : ↥(Lp E p μ)),
  Eq (α := ↥(Lp F p μ)) ((compLpL p μ (L + L') : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f : ↥(Lp F p μ))
    ((HAdd.hAdd (α := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) (compLpL p μ L) (compLpL p μ L') :
          (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
        f :
      ↥(Lp F p μ))
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
inst_7 : Fact (1 ≤ p)
𝕜'' : Type u_8
inst_8 : NormedRing 𝕜''
inst_9 : Module 𝕜'' F
inst_10 : IsBoundedSMul 𝕜'' F
inst_11 : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
⊢ compLpL p μ (c • L) = HSMul.hSMul (β := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) c (compLpL p μ L)
have h : ∀ (f : ↥(Lp E p μ)),
  Eq (α := ↥(Lp F p μ)) ((compLpL p μ (c • L) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f : ↥(Lp F p μ))
    ((HSMul.hSMul (β := ↥(Lp E p μ) →SL[σ] ↥(Lp F p μ)) c (compLpL p μ L) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f :
      ↥(Lp F p μ))
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g_1 : E → F_1
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
⊢ compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (g + h)) =
    HAdd.hAdd (α := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g))
      (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) h))
have h₁ : ∀ (f : ↥(Lp E p μ)),
  EventuallyEq.{u_1, u_8} (β := F) (ae μ)
    (↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (g + h)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
    (↑(↑((HAdd.hAdd (α := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g))
                  (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) h)) :
                (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
              f) :
          α →ₘ[μ] F) :
      α → F)
Tactic: ext f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g_1 : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
⊢ compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (c • g)) =
    HSMul.hSMul (α := 𝕜) (β := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g))
have h : ∀ (f : ↥(Lp E p μ)),
  EventuallyEq.{u_1, u_8} (β := F) (ae μ)
    (↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (c • g)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
    (↑(↑((HSMul.hSMul (α := 𝕜) (β := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                  (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g)) :
                (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
              f) :
          α →ₘ[μ] F) :
      α → F)
Tactic: ext f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g_1 : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
f : ↥(Lp E p μ)
⊢ EventuallyEq.{u_1, u_8} (β := F) (ae μ)
    (↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (c • g)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
    (↑(↑((HSMul.hSMul (α := 𝕜) (β := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                  (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g)) :
                (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
              f) :
          α →ₘ[μ] F) :
      α → F)
have h : ∀ (x : α)
  (hx :
    (↑(↑((HSMul.hSMul (β := E →L[𝕜] F) c ((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F)).compLp f) : α →ₘ[μ] F) : α → F) x =
      (HSMul.hSMul (β := E →L[𝕜] F) c ((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F) : (a : E) → F)
        ((↑(↑f : α →ₘ[μ] E) : α → E) x))
  (hg :
    Eq.{u_8 + 1} (α := F)
      ((↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f) :
                α →ₘ[μ] F) :
            α → F)
          x :
        F)
      ((((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F))
  (hsmul :
    (↑(↑(HSMul.hSMul (β := ↥(Lp F p μ)) c
                  (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g)
                    f)) :
              α →ₘ[μ] F) :
          α → F)
        x =
      HSMul.hSMul (β := α → F) c
        (↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f) :
              α →ₘ[μ] F) :
          α → F)
        x),
  Eq.{u_8 + 1} (α := F)
    ((↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (c • g)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
      x)
    ((↑(↑((HSMul.hSMul (α := 𝕜) (β := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
                    (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g)) :
                  (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
                f) :
            α →ₘ[μ] F) :
        α → F)
      x)
Tactic: filter_upwards [(c • B g).coeFn_compLp f, (B g).coeFn_compLp f,
      Lp.coeFn_smul c ((B g).compLp f)] with x hx hg hsmul
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
c : G
f : ↥(Lp E p μ)
⊢ norm (E := ↥(Lp F p μ))
      ((((compLpₗ₂ p μ B : (a : G) → ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) c : ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) :
            (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
          f :
        ↥(Lp F p μ)) ≤
    ‖B‖ * ‖c‖ * ‖f‖
have simp : norm (E := ↥(Lp F p μ))
    (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) c) f) ≤
  ‖B‖ * ‖c‖ * ‖f‖
Tactic: simp only [compLpₗ₂_apply, compLpₗ_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
c : G
f : ↥(Lp E p μ)
⊢ norm (E := ↥(Lp F p μ))
      (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) c) f) ≤
    ‖B‖ * ‖c‖ * ‖f‖
have grw : norm (E := E →L[𝕜] F) ((B : (a : G) → E →L[𝕜] F) c : E →L[𝕜] F) * ‖f‖ ≤ ‖B‖ * ‖c‖ * ‖f‖
Tactic: grw [norm_compLp_le, le_opNorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g : E → F_1
c_1 : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
c : G
f : ↥(Lp E p μ)
grw : norm (E := E →L[𝕜] F) ((B : (a : G) → E →L[𝕜] F) c : E →L[𝕜] F) * ‖f‖ ≤ ‖B‖ * ‖c‖ * ‖f‖
⊢ norm (E := ↥(Lp F p μ))
      (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) c) f) ≤
    ‖B‖ * ‖c‖ * ‖f‖
have grw₁ : ‖B‖ * ‖c‖ * ‖f‖ ≤ ‖B‖ * ‖c‖ * ‖f‖
Tactic: grw [norm_compLp_le, le_opNorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
⊢ ∀ᵐ (a : α) ∂μ, (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
have h : ∀ (a : α) (h₁ : (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a) 0)
  (h₂ : (↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a = (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ)) a),
  (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
Tactic: filter_upwards [coeFn_posPart (-f), coeFn_neg f] with _ h₁ h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h₁ : (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a = (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ)) a
⊢ (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
have h : max ((↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
Tactic: rw [h₁, h₂, Pi.neg_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h₁ : (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a = (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ)) a
h : max ((↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
⊢ (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
have h₃ : max ((-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ)) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
Tactic: rw [h₁, h₂, Pi.neg_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h₁ : (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a = (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ)) a
h : max ((↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₃ : max ((-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ)) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
⊢ (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
have h₄ : max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
Tactic: rw [h₁, h₂, Pi.neg_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h : (↑(↑(negPart f) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
⊢ (↑(↑(negPart f) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
have rw : max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = -min ((↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
Tactic: rw [h, ← max_neg_neg, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h : (↑(↑(negPart f) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
rw : max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = -min ((↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
⊢ (↑(↑(negPart f) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
have rw₁ : max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) (-0)
Tactic: rw [h, ← max_neg_neg, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h : (↑(↑(negPart f) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
rw : max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = -min ((↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
rw₁ : max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) (-0)
⊢ (↑(↑(negPart f) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
have rw₂ : max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
Tactic: rw [h, ← max_neg_neg, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
inst_1 : Nonempty ι
inst_2 : LinearOrder ι
f : ι → α → E
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
h_no_pow : ∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ = ∫⁻ (a : α), liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop ∂μ
⊢ eLpNorm' f_lim p μ = (∫⁻ (a : α), liminf (fun (x : ι) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)
have rw : (∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), liminf (fun (x : ι) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)
Tactic: rw [eLpNorm'_eq_lintegral_enorm, h_no_pow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
inst_1 : Nonempty ι
inst_2 : LinearOrder ι
f : ι → α → E
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
h_no_pow : ∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ = ∫⁻ (a : α), liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop ∂μ
rw : (∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), liminf (fun (x : ι) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)
⊢ eLpNorm' f_lim p μ = (∫⁻ (a : α), liminf (fun (x : ι) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)
have rw₁ : (∫⁻ (a : α), liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop ∂μ) ^ (1 / p) =
  (∫⁻ (a : α), liminf (fun (x : ι) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)
Tactic: rw [eLpNorm'_eq_lintegral_enorm, h_no_pow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
inst_1 : Nonempty ι
inst_2 : LinearOrder ι
f : ι → α → E
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm' f_lim p μ = (∫⁻ (a : α), liminf (fun (x : ι) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)
have suffices : ∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ = ∫⁻ (a : α), liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop ∂μ
Tactic: suffices h_no_pow : (∫⁻ a, ‖f_lim a‖ₑ ^ p ∂μ) = ∫⁻ a, atTop.liminf fun m => ‖f m a‖ₑ ^ p ∂μ by
    rw [eLpNorm'_eq_lintegral_enorm, h_no_pow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
inst_1 : Nonempty ι
inst_2 : LinearOrder ι
f : ι → α → E
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ ∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ = ∫⁻ (a : α), liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop ∂μ
have refine : ∀ (a : α) (ha : Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (f_lim a))),
  Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖f_lim a‖ₑ ^ p) a)
    ((fun (a : α) ↦ (liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop : ℝ≥0∞)) a)
Tactic: refine lintegral_congr_ae (h_lim.mono fun a ha => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
inst_1 : Nonempty ι
inst_2 : LinearOrder ι
f : ι → α → E
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (f_lim a))
⊢ ‖f_lim a‖ₑ ^ p = liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop
have rw : Tendsto (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop (𝓝 (‖f_lim a‖ₑ ^ p))
Tactic: rw [Tendsto.liminf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
ι : Type u_3
inst_1 : Nonempty ι
inst_2 : LinearOrder ι
f : ι → α → E
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (f_lim x))
a : α
ha : Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (f_lim a))
⊢ Tendsto (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop (𝓝 (‖f_lim a‖ₑ ^ p))
have refine : Tendsto (fun (m : ι) ↦ ‖f m a‖ₑ) atTop (𝓝 (↑‖f_lim a‖₊ : ℝ≥0∞))
Tactic: refine (ENNReal.continuous_rpow_const.tendsto ‖f_lim a‖₊).comp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm' f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop
have rw : (∫⁻ (a : α), liminf (fun (x : ℕ) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p) ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop
Tactic: rw [eLpNorm'_lim_eq_lintegral_liminf h_lim]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Complete (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ (∫⁻ (a : α), liminf (fun (x : ℕ) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p) ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop
have rw : ∫⁻ (a : α), liminf (fun (x : ℕ) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ ≤
  HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p
Tactic: rw [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]