awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedDivisionRing 𝕜
f : α → 𝕜
h : Integrable f μ
c : 𝕜
simp_rw : Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ f x * c⁻¹) μ
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ f x / c) μ

Tactic:
simp_rw [div_eq_mul_inv, h.mul_const]

Premises used: div_eq_mul_inv, MeasureTheory.Integrable.mul_const
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → ℝ
hf : Integrable f μ
rw : ∀ (hf : MemLp f 1 μ), MemLp.{u_1, u_8} (ε := 𝕜) (fun (x : α) ↦ (↑(f x) : 𝕜)) 1 μ
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ (↑(f x) : 𝕜)) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → ℝ
hf : MemLp f 1 μ
⊢ MemLp.{u_1, u_8} (ε := 𝕜) (fun (x : α) ↦ (↑(f x) : 𝕜)) 1 μ

Tactic:
hf.ofReal

Premises used: MeasureTheory.MemLp.ofReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → ℝ
hf : MemLp f 1 μ
⊢ MemLp.{u_1, u_8} (ε := 𝕜) (fun (x : α) ↦ (↑(f x) : 𝕜)) 1 μ

Tactic:
exact hf.ofReal

Premises used: MeasureTheory.MemLp.ofReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
simp_rw :
  MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) 1 μ ∧
      MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) 1 μ ↔
    MemLp f 1 μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ ∧
      Integrable (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ ↔
    Integrable f μ

Tactic:
simp_rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) 1 μ ∧
      MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) 1 μ ↔
    MemLp f 1 μ

Tactic:
memLp_re_im_iff

Premises used: MeasureTheory.memLp_re_im_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) 1 μ ∧
      MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) 1 μ ↔
    MemLp f 1 μ

Tactic:
exact memLp_re_im_iff

Premises used: MeasureTheory.memLp_re_im_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
hf : Integrable f μ
rw : ∀ (hf : MemLp f 1 μ), MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) 1 μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f 1 μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) 1 μ

Tactic:
hf.re

Premises used: MeasureTheory.MemLp.re
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f 1 μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) 1 μ

Tactic:
exact hf.re

Premises used: MeasureTheory.MemLp.re
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
hf : Integrable f μ
rw : ∀ (hf : MemLp f 1 μ), MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) 1 μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f 1 μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) 1 μ

Tactic:
hf.im

Premises used: MeasureTheory.MemLp.im
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f 1 μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) 1 μ

Tactic:
exact hf.im

Premises used: MeasureTheory.MemLp.im
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ Integrable f (μ'.trim hm)

Tactic:
⟨hf.aestronglyMeasurable, ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable, And.intro
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
refine : HasFiniteIntegral f (μ'.trim hm)
⊢ Integrable f (μ'.trim hm)

Tactic:
refine ⟨hf.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
rw : ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ∞
rw₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ‖f a‖ₑ
⊢ HasFiniteIntegral f (μ'.trim hm)

Tactic:
rw [HasFiniteIntegral, lintegral_trim hm _]

Premises used: MeasureTheory.lintegral_trim, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ∞

Tactic:
hf_int.2

Premises used: And.right, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ∞

Tactic:
exact hf_int.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ‖f a‖ₑ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f (μ'.trim hm)
⊢ AEStronglyMeasurable f (μ'.trim hm)

Tactic:
obtain ⟨hf_meas_ae, hf⟩ := hf_int
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f (μ'.trim hm)
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
⊢ HasFiniteIntegral f (μ'.trim hm)

Tactic:
obtain ⟨hf_meas_ae, hf⟩ := hf_int
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
hf : HasFiniteIntegral f (μ'.trim hm)
⊢ Integrable f μ'

Tactic:
⟨aestronglyMeasurable_of_aestronglyMeasurable_trim hm hf_meas_ae, ?_⟩

Premises used: MeasureTheory.Integrable, And.intro, aestronglyMeasurable_of_aestronglyMeasurable_trim
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
hf : HasFiniteIntegral f (μ'.trim hm)
refine : HasFiniteIntegral f μ'
⊢ Integrable f μ'

Tactic:
refine ⟨aestronglyMeasurable_of_aestronglyMeasurable_trim hm hf_meas_ae, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
hf : HasFiniteIntegral f (μ'.trim hm)
⊢ HasFiniteIntegral f μ'

Tactic:
simpa [HasFiniteIntegral, lintegral_trim_ae hm hf_meas_ae.enorm] using hf

Premises used: MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.HasFiniteIntegral, MeasureTheory.lintegral_trim_ae
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m m0 : MeasurableSpace α
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
hC : C < ∞
f : α → ε
hf_meas : AEStronglyMeasurable f μ
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C
⊢ Integrable f μ

Tactic:
⟨hf_meas, (lintegral_le_of_forall_fin_meas_trim_le hm C hf).trans_lt hC⟩

Premises used: MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le, MeasureTheory.Integrable, And.intro, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : SigmaFinite μ
C : ℝ≥0∞
hC : C < ∞
f : α → ε
hf_meas : AEStronglyMeasurable f μ
hf :
  ∀ (s : Set α),
    MeasurableSet s → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C
rwa rwa₁ rwa₂ rwa₃ : SigmaFinite μ
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
rwa [@trim_eq_self _ m]

Premises used: MeasureTheory.trim_eq_self
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
s : Set α
⊢ Integrable f (μ.restrict s)

Tactic:
hf.mono_measure Measure.restrict_le_self

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
H : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup H
𝕜 : Type u_10
𝕜' : Type u_11
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜' E
inst_5 : NormedSpace 𝕜 H
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
φ : α → H
L : H →SL[σ] E
φ_int : Integrable φ μ
⊢ AEStronglyMeasurable.{u_1, u_8} (β := E) (fun (a : α) ↦ (L : (a : H) → E) (φ a)) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
H : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup H
𝕜 : Type u_10
𝕜' : Type u_11
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜' E
inst_5 : NormedSpace 𝕜 H
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomIsometric σ
inst_7 : RingHomIsometric σ'
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
φ : α → H
L : H ≃SL[σ] E
h : Integrable.{u_8, u_1} (ε := E) (fun (a : α) ↦ (L : (a : H) → E) (φ a)) μ
⊢ Integrable φ μ

Tactic:
simpa using ContinuousLinearMap.integrable_comp (L.symm : E →SL[σ'] H) h

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearMap.integrable_comp, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
H : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup H
𝕜 : Type u_10
𝕜' : Type u_11
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜' E
inst_5 : NormedSpace 𝕜 H
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomIsometric σ
inst_7 : RingHomIsometric σ'
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
φ : α → H
L : H ≃ₛₗᵢ[σ] E
⊢ Integrable.{u_8, u_1} (ε := E) (fun (a : α) ↦ (L : (a : H) → E) (φ a)) μ ↔ Integrable φ μ

Tactic:
ContinuousLinearEquiv.integrable_comp_iff (L : H ≃SL[σ] E)

Premises used: ContinuousLinearEquiv.integrable_comp_iff, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
H : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup H
𝕜 : Type u_10
𝕜' : Type u_11
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜' E
inst_5 : NormedSpace 𝕜 H
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
φ : α → H →SL[σ] E
φ_int : Integrable φ μ
v : H
⊢ Integrable.{u_8, u_1} (ε := E) (fun (a : α) ↦ (φ a : (a : H) → E) v) μ

Tactic:
(ContinuousLinearMap.apply' E σ v).integrable_comp φ_int

Premises used: ContinuousLinearMap.integrable_comp, DFunLike.coe, ContinuousLinearMap.apply'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
F : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : α → E × F
hf : Integrable f μ
⊢ Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).1) μ

Tactic:
(ContinuousLinearMap.fst ℝ E F).integrable_comp hf

Premises used: Real, ContinuousLinearMap.integrable_comp, ContinuousLinearMap.fst
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
F : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : α → E × F
hf : Integrable f μ
⊢ Integrable.{u_9, u_1} (ε := F) (fun (x : α) ↦ (f x).2) μ

Tactic:
(ContinuousLinearMap.snd ℝ E F).integrable_comp hf

Premises used: Real, ContinuousLinearMap.snd, ContinuousLinearMap.integrable_comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
F : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : α → E × F
⊢ Integrable f μ ↔
    Integrable.{u_8, u_1} (ε := E) (fun (x : α) ↦ (f x).1) μ ∧ Integrable.{u_9, u_1} (ε := F) (fun (x : α) ↦ (f x).2) μ

Tactic:
⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩

Premises used: MeasureTheory.Integrable.fst, MeasureTheory.Integrable.snd, And.right, And.left, And.intro, Iff.intro, MeasureTheory.Integrable.prodMk
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
G : ℕ → ℝ → ℝ
f : ℝ → ℝ
μ : Measure ℝ
hGf : ∀ᵐ (x : ℝ) ∂μ, Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))
hG : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖G n x‖ₑ) μ
x : ℝ
hx : Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))
⊢ liminf (fun (x_1 : ℕ) ↦ ‖G x_1 x‖ₑ) atTop = ‖f x‖ₑ

Tactic:
hx.enorm.liminf_eq

Premises used: Filter.Tendsto.enorm, Filter.Tendsto.liminf_eq
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
G : ℕ → ℝ → ℝ
f : ℝ → ℝ
μ : Measure ℝ
hGf : ∀ᵐ (x : ℝ) ∂μ, Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))
hG : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖G n x‖ₑ) μ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ liminf (fun (x_1 : ℕ) ↦ ‖G x_1 x‖ₑ) atTop = ‖f x‖ₑ) x} x}
      a
h₁ h₂ :
  ∀ (x : ℝ) (hx : Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))), liminf (fun (x_1 : ℕ) ↦ ‖G x_1 x‖ₑ) atTop = ‖f x‖ₑ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ liminf (fun (x_1 : ℕ) ↦ ‖G x_1 x‖ₑ) atTop) fun (x : ℝ) ↦ ‖f x‖ₑ

Tactic:
filter_upwards [hGf] with x hx using hx.enorm.liminf_eq
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
G : ℕ → ℝ → ℝ
f : ℝ → ℝ
μ : Measure ℝ
hGf : ∀ᵐ (x : ℝ) ∂μ, Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) μ
hG' : Ne (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ), ‖G n x‖ₑ ∂μ) atTop) ∞
⊢ Integrable f μ

Tactic:
⟨aestronglyMeasurable_of_tendsto_ae _ hG hGf,
   lt_of_le_of_lt (lintegral_enorm_le_liminf_of_tendsto hGf
    (fun n ↦ (hG n).aemeasurable.enorm)) hG'.lt_top⟩

Premises used: lt_of_le_of_lt, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.enorm, MeasureTheory.Integrable, aestronglyMeasurable_of_tendsto_ae, Ne.lt_top, And.intro, MeasureTheory.lintegral_enorm_le_liminf_of_tendsto
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : MemLp f 2 μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 2) μ

Tactic:
simpa [← memLp_one_iff_integrable] using h.norm_rpow two_ne_zero ENNReal.ofNat_ne_top

Premises used: ENNReal.ofNat_ne_top, MeasureTheory.MemLp.norm_rpow, two_ne_zero, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
rw : MemLp f 2 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) 1 μ
⊢ MemLp f 2 μ ↔ Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) μ

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ ENNReal.toReal 2) (2 / 2) μ

Tactic:
(memLp_norm_rpow_iff hf two_ne_zero ENNReal.ofNat_ne_top).symm

Premises used: ENNReal.ofNat_ne_top, two_ne_zero, MeasureTheory.memLp_norm_rpow_iff, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
h : ∀ (x : α), HPow.hPow (β := ℕ) ‖f x‖ 2 = ‖f x‖ ^ ENNReal.toReal 2
h₁ : 1 = 2 / 2
⊢ MemLp f 2 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) 1 μ

Tactic:
convert! (memLp_norm_rpow_iff hf two_ne_zero ENNReal.ofNat_ne_top).symm

Premises used: ENNReal.ofNat_ne_top, two_ne_zero, MeasureTheory.memLp_norm_rpow_iff, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
x : α
⊢ HPow.hPow (β := ℕ) ‖f x‖ 2 = ‖f x‖ ^ ENNReal.toReal 2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
h : 1 = HMul.hMul (α := ℝ≥0∞) 2 2⁻¹
h₁ h₂ : Eq (α := ℝ≥0∞) 1 1
⊢ 1 = 2 / 2

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel two_ne_zero ENNReal.ofNat_ne_top]

Premises used: ENNReal.ofNat_ne_top, div_eq_mul_inv, two_ne_zero, ENNReal.mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) μ

Tactic:
memLp_two_iff_integrable_sq_norm hf

Premises used: MeasureTheory.memLp_two_iff_integrable_sq_norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
h : ∀ (x : α), HPow.hPow (β := ℕ) (f x) 2 = HPow.hPow (β := ℕ) ‖f x‖ 2
⊢ MemLp f 2 μ ↔ Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 2) μ

Tactic:
convert! memLp_two_iff_integrable_sq_norm hf using 3

Premises used: MeasureTheory.memLp_two_iff_integrable_sq_norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
x : α
⊢ HPow.hPow (β := ℕ) (f x) 2 = HPow.hPow (β := ℕ) ‖f x‖ 2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
c : E
f : α → E
hf : MemLp f p μ
⊢ MemLp.{u_1, u_3} (ε := 𝕜) (fun (a : α) ↦ ⟪c, f a⟫) p μ

Tactic:
hf.of_le_mul (AEStronglyMeasurable.inner aestronglyMeasurable_const hf.1)
    (Eventually.of_forall fun _ => norm_inner_le_norm _ _)

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.MemLp.of_le_mul, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.inner, And.left, norm_inner_le_norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f p μ
c : E
x : α
rw : ‖⟪f x, c⟫‖ ≤ ‖f x‖ * ‖c‖
⊢ ‖⟪f x, c⟫‖ ≤ ‖c‖ * ‖f x‖

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f p μ
c : E
x : α
⊢ ‖⟪f x, c⟫‖ ≤ ‖f x‖ * ‖c‖

Tactic:
norm_inner_le_norm _ _

Premises used: norm_inner_le_norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f p μ
c : E
x : α
⊢ ‖⟪f x, c⟫‖ ≤ ‖f x‖ * ‖c‖

Tactic:
exact norm_inner_le_norm _ _

Premises used: norm_inner_le_norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : Integrable f μ
rw : ∀ (hf : MemLp f 1 μ), MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ ⟪c, f x⟫) 1 μ
⊢ Integrable.{u_3, u_1} (ε := 𝕜) (fun (x : α) ↦ ⟪c, f x⟫) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : MemLp f 1 μ
⊢ MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ ⟪c, f x⟫) 1 μ

Tactic:
hf.const_inner c

Premises used: MeasureTheory.MemLp.const_inner
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : MemLp f 1 μ
⊢ MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ ⟪c, f x⟫) 1 μ

Tactic:
exact hf.const_inner c

Premises used: MeasureTheory.MemLp.const_inner
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
hf : Integrable f μ
c : E
rw : ∀ (hf : MemLp f 1 μ) (c : E), MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ ⟪f x, c⟫) 1 μ
⊢ Integrable.{u_3, u_1} (ε := 𝕜) (fun (x : α) ↦ ⟪f x, c⟫) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable