awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
α' : Type u_8
inst_2 : MeasurableSpace α'
f : α → α'
g : α' → ε
hg : @Integrable _ _ _ _ inst_2 g (Measure.map f μ)
hf : Measurable f
⊢ Integrable (g ∘ f) μ

Tactic:
hg.comp_aemeasurable hf.aemeasurable

Premises used: MeasureTheory.Integrable.comp_aemeasurable, Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → δ
hf : MeasurableEmbedding f
g : δ → ε
simp_rw : MemLp (m0 := inst) g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ
⊢ @Integrable _ _ _ _ inst g (Measure.map f μ) ↔ Integrable (g ∘ 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
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → δ
hf : MeasurableEmbedding f
g : δ → ε
⊢ MemLp (m0 := inst) g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ

Tactic:
hf.memLp_map_measure_iff

Premises used: MeasurableEmbedding.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → δ
hf : MeasurableEmbedding f
g : δ → ε
⊢ MemLp (m0 := inst) g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ

Tactic:
exact hf.memLp_map_measure_iff

Premises used: MeasurableEmbedding.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α ≃ᵐ δ
g : δ → ε
simp_rw : MemLp (m0 := inst) g 1 (Measure.map (⇑f : (a : α) → δ) μ) ↔ MemLp (g ∘ (⇑f : (a : α) → δ)) 1 μ
⊢ @Integrable _ _ _ _ inst g (Measure.map (⇑f : (a : α) → δ) μ) ↔ Integrable (g ∘ (⇑f : (a : α) → δ)) μ

Tactic:
simp_rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α ≃ᵐ δ
g : δ → ε
⊢ MemLp (m0 := inst) g 1 (Measure.map (⇑f : (a : α) → δ) μ) ↔ MemLp (g ∘ (⇑f : (a : α) → δ)) 1 μ

Tactic:
f.memLp_map_measure_iff

Premises used: MeasurableEquiv.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α ≃ᵐ δ
g : δ → ε
⊢ MemLp (m0 := inst) g 1 (Measure.map (⇑f : (a : α) → δ) μ) ↔ MemLp (g ∘ (⇑f : (a : α) → δ)) 1 μ

Tactic:
exact f.memLp_map_measure_iff

Premises used: MeasurableEquiv.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
ν : Measure δ
g : δ → ε
f : α → δ
hf : MeasurePreserving f μ ν
hg : AEStronglyMeasurable g ν
rw :
  ∀ (hg : AEStronglyMeasurable (m₀ := inst) g (Measure.map f μ)),
    Integrable (g ∘ f) μ ↔ @Integrable _ _ _ _ inst g (Measure.map f μ)
⊢ Integrable (g ∘ f) μ ↔ Integrable g ν

Tactic:
rw [← hf.map_eq] at hg ⊢

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
ν : Measure δ
g : δ → ε
f : α → δ
hf : MeasurePreserving f μ ν
hg : AEStronglyMeasurable (m₀ := inst) g (Measure.map f μ)
⊢ Integrable (g ∘ f) μ ↔ @Integrable _ _ _ _ inst g (Measure.map f μ)

Tactic:
(integrable_map_measure hg hf.measurable.aemeasurable).symm

Premises used: Measurable.aemeasurable, MeasureTheory.MeasurePreserving.measurable, MeasureTheory.integrable_map_measure, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
ν : Measure δ
g : δ → ε
f : α → δ
hf : MeasurePreserving f μ ν
hg : AEStronglyMeasurable (m₀ := inst) g (Measure.map f μ)
⊢ Integrable (g ∘ f) μ ↔ @Integrable _ _ _ _ inst g (Measure.map f μ)

Tactic:
exact (integrable_map_measure hg hf.measurable.aemeasurable).symm

Premises used: Measurable.aemeasurable, MeasureTheory.MeasurePreserving.measurable, MeasureTheory.integrable_map_measure, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
ν : Measure δ
g : δ → ε
f : α → δ
hf : MeasurePreserving f μ ν
hg : Integrable g ν
⊢ Integrable (g ∘ f) μ

Tactic:
hf.integrable_comp hg.aestronglyMeasurable |>.mpr hg

Premises used: Iff.mpr, MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.MeasurePreserving.integrable_comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
δ : Type u_4
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace δ
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → δ
ν : Measure δ
h₁ : MeasurePreserving f μ ν
h₂ : MeasurableEmbedding f
g : δ → ε
⊢ Integrable (g ∘ f) μ ↔ Integrable g ν

Tactic:
h₁.map_eq ▸ Iff.symm h₂.integrable_map_iff

Premises used: Eq.rec, MeasurableEmbedding.integrable_map_iff, MeasureTheory.MeasurePreserving.map_eq, Iff.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
simp_rw : HasFiniteIntegral f μ ∧ HasFiniteIntegral g μ
⊢ ∫⁻ (a : α), edist (f a) (0 a) ∂μ < ∞ ∧ ∫⁻ (a : α), edist (g a) (0 a) ∂μ < ∞

Tactic:
simp_rw [Pi.zero_apply, ← hasFiniteIntegral_iff_edist]

Premises used: MeasureTheory.hasFiniteIntegral_iff_edist, Pi.zero_apply
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ HasFiniteIntegral f μ ∧ HasFiniteIntegral g μ

Tactic:
⟨hf.hasFiniteIntegral, hg.hasFiniteIntegral⟩

Premises used: And.intro, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ HasFiniteIntegral f μ ∧ HasFiniteIntegral g μ

Tactic:
exact ⟨hf.hasFiniteIntegral, hg.hasFiniteIntegral⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
ε' : Type u_8
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
μ : Measure α
⊢ Integrable.{u_8, u_1} (ε := ε') (fun (x : α) ↦ 0) μ

Tactic:
simp [Integrable, aestronglyMeasurable_const]

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_8
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
f g : α → ε'
hf : Integrable f μ
hg : Integrable g μ
⊢ HasFiniteIntegral (f + g) μ

Tactic:
calc
    ∫⁻ a, ‖f a + g a‖ₑ ∂μ ≤ ∫⁻ a, ‖f a‖ₑ + ‖g a‖ₑ ∂μ := lintegral_mono fun _ ↦ enorm_add_le _ _
    _ = _ := lintegral_enorm_add_left hf.aestronglyMeasurable _
    _ < ∞ := add_lt_top.2 ⟨hf.hasFiniteIntegral, hg.hasFiniteIntegral⟩

Premises used: Iff.mpr, MeasureTheory.Integrable.aestronglyMeasurable, Trans.trans, MeasureTheory.lintegral_mono, And.intro, MeasureTheory.lintegral_enorm_add_left, MeasureTheory.HasFiniteIntegral, enorm_add_le, ENNReal.add_lt_top, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_8
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
inst_2 : ContinuousAdd ε'
f g : α → ε'
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f + g) μ

Tactic:
⟨hf.aestronglyMeasurable.add hg.aestronglyMeasurable, hf.add' hg⟩

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.Integrable.add', MeasureTheory.Integrable, MeasureTheory.AEStronglyMeasurable.add, And.intro
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_8
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
inst_2 : Subsingleton ε'
f : α → ε'
⊢ Integrable f μ

Tactic:
integrable_zero _ _ _ |>.congr <| .of_forall fun _ ↦ Subsingleton.elim _ _

Premises used: Filter.Eventually.of_forall, MeasureTheory.integrable_zero, MeasureTheory.Integrable.congr, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_8
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
inst_2 : ContinuousAdd ε'
ι : Type u_9
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ Integrable.{u_8, u_1} (ε := ε') (∑ i ∈ s, f i) μ

Tactic:
Finset.sum_induction f (fun g => Integrable g μ) (fun _ _ => Integrable.add)
    (integrable_zero _ _ _) hf

Premises used: MeasureTheory.Integrable, MeasureTheory.integrable_zero, MeasureTheory.Integrable.add, Finset.sum_induction
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_8
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
inst_2 : ContinuousAdd ε'
ι : Type u_9
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ Integrable.{u_8, u_1} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) μ

Tactic:
simpa only [← Finset.sum_apply] using integrable_finsetSum' s hf

Premises used: Finset.sum_apply, MeasureTheory.integrable_finsetSum'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ HasFiniteIntegral (-f) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
⊢ Integrable (-f) μ ↔ Integrable f μ

Tactic:
⟨fun h => neg_neg f ▸ h.neg, Integrable.neg⟩

Premises used: MeasureTheory.Integrable.neg, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ -f x) μ ↔ Integrable f μ

Tactic:
integrable_neg_iff

Premises used: MeasureTheory.integrable_neg_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
h : Integrable (f + g) μ
⊢ g = f + g + -f

Tactic:
simp only [add_neg_cancel_comm]

Premises used: add_neg_cancel_comm
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ f x + g x) μ ↔ Integrable g μ

Tactic:
integrable_add_iff_integrable_right hf

Premises used: MeasureTheory.integrable_add_iff_integrable_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
rw : Integrable (f + g) μ ↔ Integrable g μ
rw₁ rw₂ : Integrable g μ ↔ Integrable g μ
⊢ Integrable (g + f) μ ↔ Integrable g μ

Tactic:
rw [add_comm, integrable_add_iff_integrable_right hf]

Premises used: add_comm, MeasureTheory.integrable_add_iff_integrable_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ g x + f x) μ ↔ Integrable g μ

Tactic:
integrable_add_iff_integrable_left hf

Premises used: MeasureTheory.integrable_add_iff_integrable_left
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
⊢ Integrable f μ

Tactic:
h_int.mono' h_meas ?_

Premises used: MeasureTheory.Integrable.mono'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
refine : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ (f + g) a
⊢ Integrable f μ

Tactic:
refine h_int.mono' h_meas ?_

Premises used: MeasureTheory.Integrable.mono'
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
h : ∀ (a : α) (haf : 0 a ≤ f a) (hag : 0 a ≤ g a), ‖f a‖ ≤ (f + g) a
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ (f + g) a

Tactic:
filter_upwards [hf, hg] with a haf hag
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
a : α
haf : 0 a ≤ f a
hag : 0 a ≤ g a
⊢ ‖f a‖ ≤ (f + g) a

Tactic:
(Real.norm_of_nonneg haf).symm ▸ le_add_of_nonneg_right hag

Premises used: Eq.rec, le_add_of_nonneg_right, Eq.symm, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
a : α
haf : 0 a ≤ f a
hag : 0 a ≤ g a
⊢ ‖f a‖ ≤ (f + g) a

Tactic:
exact (Real.norm_of_nonneg haf).symm ▸ le_add_of_nonneg_right hag
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
⊢ Integrable g μ

Tactic:
integrable_left_of_integrable_add_of_nonneg
    ((AEStronglyMeasurable.add_iff_right h_meas).mp h_int.aestronglyMeasurable)
      hg hf (add_comm f g ▸ h_int)

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Eq.rec, add_comm, Iff.mp, MeasureTheory.integrable_left_of_integrable_add_of_nonneg, MeasureTheory.AEStronglyMeasurable.add_iff_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

Tactic:
⟨fun h ↦ ⟨integrable_left_of_integrable_add_of_nonneg h_meas hf hg h,
    integrable_right_of_integrable_add_of_nonneg h_meas hf hg h⟩, fun ⟨hf, hg⟩ ↦ hf.add hg⟩

Premises used: MeasureTheory.Integrable, HAdd.hAdd, And.intro, Iff.intro, MeasureTheory.Integrable.add, _private.0.MeasureTheory.integrable_add_iff_of_nonneg.match_1, MeasureTheory.integrable_right_of_integrable_add_of_nonneg, MeasureTheory.integrable_left_of_integrable_add_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : f ≤ᶠ[ae μ] 0
hg : g ≤ᶠ[ae μ] 0
rw : Integrable (-f + -g) μ ↔ Integrable (-f) μ ∧ Integrable (-g) μ
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

Tactic:
rw [← integrable_neg_iff, ← integrable_neg_iff (f := f), ← integrable_neg_iff (f := g), neg_add]

Premises used: neg_add, MeasureTheory.integrable_neg_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : f ≤ᶠ[ae μ] 0
hg : g ≤ᶠ[ae μ] 0
⊢ Integrable (-f + -g) μ ↔ Integrable (-f) μ ∧ Integrable (-g) μ

Tactic:
integrable_add_iff_of_nonneg h_meas.neg (hf.mono (fun _ ↦ neg_nonneg_of_nonpos))
    (hg.mono (fun _ ↦ neg_nonneg_of_nonpos))

Premises used: MeasureTheory.integrable_add_iff_of_nonneg, MeasureTheory.AEStronglyMeasurable.neg, Filter.Eventually.mono, neg_nonneg_of_nonpos
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : f ≤ᶠ[ae μ] 0
hg : g ≤ᶠ[ae μ] 0
⊢ Integrable (-f + -g) μ ↔ Integrable (-f) μ ∧ Integrable (-g) μ

Tactic:
exact integrable_add_iff_of_nonneg h_meas.neg (hf.mono (fun _ ↦ neg_nonneg_of_nonpos))
    (hg.mono (fun _ ↦ neg_nonneg_of_nonpos))

Premises used: MeasureTheory.integrable_add_iff_of_nonneg, MeasureTheory.AEStronglyMeasurable.neg, Filter.Eventually.mono, neg_nonneg_of_nonpos
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
c : β
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ f x + c) μ ↔ Integrable f μ

Tactic:
integrable_add_iff_integrable_left (integrable_const _)

Premises used: MeasureTheory.integrable_add_iff_integrable_left, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
c : β
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ c + f x) μ ↔ Integrable f μ

Tactic:
integrable_add_iff_integrable_right (integrable_const _)

Premises used: MeasureTheory.integrable_add_iff_integrable_right, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f - g) μ

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: MeasureTheory.Integrable.neg, sub_eq_add_neg, MeasureTheory.Integrable.add
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable.{u_2, u_1} (ε := β) (fun (a : α) ↦ f a - g a) μ

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: MeasureTheory.Integrable.neg, sub_eq_add_neg, MeasureTheory.Integrable.add
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
left : AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ
right : HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ AEStronglyMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ HasFiniteIntegral (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
left : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖) μ
right : HasFiniteIntegral (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ ‖f a‖) μ

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

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

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
rw : ∀ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ), MemLp (f ⊓ g) 1 μ
⊢ Integrable (f ⊓ g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊓ g) 1 μ

Tactic:
hf.inf hg

Premises used: MeasureTheory.MemLp.inf
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊓ g) 1 μ

Tactic:
exact hf.inf hg

Premises used: MeasureTheory.MemLp.inf
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
rw : ∀ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ), MemLp (f ⊔ g) 1 μ
⊢ Integrable (f ⊔ g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊔ g) 1 μ

Tactic:
hf.sup hg

Premises used: MeasureTheory.MemLp.sup
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊔ g) 1 μ

Tactic:
exact hf.sup hg

Premises used: MeasureTheory.MemLp.sup
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
inst_1 : Lattice β
inst_2 : HasSolidNorm β
inst_3 : IsOrderedAddMonoid β
f : α → β
hf : Integrable f μ
rw : ∀ (hf : MemLp f 1 μ), MemLp.{u_1, u_8} (ε := β) (fun (a : α) ↦ |f a|) 1 μ
⊢ Integrable.{u_8, u_1} (ε := β) (fun (a : α) ↦ |f a|) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable