awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
h :
  ∀ (x : α)
    (hx :
      (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
                α →ₘ[μ] E) :
            α → E)
          x =
        f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x),
    ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
                α →ₘ[μ] E) :
            α → E)
          x‖ₑ =
      HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
        (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) x
⊢ (fun (a : α) ↦
      ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                    ⋯) :
                α →ₘ[μ] E) :
            α → E)
          a‖ₑ) =ᶠ[ae μ]
    HMul.hMul (α := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) fun (a : α) ↦
      ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ

Tactic:
filter_upwards [(memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp] with x hx

Premises used: MeasureTheory.memL1_smul_of_L1_withDensity, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
hx :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
h :
  ‖f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x‖ₑ =
    HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
      (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) x
⊢ ‖(↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
              α →ₘ[μ] E) :
          α → E)
        x‖ₑ =
    HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
      (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) x

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
x : α
hx :
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
            α →ₘ[μ] E) :
        α → E)
      x =
    f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x
⊢ ‖f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x‖ₑ =
    HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
      (fun (a : α) ↦ ‖(↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a‖ₑ) x

Tactic:
simp [NNReal.smul_def, enorm_smul]

Premises used: enorm_smul, NNReal.smul_def
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
⊢ (withDensitySMulLI μ f_meas : (a : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))) → ↥(Lp E 1 μ)) u =
    MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯

Tactic:
rfl

Premises used: MeasureTheory.MemLp.toLp, rfl
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
rw : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), ‖(f x).toReal‖ₑ ∂μ < ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (f x).toReal) 1 μ

Tactic:
rw [MemLp, eLpNorm_one_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm, MeasureTheory.MemLp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), ‖(f x).toReal‖ₑ ∂μ < ∞

Tactic:
⟨(AEMeasurable.ennreal_toReal hfm).aestronglyMeasurable,
    hasFiniteIntegral_toReal_of_lintegral_ne_top hfi⟩

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top, And.intro, AEMeasurable.ennreal_toReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), ‖(f x).toReal‖ₑ ∂μ < ∞

Tactic:
exact ⟨(AEMeasurable.ennreal_toReal hfm).aestronglyMeasurable,
    hasFiniteIntegral_toReal_of_lintegral_ne_top hfi⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ

Tactic:
memLp_one_iff_integrable.1 <| mem_L1_toReal_of_lintegral_ne_top hfm hfi

Premises used: MeasureTheory.mem_L1_toReal_of_lintegral_ne_top, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
rw : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), f x ∂μ ≠ ∞ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞

Tactic:
rw [Integrable, hasFiniteIntegral_toReal_iff hf_ne_top]

Premises used: MeasureTheory.Integrable, MeasureTheory.hasFiniteIntegral_toReal_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), f x ∂μ ≠ ∞ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞

Tactic:
simp only [hf.ennreal_toReal.aestronglyMeasurable, ne_eq, true_and]

Premises used: AEMeasurable.aestronglyMeasurable, ne_eq, AEMeasurable.ennreal_toReal, true_and
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfm : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
rw : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ∞ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ∞ ↔ Integrable f μ

Tactic:
rw [Integrable, hasFiniteIntegral_iff_ofReal hf]

Premises used: MeasureTheory.Integrable, MeasureTheory.hasFiniteIntegral_iff_ofReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfm : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ∞ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞

Tactic:
simp [hfm]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
left : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ max (f a) 0) μ
right : HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ max (f a) 0) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ max (f a) 0) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ max (f a) 0) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ max (f a) 0) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ max (-f a) 0) μ

Tactic:
hf.neg.pos_part

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.Integrable.pos_part
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : Integrable f μ
left : AEStronglyMeasurable (c • f) μ
right : HasFiniteIntegral (c • f) μ
⊢ Integrable (c • f) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : Integrable f μ
⊢ AEStronglyMeasurable (c • f) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : Integrable f μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : NormedAddCommGroup 𝕜
inst_3 : SMul 𝕜 ε
inst_4 : ContinuousConstSMul 𝕜 ε
inst_5 : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
hf : Integrable f μ
left : AEStronglyMeasurable (c • f) μ
right : HasFiniteIntegral (c • f) μ
⊢ Integrable (c • f) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : NormedAddCommGroup 𝕜
inst_3 : SMul 𝕜 ε
inst_4 : ContinuousConstSMul 𝕜 ε
inst_5 : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
hf : Integrable f μ
⊢ AEStronglyMeasurable (c • f) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
ε : Type u_9
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : NormedAddCommGroup 𝕜
inst_3 : SMul 𝕜 ε
inst_4 : ContinuousConstSMul 𝕜 ε
inst_5 : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
hf : Integrable f μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
hc : IsUnit c
f : α → β
⊢ Integrable (c • f) μ ↔ Integrable f μ

Tactic:
and_congr hc.aestronglyMeasurable_const_smul_iff (hasFiniteIntegral_smul_iff hc f)

Premises used: MeasureTheory.Integrable, IsUnit.aestronglyMeasurable_const_smul_iff, MeasureTheory.hasFiniteIntegral_smul_iff, and_congr
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedDivisionRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
hc : c ≠ 0
f : α → β
⊢ Integrable (c • f) μ ↔ Integrable f μ

Tactic:
(IsUnit.mk0 _ hc).integrable_smul_iff f

Premises used: IsUnit.mk0, IsUnit.integrable_smul_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedDivisionRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
hc : c ≠ 0
f : α → β
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ c • f x) μ ↔ Integrable f μ

Tactic:
integrable_smul_iff hc f

Premises used: MeasureTheory.integrable_smul_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Integrable f μ
hφ : MemLp φ ∞ μ
rw : ∀ (hf : MemLp f 1 μ) (hφ : MemLp φ ∞ μ), MemLp (φ • f) 1 μ
⊢ Integrable (φ • f) μ

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
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : MemLp f 1 μ
hφ : MemLp φ ∞ μ
⊢ MemLp (φ • f) 1 μ

Tactic:
MemLp.smul hf hφ

Premises used: MeasureTheory.MemLp.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : MemLp f 1 μ
hφ : MemLp φ ∞ μ
⊢ MemLp (φ • f) 1 μ

Tactic:
exact MemLp.smul hf hφ

Premises used: MeasureTheory.MemLp.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Integrable f μ
C : ℝ
hφ1 : AEStronglyMeasurable φ μ
hφ2 : ∀ᵐ (a : α) ∂μ, ‖φ a‖ ≤ C
⊢ Integrable (φ • f) μ

Tactic:
hf.smul_of_top_right (memLp_top_of_bound hφ1 C hφ2)

Premises used: MeasureTheory.memLp_top_of_bound, MeasureTheory.Integrable.smul_of_top_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : Integrable φ μ
hf : MemLp f ∞ μ
rw : ∀ (hφ : MemLp φ 1 μ) (hf : MemLp f ∞ μ), MemLp (φ • f) 1 μ
⊢ Integrable (φ • f) μ

Tactic:
rw [← memLp_one_iff_integrable] at hφ ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : MemLp φ 1 μ
hf : MemLp f ∞ μ
⊢ MemLp (φ • f) 1 μ

Tactic:
MemLp.smul hf hφ

Premises used: MeasureTheory.MemLp.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : MemLp φ 1 μ
hf : MemLp f ∞ μ
⊢ MemLp (φ • f) 1 μ

Tactic:
exact MemLp.smul hf hφ

Premises used: MeasureTheory.MemLp.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hφ : Integrable φ μ
C : ℝ
hf1 : AEStronglyMeasurable f μ
hf2 : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C
⊢ Integrable (φ • f) μ

Tactic:
hφ.smul_of_top_left (memLp_top_of_bound hf1 C hf2)

Premises used: MeasureTheory.memLp_top_of_bound, MeasureTheory.Integrable.smul_of_top_left
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_8
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → 𝕜
hf : Integrable f μ
c : β
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ f x • c) μ

Tactic:
hf.smul_of_top_left (memLp_top_const c)

Premises used: MeasureTheory.Integrable.smul_of_top_left, MeasureTheory.memLp_top_const
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_9
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
simp_rw : AEStronglyMeasurable f μ → (∫⁻ (a : α), ‖f a‖ₑ * ‖c‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞)
⊢ Integrable.{u_9, u_1} (ε := E) (fun (x : α) ↦ f x • c) μ ↔ Integrable f μ

Tactic:
simp_rw [Integrable, aestronglyMeasurable_smul_const_iff (f := f) hc, and_congr_right_iff,
    hasFiniteIntegral_iff_enorm, enorm_smul]

Premises used: enorm_smul, MeasureTheory.Integrable, aestronglyMeasurable_smul_const_iff, and_congr_right_iff, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_9
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
h : AEStronglyMeasurable f μ
rw : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ∧ ‖c‖ₑ < ∞ ∨ ∫⁻ (a : α), ‖f a‖ₑ ∂μ = 0 ∨ ‖c‖ₑ = 0 ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ * ‖c‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
rw [lintegral_mul_const' _ _ enorm_ne_top, ENNReal.mul_lt_top_iff]

Premises used: ENNReal.mul_lt_top_iff, MeasureTheory.lintegral_mul_const', enorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_9
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
h : AEStronglyMeasurable f μ
⊢ ∀ (x : ℝ≥0∞), x = 0 → x < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_9
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
h : AEStronglyMeasurable f μ
⊢ ∀ (x : ℝ≥0∞), x = 0 → x < ∞

Tactic:
have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_9
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
h : AEStronglyMeasurable f μ
this : ∀ (x : ℝ≥0∞), x = 0 → x < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ∧ ‖c‖ₑ < ∞ ∨ ∫⁻ (a : α), ‖f a‖ₑ ∂μ = 0 ∨ ‖c‖ₑ = 0 ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
simp [hc, or_iff_left_of_imp (this _)]

Premises used: or_iff_left_of_imp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
f : α → 𝕜
h : Integrable f μ
c : 𝕜
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ c * f x) μ

Tactic:
h.smul c

Premises used: MeasureTheory.Integrable.smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
f : α → 𝕜
h : Integrable f μ
c : 𝕜
⊢ Integrable ((fun (x : α) ↦ c) * f) μ

Tactic:
Integrable.const_mul h c

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
f : α → 𝕜
h : Integrable f μ
c : 𝕜
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ f x * c) μ

Tactic:
h.smul (MulOpposite.op c)

Premises used: MeasureTheory.Integrable.smul, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
f : α → 𝕜
h : Integrable f μ
c : 𝕜
⊢ Integrable (f * fun (x : α) ↦ c) μ

Tactic:
Integrable.mul_const h c

Premises used: MeasureTheory.Integrable.mul_const
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
c : 𝕜
hc : IsUnit c
f : α → 𝕜
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ c * f x) μ ↔ Integrable f μ

Tactic:
hc.integrable_smul_iff f

Premises used: IsUnit.integrable_smul_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
c : 𝕜
hc : IsUnit c
f : α → 𝕜
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ f x * c) μ ↔ Integrable f μ

Tactic:
hc.op.integrable_smul_iff f

Premises used: MulOpposite.unop, IsUnit.integrable_smul_iff, IsUnit.op
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
f g : α → 𝕜
c : ℝ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ f x * g x) μ

Tactic:
hg.bdd_smul c hf hf_bound

Premises used: MeasureTheory.Integrable.bdd_smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
f g : α → 𝕜
c : ℝ
hf : Integrable f μ
hg : AEStronglyMeasurable g μ
hg_bound : ∀ᵐ (x : α) ∂μ, ‖g x‖ ≤ c
⊢ Integrable.{u_8, u_1} (ε := 𝕜) (fun (x : α) ↦ f x * g x) μ

Tactic:
hf.smul_bdd c hg hg_bound

Premises used: MeasureTheory.Integrable.smul_bdd
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
f φ : α → 𝕜
hf : Integrable f μ
hφ : MemLp φ ∞ μ
⊢ Integrable (φ * f) μ

Tactic:
hf.smul_of_top_right hφ

Premises used: MeasureTheory.Integrable.smul_of_top_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
f φ : α → 𝕜
hφ : Integrable φ μ
hf : MemLp f ∞ μ
⊢ Integrable (φ * f) μ

Tactic:
hφ.smul_of_top_left hf

Premises used: MeasureTheory.Integrable.smul_of_top_left
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst : NormedRing 𝕜
p q : ℝ≥0∞
f g : α → 𝕜
hf : MemLp f p μ
hg : MemLp g q μ
inst_1 : p.HolderTriple q 1
⊢ Integrable (f * g) μ

Tactic:
memLp_one_iff_integrable.1 <| hg.mul hf

Premises used: MeasureTheory.MemLp.mul, Iff.mp, MeasureTheory.memLp_one_iff_integrable