awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedSpace 𝕜 E
F : Type u_8
G : Type u_9
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
⊢ norm (E := G →L[𝕜] ↥(Lp E p μ) →L[𝕜] ↥(Lp F p μ)) (compLpL₂ p μ B) ≤ ‖B‖

Tactic:
LinearMap.mkContinuous₂_norm_le _ (norm_nonneg _) _

Premises used: LinearMap.mkContinuous₂_norm_le, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
⊢ LipschitzWith (β := ℝ) 1 fun (x : ℝ) ↦ max x 0

Tactic:
LipschitzWith.id.max_const _

Premises used: LipschitzWith.max_const, LipschitzWith.id
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : α → ℝ
hf : MemLp f p μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ max (f x) 0) p μ

Tactic:
lipschitzWith_pos_part.comp_memLp (max_eq_right le_rfl) hf

Premises used: le_rfl, LipschitzWith.comp_memLp, MeasureTheory.Lp.lipschitzWith_pos_part, max_eq_right
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : α → ℝ
hf : MemLp f p μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ max (-f x) 0) p μ

Tactic:
lipschitzWith_pos_part.comp_memLp (max_eq_right le_rfl) hf.neg

Premises used: le_rfl, LipschitzWith.comp_memLp, MeasureTheory.Lp.lipschitzWith_pos_part, max_eq_right, MeasureTheory.MemLp.neg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
⊢ (↑(posPart f) : α →ₘ[μ] ℝ) = (↑f : α →ₘ[μ] ℝ).posPart

Tactic:
rfl

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.posPart, rfl, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
⊢ (↑(↑(posPart f) : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae μ] fun (a : α) ↦ max ((↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0

Tactic:
AEEqFun.coeFn_posPart _

Premises used: Quotient.liftOn', MeasureTheory.AEEqFun.posPart, MeasureTheory.AEEqFun.coeFn_posPart, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
h :
  ∀ (a : α) (h₁ : (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a) 0)
    (h₂ : (↑(↑(-f) : α →ₘ[μ] ℝ) : α → ℝ) a = (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ)) a),
    (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
⊢ ∀ᵐ (a : α) ∂μ, (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0

Tactic:
filter_upwards [coeFn_posPart (-f), coeFn_neg f] with _ h₁ h₂

Premises used: MeasureTheory.Lp.coeFn_neg, MeasureTheory.Lp.coeFn_posPart, Neg.neg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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
h₄ h₅ : max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
⊢ (↑(↑(posPart (-f)) : α →ₘ[μ] ℝ) : α → ℝ) a = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0

Tactic:
rw [h₁, h₂, Pi.neg_apply]

Premises used: Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
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)
rw₂ rw₃ : max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0 = max (-(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0
⊢ (↑(↑(negPart f) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) a) 0

Tactic:
rw [h, ← max_neg_neg, neg_zero]

Premises used: max_neg_neg, neg_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : Fact (1 ≤ p)
⊢ Continuous (Y := ↥(Lp ℝ p μ)) fun (f : ↥(Lp ℝ p μ)) ↦ posPart f

Tactic:
LipschitzWith.continuous_compLp _ _

Premises used: MeasureTheory.Lp.posPart, LipschitzWith.continuous_compLp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : Fact (1 ≤ p)
⊢ Continuous (Y := ↥(Lp ℝ p μ)) fun (f : ↥(Lp ℝ p μ)) ↦ posPart (-f)

Tactic:
continuous_posPart.comp continuous_neg

Premises used: ContinuousNeg.continuous_neg, Continuous.comp, MeasureTheory.Lp.posPart, LipschitzWith.compLp, MeasureTheory.Lp.continuous_posPart
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : Fact (1 ≤ p)
⊢ Continuous (Y := ↥(Lp ℝ p μ)) fun (f : ↥(Lp ℝ p μ)) ↦ posPart (-f)

Tactic:
exact continuous_posPart.comp continuous_neg

Premises used: ContinuousNeg.continuous_neg, Continuous.comp, MeasureTheory.Lp.continuous_posPart
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ₑ ^ p.toReal} : ℝ≥0∞) ^
      (1 / p.toReal) ≤
    ENNReal.ofReal ‖f‖

Tactic:
(ENNReal.ofReal_toReal (eLpNorm_ne_top f)).symm ▸
    pow_mul_meas_ge_le_eLpNorm μ hp_ne_zero hp_ne_top (Lp.aestronglyMeasurable f) ε

Premises used: MeasureTheory.Lp.aestronglyMeasurable, Eq.rec, ENNReal.ofReal_toReal, MeasureTheory.pow_mul_meas_ge_le_eLpNorm, Eq.symm, MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ₑ ^ p.toReal} : ℝ≥0∞) ≤
    ENNReal.ofReal ‖f‖ ^ p.toReal

Tactic:
(ENNReal.ofReal_toReal (eLpNorm_ne_top f)).symm ▸
    mul_meas_ge_le_pow_eLpNorm μ hp_ne_zero hp_ne_top (Lp.aestronglyMeasurable f) ε

Premises used: MeasureTheory.Lp.aestronglyMeasurable, Eq.rec, ENNReal.ofReal_toReal, Eq.symm, MeasureTheory.mul_meas_ge_le_pow_eLpNorm, MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal)
      ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ : ℝ≥0∞)} : ℝ≥0∞) ≤
    ENNReal.ofReal ‖f‖ ^ p.toReal

Tactic:
(ENNReal.ofReal_toReal (eLpNorm_ne_top f)).symm ▸
    mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top (Lp.aestronglyMeasurable f) ε

Premises used: MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.mul_meas_ge_le_pow_eLpNorm', Eq.rec, ENNReal.ofReal_toReal, Eq.symm, MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p_1 : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
R : Type u_6
inst_2 : NormedAddCommGroup R
inst_3 : StarAddMonoid R
inst_4 : NormedStarGroup R
p : ℝ≥0∞
f : ↥(Lp R p μ)
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] R)) (Lp R p μ) (star (↑f : α →ₘ[μ] R))

Tactic:
simpa [Lp.mem_Lp_iff_eLpNorm_lt_top] using Lp.eLpNorm_lt_top f

Premises used: MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top, MeasureTheory.Lp.eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_6
inst : NormedAddCommGroup R
inst_1 : StarAddMonoid R
inst_2 : NormedStarGroup R
p : ℝ≥0∞
f : ↥(Lp R p μ)
⊢ (↑(↑(star f) : α →ₘ[μ] R) : α → R) =ᶠ[ae μ] star (↑(↑f : α →ₘ[μ] R) : α → R)

Tactic:
(f : α →ₘ[μ] R).coeFn_star

Premises used: MeasureTheory.AEEqFun.coeFn_star, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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)
rw₁ rw₂ :
  (∫⁻ (a : α), liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop ∂μ) ^ (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)

Tactic:
rw [eLpNorm'_eq_lintegral_enorm, h_no_pow]

Premises used: MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
suffices : ∫⁻ (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)

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]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 ∂μ

Tactic:
lintegral_congr_ae (h_lim.mono fun a ha => ?_)

Premises used: MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
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)
⊢ ∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ = ∫⁻ (a : α), liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop ∂μ

Tactic:
refine lintegral_congr_ae (h_lim.mono fun a ha => ?_)

Premises used: MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
rw : Tendsto (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop (𝓝 (‖f_lim a‖ₑ ^ p))
⊢ ‖f_lim a‖ₑ ^ p = liminf (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop

Tactic:
rw [Tendsto.liminf_eq]

Premises used: Filter.Tendsto.liminf_eq
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))

Tactic:
(ENNReal.continuous_rpow_const.tendsto ‖f_lim a‖₊).comp ?_

Premises used: ENNReal.ofNNReal, NNNorm.nnnorm, Continuous.tendsto, Filter.Tendsto.comp, ENNReal.continuous_rpow_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
refine : Tendsto (fun (m : ι) ↦ ‖f m a‖ₑ) atTop (𝓝 (↑‖f_lim a‖₊ : ℝ≥0∞))
⊢ Tendsto (fun (m : ι) ↦ ‖f m a‖ₑ ^ p) atTop (𝓝 (‖f_lim a‖ₑ ^ p))

Tactic:
refine (ENNReal.continuous_rpow_const.tendsto ‖f_lim a‖₊).comp ?_

Premises used: ENNReal.ofNNReal, NNNorm.nnnorm, Continuous.tendsto, Filter.Tendsto.comp, ENNReal.continuous_rpow_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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‖ₑ) atTop (𝓝 (↑‖f_lim a‖₊ : ℝ≥0∞))

Tactic:
(continuous_enorm.tendsto (f_lim a)).comp ha

Premises used: continuous_enorm, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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‖ₑ) atTop (𝓝 (↑‖f_lim a‖₊ : ℝ≥0∞))

Tactic:
exact (continuous_enorm.tendsto (f_lim a)).comp ha

Premises used: continuous_enorm, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
rw :
  (∫⁻ (a : α), liminf (fun (x : ℕ) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p) ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop
⊢ eLpNorm' f_lim p μ ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop

Tactic:
rw [eLpNorm'_lim_eq_lintegral_liminf h_lim]

Premises used: MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
⊢ 0 < p⁻¹

Tactic:
simp [hp_pos]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
rw :
  ∫⁻ (a : α), liminf (fun (x : ℕ) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p
⊢ (∫⁻ (a : α), liminf (fun (x : ℕ) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p) ≤ liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop

Tactic:
rw [one_div, ← ENNReal.le_rpow_inv_iff (by simp [hp_pos] : 0 < p⁻¹), inv_inv]

Premises used: ENNReal.le_rpow_inv_iff, inv_inv, one_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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 ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p

Tactic:
(lintegral_liminf_le' fun m => (hf m).enorm.pow_const _).trans_eq ?_

Premises used: AEMeasurable.pow_const, LE.le.trans_eq, MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.lintegral_liminf_le'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
refine :
  liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p
⊢ ∫⁻ (a : α), liminf (fun (x : ℕ) ↦ ‖f x a‖ₑ ^ p) atTop ∂μ ≤
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p

Tactic:
refine (lintegral_liminf_le' fun m => (hf m).enorm.pow_const _).trans_eq ?_

Premises used: AEMeasurable.pow_const, LE.le.trans_eq, MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.lintegral_liminf_le'
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
⊢ StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p

Tactic:
have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hp_pos
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
⊢ Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p

Tactic:
have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop

Tactic:
(h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_

Premises used: ENNReal.rpow, OrderIso.liminf_apply, StrictMono.orderIsoOfSurjective
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ
refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ
refine_3 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (eLpNorm' (f x) p μ)
refine_4 :
  IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (eLpNorm' (f x) p μ)
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop

Tactic:
refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_

Premises used: OrderIso.liminf_apply, StrictMono.orderIsoOfSurjective
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ eLpNorm' (f n) p μ

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (eLpNorm' (f x) p μ)

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
h_rpow_mono : StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x ^ p
h_rpow_surj : Function.Surjective (β := ℝ≥0∞) fun (y : ℝ≥0∞) ↦ y ^ p
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦
    (StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ x ^ p) h_rpow_mono h_rpow_surj : (a : ℝ≥0∞) → ℝ≥0∞)
      (eLpNorm' (f x) p μ)

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Complete
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))
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ) atTop) p =
    liminf (fun (n : ℕ) ↦ eLpNorm' (f n) p μ ^ p) atTop

Tactic:
have h_pow_liminf :
    atTop.liminf (fun n ↦ eLpNorm' (f n) p μ) ^ p
      = atTop.liminf fun n ↦ eLpNorm' (f n) p μ ^ p := by
    have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hp_pos
    have h_rpow_surj := (ENNReal.rpow_left_bijective hp_pos.ne.symm).2
    refine (h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj).liminf_apply ?_ ?_ ?_ ?_
    all_goals isBoundedDefault