awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
α : Type u_6
inst_2 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → G
⊢ Eq.{u_5 + 1} (α := G)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ) fun (x : (↑s : Type u_6)) ↦ f (↑x : α))
    (@integral _ _ _ _ inst_2
      (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ))
      fun (x : α) ↦ f x)

Tactic:
exact ((MeasurableEmbedding.subtype_coe hs).integral_map _).symm

Premises used: MeasurableEmbedding.integral_map, Eq.symm, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
α : Type u_6
inst_2 : MeasureSpace α
s : Set α
hs : MeasurableSet s
f : α → G
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (↑s : Type u_6)) ↦ f (↑x : α))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : α) ↦ f x)

Tactic:
integral_subtype_comap hs f

Premises used: MeasureTheory.integral_subtype_comap
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f x)
    (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f a)

Tactic:
integral_congr_ae <| ae_eq_dirac' hfm.measurable

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.ae_eq_dirac'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f a) = f a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
f₁ : (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f a) = f a
⊢ (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f x) = f a

Tactic:
calc
    ∫ x, f x ∂Measure.dirac a = ∫ _, f a ∂Measure.dirac a :=
      integral_congr_ae <| ae_eq_dirac' hfm.measurable
    _ = f a := by simp

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.Measure.dirac, MeasureTheory.ae_eq_dirac'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
⊢ (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f a) = f a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst_2 : Decidable (a ∈ s)
rw : (@integral _ _ _ _ mα (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
⊢ (@integral _ _ _ _ mα (Measure.restrict (Measure.dirac a) s) fun (x : α) ↦ f x) = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac' hs]

Premises used: MeasureTheory.restrict_dirac'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst_2 : Decidable (a ∈ s)
pos : a ∈ s → (@integral _ _ _ _ mα (Measure.dirac a) fun (x : α) ↦ f x) = f a
neg : a ∉ s → Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ mα 0 fun (x : α) ↦ f x) 0
⊢ (@integral _ _ _ _ mα (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst_2 : Decidable (a ∈ s)
h : a ∈ s
⊢ (@integral _ _ _ _ mα (Measure.dirac a) fun (x : α) ↦ f x) = f a

Tactic:
integral_dirac' _ _ hf

Premises used: MeasureTheory.integral_dirac'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst_2 : Decidable (a ∈ s)
h : a ∈ s
⊢ (@integral _ _ _ _ mα (Measure.dirac a) fun (x : α) ↦ f x) = f a

Tactic:
exact integral_dirac' _ _ hf

Premises used: MeasureTheory.integral_dirac'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst_2 : Decidable (a ∈ s)
h : a ∉ s
⊢ Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ mα 0 fun (x : α) ↦ f x) 0

Tactic:
integral_zero_measure _

Premises used: MeasureTheory.integral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst_2 : Decidable (a ∈ s)
h : a ∉ s
⊢ Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ mα 0 fun (x : α) ↦ f x) 0

Tactic:
exact integral_zero_measure _

Premises used: MeasureTheory.integral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst_4 : Decidable (a ∈ s)
rw : (@integral _ _ _ _ inst_2 (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
⊢ (@integral _ _ _ _ inst_2 (Measure.restrict (Measure.dirac a) s) fun (x : α) ↦ f x) = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac]

Premises used: MeasureTheory.restrict_dirac
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst_4 : Decidable (a ∈ s)
pos : a ∈ s → (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f x) = f a
neg : a ∉ s → Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst_2 0 fun (x : α) ↦ f x) 0
⊢ (@integral _ _ _ _ inst_2 (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst_4 : Decidable (a ∈ s)
h : a ∈ s
⊢ (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f x) = f a

Tactic:
integral_dirac _ _

Premises used: MeasureTheory.integral_dirac
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst_4 : Decidable (a ∈ s)
h : a ∈ s
⊢ (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f x) = f a

Tactic:
exact integral_dirac _ _

Premises used: MeasureTheory.integral_dirac
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst_4 : Decidable (a ∈ s)
h : a ∉ s
⊢ Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst_2 0 fun (x : α) ↦ f x) 0

Tactic:
integral_zero_measure _

Premises used: MeasureTheory.integral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst_4 : Decidable (a ∈ s)
h : a ∉ s
⊢ Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ inst_2 0 fun (x : α) ↦ f x) 0

Tactic:
exact integral_zero_measure _

Premises used: MeasureTheory.integral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
inl :
  ∀ (hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
inr :
  ∀ (hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
⊢ ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ

Tactic:
rcases eq_top_or_lt_top (μ {x | ε ≤ f x}) with hμ | hμ

Premises used: setOf, LE.le, DFunLike.coe, eq_top_or_lt_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ

Tactic:
simpa [measureReal_def, hμ] using integral_nonneg_of_ae hf_nonneg

Premises used: MeasureTheory.integral_nonneg_of_ae, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have := Fact.mk hμ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ε * μ.real {x : α | ε ≤ f x} = ∫ (x : α) in {x : α | ε ≤ f x}, ε ∂μ

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | ε ≤ f x}, ε ∂μ) (∫ (x : α) in {x : α | ε ≤ f x}, f x ∂μ)

Tactic:
integral_mono_ae (integrable_const _) (hf_int.mono_measure μ.restrict_le_self) <|
          ae_restrict_mem₀ <| hf_int.aemeasurable.nullMeasurable measurableSet_Ici

Premises used: MeasureTheory.Integrable.mono_measure, AEMeasurable.nullMeasurable, MeasureTheory.ae_restrict_mem₀, MeasureTheory.Integrable.aemeasurable, MeasureTheory.integral_mono_ae, MeasureTheory.Measure.restrict_le_self, measurableSet_Ici, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | ε ≤ f x}, f x ∂μ) (∫ (a : α), f a ∂μ)

Tactic:
integral_mono_measure μ.restrict_le_self hf_nonneg hf_int

Premises used: MeasureTheory.integral_mono_measure, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (∞ : ℝ≥0∞))
ε₁ : ε * μ.real {x : α | ε ≤ f x} = ∫ (x : α) in {x : α | ε ≤ f x}, ε ∂μ
⊢ ε * μ.real {x : α | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ

Tactic:
calc
      ε * μ.real { x | ε ≤ f x } = ∫ _ in {x | ε ≤ f x}, ε ∂μ := by simp [mul_comm]
      _ ≤ ∫ x in {x | ε ≤ f x}, f x ∂μ :=
        integral_mono_ae (integrable_const _) (hf_int.mono_measure μ.restrict_le_self) <|
          ae_restrict_mem₀ <| hf_int.aemeasurable.nullMeasurable measurableSet_Ici
      _ ≤ _ := integral_mono_measure μ.restrict_le_self hf_nonneg hf_int

Premises used: MeasureTheory.Integrable.mono_measure, AEMeasurable.nullMeasurable, setOf, MeasureTheory.Measure.real, MeasureTheory.ae_restrict_mem₀, MeasureTheory.Integrable.aemeasurable, LE.le, MeasureTheory.integral_mono_ae, MeasureTheory.integral_mono_measure, MeasureTheory.Measure.restrict_le_self, measurableSet_Ici, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
rw :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖ ^ q
hfm : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖g a‖ ^ q) μ
hf₂ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p
hfm₁ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p) μ
hf₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ * ‖g a‖
hfm₂ : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ * ‖g a‖) μ
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤
    HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p ∂μ) (1 / p) * HPow.hPow (α := ℝ) (∫ (a : α), ‖g a‖ ^ q ∂μ) (1 / q)

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
    integral_eq_lintegral_of_nonneg_ae]

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
⊢ LE.le (α := ℝ) (0 x) ((fun (a : α) ↦ ‖g a‖ ^ q) x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖ ^ q

Tactic:
exact Eventually.of_forall fun x ↦ by positivity

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖g a‖ ^ q) μ

Tactic:
(hg.1.norm.aemeasurable.pow aemeasurable_const).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.pow, MeasureTheory.AEStronglyMeasurable.norm, And.left, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖g a‖ ^ q) μ

Tactic:
exact (hg.1.norm.aemeasurable.pow aemeasurable_const).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.pow, MeasureTheory.AEStronglyMeasurable.norm, And.left, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
⊢ LE.le (α := ℝ) (0 x) ((fun (a : α) ↦ ‖f a‖ ^ p) x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p

Tactic:
exact Eventually.of_forall fun x ↦ by positivity

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p) μ

Tactic:
(hf.1.norm.aemeasurable.pow aemeasurable_const).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.pow, MeasureTheory.AEStronglyMeasurable.norm, And.left, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p) μ

Tactic:
exact (hf.1.norm.aemeasurable.pow aemeasurable_const).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.pow, MeasureTheory.AEStronglyMeasurable.norm, And.left, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
x : α
⊢ LE.le (α := ℝ) (0 x) ((fun (a : α) ↦ ‖f a‖ * ‖g a‖) x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ * ‖g a‖

Tactic:
exact Eventually.of_forall fun x ↦ by positivity

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ * ‖g a‖) μ

Tactic:
hf.1.norm.mul hg.1.norm

Premises used: MeasureTheory.AEStronglyMeasurable.norm, And.left, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ * ‖g a‖) μ

Tactic:
exact hf.1.norm.mul hg.1.norm

Premises used: MeasureTheory.AEStronglyMeasurable.norm, And.left, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
rw :
  (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)

Tactic:
rw [ENNReal.toReal_rpow, ENNReal.toReal_rpow, ← ENNReal.toReal_mul]

Premises used: ENNReal.toReal_mul, ENNReal.toReal_rpow
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
simp_rw : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ * ‖g a‖ₑ ∂μ
simp_rw₁ : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ * ENNReal.ofReal ‖g a‖ ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ

Tactic:
simp_rw [Pi.mul_apply, ← ofReal_norm, ENNReal.ofReal_mul (norm_nonneg _)]

Premises used: Pi.mul_apply, ENNReal.ofReal_mul, ofReal_norm, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ

Tactic:
have h_left : ∫⁻ a, ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
      ∫⁻ a, ((‖f ·‖ₑ) * (‖g ·‖ₑ)) a ∂μ := by
    simp_rw [Pi.mul_apply, ← ofReal_norm, ENNReal.ofReal_mul (norm_nonneg _)]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left :
  ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ =
    ∫⁻ (a : α), HMul.hMul (α := α → ℝ≥0∞) (β := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) a ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ

Tactic:
lintegral_congr fun x => ?_

Premises used: MeasureTheory.lintegral_congr