awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f : X → E
s : Set X
inst_5 : ClosedIciTopology E
inst_6 : CompleteSpace E
c : E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn.{u_1, u_3} (ε := E) (fun (x : X) ↦ f x) s μ
rw : LE.le.{u_3} (α := E) (∫ (x : X) in s, c ∂μ) (∫ (x : X) in s, f x ∂μ)
⊢ μ.real s • c ≤ ∫ (x : X) in s, f x ∂μ

Tactic:
rw [← setIntegral_const c]

Premises used: MeasureTheory.setIntegral_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f : X → E
s : Set X
inst_5 : ClosedIciTopology E
inst_6 : CompleteSpace E
c : E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn.{u_1, u_3} (ε := E) (fun (x : X) ↦ f x) s μ
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, c ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
setIntegral_mono_on (integrableOn_const hμs) hfint hs hf

Premises used: MeasureTheory.integrableOn_const, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f : X → E
s : Set X
inst_5 : ClosedIciTopology E
inst_6 : CompleteSpace E
c : E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn.{u_1, u_3} (ε := E) (fun (x : X) ↦ f x) s μ
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, c ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
exact setIntegral_mono_on (integrableOn_const hμs) hfint hs hf

Premises used: MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
s : Set X
f : X → ℝ
c : ℝ
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn (ε := ℝ) (fun (x : X) ↦ f x) s μ
⊢ c * μ.real s ≤ ∫ (x : X) in s, f x ∂μ

Tactic:
simpa [mul_comm] using setIntegral_ge_of_const_le hs hμs hf hfint

Premises used: MeasureTheory.setIntegral_ge_of_const_le, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
⊢ LE.le (α := ℝ) 0 (∫ (x : X) in s, f x ∂μ)

Tactic:
integral_nonneg_of_ae hf

Premises used: MeasureTheory.integral_nonneg_of_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hf : 0 ≤ᶠ[ae μ] f
⊢ LE.le (α := ℝ) 0 (∫ (x : X) in s, f x ∂μ)

Tactic:
setIntegral_nonneg_of_ae_restrict (ae_restrict_of_ae hf)

Premises used: MeasureTheory.ae_restrict_of_ae, MeasureTheory.setIntegral_nonneg_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ x ∈ s, 0 ≤ f x
⊢ LE.le (α := ℝ) 0 (∫ (x : X) in s, f x ∂μ)

Tactic:
setIntegral_nonneg_of_ae_restrict ((ae_restrict_iff' hs).mpr (ae_of_all μ hf))

Premises used: Iff.mpr, MeasureTheory.setIntegral_nonneg_of_ae_restrict, MeasureTheory.ae_of_all, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 ≤ f x
rwa : ∀ᵐ (x : X) ∂μ.restrict s, 0 x ≤ f x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ᵐ (x : X) ∂μ, x ∈ s → 0 x ≤ f x
⊢ 0 ≤ᶠ[ae (μ.restrict s)] f

Tactic:
rwa [EventuallyLE, ae_restrict_iff' hs]

Premises used: MeasureTheory.ae_restrict_iff', Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
rw : LE.le (α := ℝ) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X), indicator {a : X | 0 ≤ f a} f x ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in {y : X | 0 ≤ f y}, f x ∂μ)

Tactic:
rw [← integral_indicator hs, ←
    integral_indicator (stronglyMeasurable_const.measurableSet_le hf)]

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.integral_indicator, MeasureTheory.StronglyMeasurable.measurableSet_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X), indicator {a : X | 0 ≤ f a} f x ∂μ)

Tactic:
integral_mono (hfi.indicator hs)
      (hfi.indicator (stronglyMeasurable_const.measurableSet_le hf))
      (indicator_le_indicator_nonneg s f)

Premises used: MeasureTheory.stronglyMeasurable_const, Set.indicator_le_indicator_nonneg, MeasureTheory.integral_mono, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X), indicator {a : X | 0 ≤ f a} f x ∂μ)

Tactic:
exact
    integral_mono (hfi.indicator hs)
      (hfi.indicator (stronglyMeasurable_const.measurableSet_le hf))
      (indicator_le_indicator_nonneg s f)

Premises used: MeasureTheory.stronglyMeasurable_const, Set.indicator_le_indicator_nonneg, MeasureTheory.integral_mono, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hf : f ≤ᶠ[ae (μ.restrict s)] 0
⊢ LE.le (α := ℝ) (∫ (x : X) in s, f x ∂μ) 0

Tactic:
integral_nonpos_of_ae hf

Premises used: MeasureTheory.integral_nonpos_of_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hf : f ≤ᶠ[ae μ] 0
⊢ LE.le (α := ℝ) (∫ (x : X) in s, f x ∂μ) 0

Tactic:
setIntegral_nonpos_of_ae_restrict (ae_restrict_of_ae hf)

Premises used: MeasureTheory.ae_restrict_of_ae, MeasureTheory.setIntegral_nonpos_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0
rwa : ∀ᵐ (x : X) ∂μ.restrict s, f x ≤ 0 x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ 0 x
⊢ f ≤ᶠ[ae (μ.restrict s)] 0

Tactic:
rwa [EventuallyLE, ae_restrict_iff' hs]

Premises used: MeasureTheory.ae_restrict_iff', Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : ∀ x ∈ s, f x ≤ 0
⊢ LE.le (α := ℝ) (∫ (x : X) in s, f x ∂μ) 0

Tactic:
setIntegral_nonpos_ae hs <| ae_of_all μ hf

Premises used: MeasureTheory.setIntegral_nonpos_ae, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
rw : LE.le (α := ℝ) (∫ (x : X), indicator {a : X | f a ≤ 0} f x ∂μ) (∫ (x : X), s.indicator f x ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : X) in {y : X | f y ≤ 0}, f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
rw [← integral_indicator hs, ←
    integral_indicator (hf.measurableSet_le stronglyMeasurable_const)]

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.integral_indicator, MeasureTheory.StronglyMeasurable.measurableSet_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : X), indicator {a : X | f a ≤ 0} f x ∂μ) (∫ (x : X), s.indicator f x ∂μ)

Tactic:
integral_mono (hfi.indicator (hf.measurableSet_le stronglyMeasurable_const))
      (hfi.indicator hs) (indicator_nonpos_le_indicator s f)

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.integral_mono, Set.indicator_nonpos_le_indicator, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : X), indicator {a : X | f a ≤ 0} f x ∂μ) (∫ (x : X), s.indicator f x ∂μ)

Tactic:
exact
    integral_mono (hfi.indicator (hf.measurableSet_le stronglyMeasurable_const))
      (hfi.indicator hs) (indicator_nonpos_le_indicator s f)

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.integral_mono, Set.indicator_nonpos_le_indicator, MeasureTheory.StronglyMeasurable.measurableSet_le, MeasureTheory.Integrable.indicator
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
rw : (μ : (a : Set X) → ℝ≥0∞) s ≤ ∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ
⊢ (μ : (a : Set X) → ℝ≥0∞) s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal f_int f_nonneg]

Premises used: MeasureTheory.ofReal_integral_eq_lintegral_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
hf : AEMeasurable (β := ℝ≥0∞) (fun (a : X) ↦ ENNReal.ofReal (f a)) μ
hs₁ : ∀ x ∈ s, 1 ≤ ENNReal.ofReal (f x)
⊢ (μ : (a : Set X) → ℝ≥0∞) s ≤ ∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ

Tactic:
apply meas_le_lintegral₀

Premises used: MeasureTheory.meas_le_lintegral₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : X) ↦ ENNReal.ofReal (f a)) μ

Tactic:
ENNReal.continuous_ofReal.measurable.comp_aemeasurable f_int.1.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ENNReal.ofNNReal, ENNReal.ofReal, ENNReal.continuous_ofReal, WithTop.some, And.left, Continuous.measurable, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : X) ↦ ENNReal.ofReal (f a)) μ

Tactic:
exact ENNReal.continuous_ofReal.measurable.comp_aemeasurable f_int.1.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ENNReal.continuous_ofReal, And.left, Continuous.measurable, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
f_int : Integrable f μ
f_nonneg : 0 ≤ᶠ[ae μ] f
s : Set X
hs : ∀ x ∈ s, 1 ≤ f x
x : X
hx : x ∈ s
⊢ 1 ≤ ENNReal.ofReal (f x)

Tactic:
simpa using ENNReal.ofReal_le_ofReal (hs x hx)

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
pos : ∀ (H : Integrable f μ), ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
neg : ∀ (H : ¬Integrable f μ), ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s

Tactic:
by_cases H : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : ¬Integrable f μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s

Tactic:
simp [integral_undef H]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
⊢ Integrable g μ

Tactic:
have g_int : Integrable g μ := H.pos_part
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
h : LE.le (α := ℝ) (∫ (x : X), f x ∂μ) (∫ (x : X), g x ∂μ)
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)

Tactic:
apply ENNReal.ofReal_le_ofReal

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
⊢ LE.le (α := ℝ) (∫ (x : X), f x ∂μ) (∫ (x : X), g x ∂μ)

Tactic:
integral_mono H g_int (fun x ↦ le_max_left _ _)

Premises used: MeasureTheory.integral_mono, OfNat.ofNat, le_max_left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
⊢ LE.le (α := ℝ) (∫ (x : X), f x ∂μ) (∫ (x : X), g x ∂μ)

Tactic:
exact integral_mono H g_int (fun x ↦ le_max_left _ _)

Premises used: MeasureTheory.integral_mono, OfNat.ofNat, le_max_left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)

Tactic:
have : ENNReal.ofReal (∫ x, f x ∂μ) ≤ ENNReal.ofReal (∫ x, g x ∂μ) := by
    apply ENNReal.ofReal_le_ofReal
    exact integral_mono H g_int (fun x ↦ le_max_left _ _)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
pos : ENNReal.ofReal (∫ (x : X), g x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s

Tactic:
apply this.trans

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
pos : ∫⁻ (x : X), ENNReal.ofReal (g x) ∂μ ≤ (μ : (a : Set X) → ℝ≥0∞) s
⊢ ENNReal.ofReal (∫ (x : X), g x ∂μ) ≤ (μ : (a : Set X) → ℝ≥0∞) s

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal g_int (Eventually.of_forall (fun x ↦ le_max_right _ _))]

Premises used: le_max_right, Filter.Eventually.of_forall, MeasureTheory.ofReal_integral_eq_lintegral_ofReal, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
pos : ∀ (a : X), ENNReal.ofReal (g a) ≤ 1
pos₁ : ∀ a ∈ sᶜ, ENNReal.ofReal (g a) = 0
⊢ ∫⁻ (x : X), ENNReal.ofReal (g x) ∂μ ≤ (μ : (a : Set X) → ℝ≥0∞) s

Tactic:
apply lintegral_le_meas

Premises used: MeasureTheory.lintegral_le_meas
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
pos : g x ≤ ENNReal.toReal 1
⊢ ENNReal.ofReal (g x) ≤ 1

Tactic:
apply ENNReal.ofReal_le_of_le_toReal

Premises used: ENNReal.ofReal_le_of_le_toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
pos : ∀ (H : x ∈ s), g x ≤ ENNReal.toReal 1
neg : ∀ (H : x ∉ s), g x ≤ ENNReal.toReal 1
⊢ g x ≤ ENNReal.toReal 1

Tactic:
by_cases H : x ∈ s
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H_1 : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
H : x ∈ s
⊢ g x ≤ ENNReal.toReal 1

Tactic:
simpa [g] using hs x H
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H_1 : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
H : x ∉ s
apply : g x ≤ 0
⊢ g x ≤ ENNReal.toReal 1

Tactic:
apply le_trans _ zero_le_one

Premises used: zero_le_one, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H_1 : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
H : x ∉ s
⊢ g x ≤ 0

Tactic:
simpa [g] using h's x H
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
g : (x : X) → ℝ := fun (x : X) ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
x : X
hx : x ∈ sᶜ
⊢ ENNReal.ofReal (g x) = 0

Tactic:
simpa [g] using h's x hx
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
⊢ IntegrableOn f (iUnion s) μ

Tactic:
⟨AEStronglyMeasurable.iUnion fun i => (hi i).1, (lintegral_iUnion_le _ _).trans_lt ?_⟩

Premises used: MeasureTheory.lintegral_iUnion_le, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, And.left, And.intro, LE.le.trans_lt, MeasureTheory.AEStronglyMeasurable.iUnion
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
refine : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ) ∞
⊢ IntegrableOn f (iUnion s) μ

Tactic:
refine ⟨AEStronglyMeasurable.iUnion fun i => (hi i).1, (lintegral_iUnion_le _ _).trans_lt ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
⊢ ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)

Tactic:
have B := fun i => lintegral_coe_eq_integral (fun x : X => ‖f x‖₊) (hi i).norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
simp_rw : LT.lt (α := ℝ≥0∞) (∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, (↑‖f a‖₊ : ℝ) ∂μ)) ∞
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : X) in s i, ‖f a‖ₑ ∂μ) ∞

Tactic:
simp_rw [enorm_eq_nnnorm, tsum_congr B]

Premises used: tsum_congr, enorm_eq_nnnorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
rw : Summable (α := ℝ) fun (a : ι) ↦ (↑(NNReal.mk (∫ (x : X) in s a, (↑‖f x‖₊ : ℝ) ∂μ) ⋯) : ℝ)
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) ⋯

Tactic:
rw [← NNReal.summable_coe]

Premises used: NNReal.summable_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
⊢ Summable (α := ℝ) fun (a : ι) ↦ (↑(NNReal.mk (∫ (x : X) in s a, (↑‖f x‖₊ : ℝ) ∂μ) ⋯) : ℝ)

Tactic:
h

Premises used: NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
⊢ Summable (α := ℝ) fun (a : ι) ↦ (↑(NNReal.mk (∫ (x : X) in s a, (↑‖f x‖₊ : ℝ) ∂μ) ⋯) : ℝ)

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
f : X → E
s : ι → Set X
hi : ∀ (i : ι), IntegrableOn f (s i) μ
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X) in s i, ‖f x‖ ∂μ
B : ∀ (i : ι), ∫⁻ (a : X) in s i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : X) in s i, (↑‖f a‖₊ : ℝ) ∂μ)
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ NNReal.mk (∫ (x : X) in s i, (↑‖f x‖₊ : ℝ) ∂μ) ⋯

Tactic:
have S' : Summable fun i : ι =>
      (NNReal.mk (∫ x : X in s i, ‖f x‖₊ ∂μ) (integral_nonneg fun x => NNReal.coe_nonneg _)) := by
    rw [← NNReal.summable_coe]; exact h