awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm_1 : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s_1 : ι → Set X
li : Filter ι
hs : Tendsto s_1 li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s_1 i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
s : Set X
hμs : LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal) (⊤ : ENNReal)
h_integrable : IntegrableOn f s μ
hfm : AEStronglyMeasurable f (μ.restrict s)
h_norm : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε
h₁ : Norm.norm.{u_2} (E := E) (∫ (a : X) in s, f a - b ∂μ) ≤ ε * μ.real s
⊢ ‖∫ (x : X) in s, f x ∂μ - μ.real s • b‖ ≤ ε * ‖μ.real s‖

Tactic:
rw [← setIntegral_const,
    ← integral_sub h_integrable (integrableOn_const hμs.ne),
    Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]

Premises used: MeasureTheory.measureReal_nonneg, MeasureTheory.integral_sub, MeasureTheory.integrableOn_const, abs_of_nonneg, Real.norm_eq_abs, LT.lt.ne, MeasureTheory.setIntegral_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm_1 : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s_1 : ι → Set X
li : Filter ι
hs : Tendsto s_1 li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s_1 i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
s : Set X
hμs : LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal) (⊤ : ENNReal)
h_integrable : IntegrableOn f s μ
hfm : AEStronglyMeasurable f (μ.restrict s)
h_norm : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε
⊢ Norm.norm.{u_2} (E := E) (∫ (a : X) in s, f a - b ∂μ) ≤ ε * μ.real s

Tactic:
norm_setIntegral_le_of_norm_le_const_ae' hμs h_norm

Premises used: MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm_1 : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s_1 : ι → Set X
li : Filter ι
hs : Tendsto s_1 li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s_1 i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
s : Set X
hμs : LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal) (⊤ : ENNReal)
h_integrable : IntegrableOn f s μ
hfm : AEStronglyMeasurable f (μ.restrict s)
h_norm : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε
⊢ Norm.norm.{u_2} (E := E) (∫ (a : X) in s, f a - b ∂μ) ≤ ε * μ.real s

Tactic:
exact norm_setIntegral_le_of_norm_le_const_ae' hμs h_norm

Premises used: MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : TopologicalSpace X
inst_5 : OpensMeasurableSpace X
μ : Measure X
inst_6 : IsLocallyFiniteMeasure μ
x : X
t : Set X
f : X → E
hx : ContinuousWithinAt f t x
ht : MeasurableSet t
hfm : StronglyMeasurableAtFilter f (𝓝[t] x) μ
s : ι → Set X
li : Filter ι
hs : Tendsto s li (𝓝[t] x).smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
⊢ IsLittleO.{u_3, u_2, 0} (E := E) li (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ - m i • f x) m

Tactic:
haveI : (𝓝[t] x).IsMeasurablyGenerated := ht.nhdsWithin_isMeasurablyGenerated _
  (hx.mono_left inf_le_left).integral_sub_linear_isLittleO_ae hfm (μ.finiteAt_nhdsWithin x t) hs m
    hsμ

Premises used: MeasureTheory.Measure.finiteAt_nhdsWithin, Filter.Tendsto.integral_sub_linear_isLittleO_ae, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : TopologicalSpace X
inst_5 : OpensMeasurableSpace X
μ : Measure X
inst_6 : IsLocallyFiniteMeasure μ
x : X
f : X → E
hx : ContinuousAt f x
hfm : StronglyMeasurableAtFilter f (𝓝 x) μ
s : ι → Set X
li : Filter ι
hs : Tendsto s li (𝓝 x).smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
⊢ IsLittleO.{u_3, u_2, 0} (E := E) li (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ - m i • f x) m

Tactic:
(hx.mono_left inf_le_left).integral_sub_linear_isLittleO_ae hfm (μ.finiteAt_nhds x) hs m hsμ

Premises used: MeasureTheory.Measure.finiteAt_nhds, Filter.Tendsto.integral_sub_linear_isLittleO_ae, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : TopologicalSpace X
inst_5 : OpensMeasurableSpace X
inst_6 : SecondCountableTopologyEither X E
μ : Measure X
inst_7 : IsLocallyFiniteMeasure μ
x : X
t : Set X
f : X → E
hft : ContinuousOn f t
hx : x ∈ t
ht : MeasurableSet t
s : ι → Set X
li : Filter ι
hs : Tendsto s li (𝓝[t] x).smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
⊢ IsLittleO.{u_3, u_2, 0} (E := E) li (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ - m i • f x) m

Tactic:
(hft x hx).integral_sub_linear_isLittleO_ae ht
    ⟨t, self_mem_nhdsWithin, hft.aestronglyMeasurable ht⟩ hs m hsμ

Premises used: ContinuousOn.aestronglyMeasurable, ContinuousWithinAt.integral_sub_linear_isLittleO_ae, self_mem_nhdsWithin, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
x : F
⊢ (weightedSMul μ s : (a : F) → F) x = μ.real s • x

Tactic:
simp [weightedSMul]

Premises used: MeasureTheory.weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
h : ∀ (x : Set α), Eq.{u_3 + 1} (α := F →L[ℝ] F) (@weightedSMul _ _ _ _ m 0 x) (0 x)
⊢ Eq (α := (s : Set α) → F →L[ℝ] F) (@weightedSMul _ _ _ _ m 0) 0

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
x : Set α
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] F) (@weightedSMul _ _ _ _ m 0 x) (0 x)

Tactic:
simp [weightedSMul]

Premises used: MeasureTheory.weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
h : ∀ (x : F), Eq (α := F) ((weightedSMul μ ∅ : (a : F) → F) x : F) ((0 : (a : F) → F) x : F)
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] F) (weightedSMul μ ∅) 0

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
h : μ.real ∅ • x = (0 : (a : F) → F) x
⊢ Eq (α := F) ((weightedSMul μ ∅ : (a : F) → F) x : F) ((0 : (a : F) → F) x : F)

Tactic:
rw [weightedSMul_apply]

Premises used: MeasureTheory.weightedSMul_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ μ.real ∅ • x = (0 : (a : F) → F) x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (x : F),
    Eq (α := F) ((weightedSMul (μ + ν) s : (a : F) → F) x : F)
      ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul ν s) : (a : F) → F) x : F)
⊢ weightedSMul (μ + ν) s = HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul ν s)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F
h :
  (weightedSMul (μ + ν) s : (a : F) → F) x =
    HAdd.hAdd (α := (a : F) → F) (β := (a : F) → F) (⇑(weightedSMul μ s) : (a : F) → F)
      (⇑(weightedSMul ν s) : (a : F) → F) x
⊢ Eq (α := F) ((weightedSMul (μ + ν) s : (a : F) → F) x : F)
    ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul ν s) : (a : F) → F) x : F)

Tactic:
push_cast
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F
h : (μ + ν).real s • x = μ.real s • x + ν.real s • x
⊢ (weightedSMul (μ + ν) s : (a : F) → F) x =
    HAdd.hAdd (α := (a : F) → F) (β := (a : F) → F) (⇑(weightedSMul μ s) : (a : F) → F)
      (⇑(weightedSMul ν s) : (a : F) → F) x

Tactic:
simp_rw [Pi.add_apply, weightedSMul_apply]

Premises used: MeasureTheory.weightedSMul_apply, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F
h : (μ.real s + ν.real s) • x = μ.real s • x + ν.real s • x
h₁ h₂ : μ.real s • x + ν.real s • x = μ.real s • x + ν.real s • x
⊢ (μ + ν).real s • x = μ.real s • x + ν.real s • x

Tactic:
rw [measureReal_add_apply, add_smul]

Premises used: MeasureTheory.measureReal_add_apply, add_smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
h :
  ∀ (x : F),
    Eq (α := F) ((weightedSMul (c • μ) s : (a : F) → F) x : F)
      ((HSMul.hSMul (β := F →L[ℝ] F) c.toReal (weightedSMul μ s) : (a : F) → F) x : F)
⊢ weightedSMul (c • μ) s = HSMul.hSMul (β := F →L[ℝ] F) c.toReal (weightedSMul μ s)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
x : F
⊢ Eq (α := F) ((weightedSMul (c • μ) s : (a : F) → F) x : F)
    ((HSMul.hSMul (β := F →L[ℝ] F) c.toReal (weightedSMul μ s) : (a : F) → F) x : F)

Tactic:
simp [weightedSMul_apply, smul_smul]

Premises used: MeasureTheory.weightedSMul_apply, smul_smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h : ∀ (x : F), Eq (α := F) ((weightedSMul μ s : (a : F) → F) x : F) ((weightedSMul μ t : (a : F) → F) x : F)
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
x : F
h : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) • x = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) • x
⊢ Eq (α := F) ((weightedSMul μ s : (a : F) → F) x : F) ((weightedSMul μ t : (a : F) → F) x : F)

Tactic:
simp_rw [weightedSMul_apply, measureReal_def]

Premises used: MeasureTheory.weightedSMul_apply, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
x : F
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) • x = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) • x

Tactic:
congr 2
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h : ∀ (x : F), Eq (α := F) ((weightedSMul μ s : (a : F) → F) x : F) ((0 : (a : F) → F) x : F)
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] F) (weightedSMul μ s) 0

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : F
h : ENNReal.toReal 0 • x = (0 : (a : F) → F) x
⊢ Eq (α := F) ((weightedSMul μ s : (a : F) → F) x : F) ((0 : (a : F) → F) x : F)

Tactic:
rw [weightedSMul_apply, measureReal_def, h_zero]

Premises used: MeasureTheory.weightedSMul_apply, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : F
⊢ ENNReal.toReal 0 • x = (0 : (a : F) → F) x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hdisj : Disjoint s t
h :
  ∀ (x : F),
    Eq (α := F) ((weightedSMul μ (s ∪ t) : (a : F) → F) x : F)
      ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t) : (a : F) → F) x : F)
⊢ weightedSMul μ (s ∪ t) = HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hdisj : Disjoint s t
x : F
h :
  (weightedSMul μ (s ∪ t) : (a : F) → F) x =
    HAdd.hAdd (α := F) (β := F) ((weightedSMul μ s : (a : F) → F) x : F) ((weightedSMul μ t : (a : F) → F) x : F)
h₁ : μ.real (s ∪ t) • x = μ.real s • x + μ.real t • x
h₂ : (μ.real s + μ.real t) • x = μ.real s • x + μ.real t • x
⊢ Eq (α := F) ((weightedSMul μ (s ∪ t) : (a : F) → F) x : F)
    ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t) : (a : F) → F) x : F)

Tactic:
simp_rw [add_apply, weightedSMul_apply, measureReal_union hdisj ht, add_smul]

Premises used: MeasureTheory.weightedSMul_apply, ContinuousLinearMap.add_apply, add_smul, MeasureTheory.measureReal_union
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
_hs : MeasurableSet s
ht : MeasurableSet t
hs_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hdisj : Disjoint s t
⊢ weightedSMul μ (s ∪ t) = HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t)

Tactic:
weightedSMul_union' s t ht hs_finite ht_finite hdisj

Premises used: MeasureTheory.weightedSMul_union'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
𝕜 : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : SMul 𝕜 F
inst_3 : SMulCommClass ℝ 𝕜 F
c : 𝕜
s : Set α
x : F
simp_rw : μ.real s • c • x = c • μ.real s • x
⊢ (weightedSMul μ s : (a : F) → F) (c • x) = HSMul.hSMul (β := F) c ((weightedSMul μ s : (a : F) → F) x : F)

Tactic:
simp_rw [weightedSMul_apply, smul_comm]

Premises used: MeasureTheory.weightedSMul_apply, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
⊢ norm.{u_3} (E := F →L[ℝ] F) (weightedSMul μ s) ≤ μ.real s

Tactic:
calc
    ‖(weightedSMul μ s : F →L[ℝ] F)‖ = ‖μ.real s‖ * ‖ContinuousLinearMap.id ℝ F‖ :=
      norm_smul (μ.real s) (ContinuousLinearMap.id ℝ F)
    _ ≤ ‖μ.real s‖ :=
      ((mul_le_mul_of_nonneg_left norm_id_le (norm_nonneg _)).trans (mul_one _).le)
    _ = abs μ.real s := Real.norm_eq_abs _
    _ = μ.real s := abs_eq_self.mpr ENNReal.toReal_nonneg

Premises used: Iff.mpr, Real, Trans.trans, norm_smul, MeasureTheory.Measure.real, ContinuousLinearMap.id, Eq.le, ENNReal.toReal_nonneg, ContinuousLinearMap.norm_id_le, LE.le.trans, mul_one, abs_eq_self, mul_le_mul_of_nonneg_left, norm_nonneg, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : MeasurableSpace α
μ : Measure α
⊢ DominatedFinMeasAdditive.{u_1, u_3} (β := F →L[ℝ] F) μ (weightedSMul μ) 1

Tactic:
⟨weightedSMul_union, fun s _ _ => (norm_weightedSMul_le s).trans (one_mul _).symm.le⟩

Premises used: MeasureTheory.Measure.real, Eq.le, MeasureTheory.norm_weightedSMul_le, MeasureTheory.weightedSMul_union, MeasureTheory.DominatedFinMeasAdditive, And.intro, LE.le.trans, Eq.symm, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedModule ℝ F
s : Set α
x : F
hx : 0 ≤ x
simp : 0 ≤ μ.real s • x
⊢ LE.le (α := F) (0 : F) ((weightedSMul μ s : (a : F) → F) x : F)

Tactic:
simp only [weightedSMul, coe_smul', _root_.id, coe_id', Pi.smul_apply]

Premises used: ContinuousLinearMap.coe_smul', id, MeasureTheory.weightedSMul, ContinuousLinearMap.coe_id', Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedModule ℝ F
s : Set α
x : F
hx : 0 ≤ x
⊢ 0 ≤ μ.real s • x

Tactic:
smul_nonneg toReal_nonneg hx

Premises used: smul_nonneg, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedModule ℝ F
s : Set α
x : F
hx : 0 ≤ x
⊢ 0 ≤ μ.real s • x

Tactic:
exact smul_nonneg toReal_nonneg hx

Premises used: smul_nonneg, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
H : ∀ (a : α), Eq (α := ℝ) ((map norm f.posPart : (a : α) → ℝ) a : ℝ) ((f.posPart : (a : α) → ℝ) a : ℝ)
⊢ map norm f.posPart = f.posPart

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
a : α
H : LE.le (α := ℝ) (0 : ℝ) ((f.posPart : (a : α) → ℝ) a : ℝ)
⊢ Eq (α := ℝ) ((map norm f.posPart : (a : α) → ℝ) a : ℝ) ((f.posPart : (a : α) → ℝ) a : ℝ)

Tactic:
rw [map_apply, Real.norm_eq_abs, abs_of_nonneg]

Premises used: abs_of_nonneg, MeasureTheory.SimpleFunc.map_apply, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ LE.le (α := ℝ) (0 : ℝ) ((f.posPart : (a : α) → ℝ) a : ℝ)

Tactic:
le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ LE.le (α := ℝ) (0 : ℝ) ((f.posPart : (a : α) → ℝ) a : ℝ)

Tactic:
exact le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (-f).posPart = (-f).posPart

Tactic:
posPart_map_norm _

Premises used: MeasureTheory.SimpleFunc.posPart_map_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (-f).posPart = (-f).posPart

Tactic:
exact posPart_map_norm _

Premises used: MeasureTheory.SimpleFunc.posPart_map_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
H :
  ∀ (a : α),
    Eq (α := ℝ)
      ((HSub.hSub (α := α →ₛ ℝ) (map (fun (b : ℝ) ↦ max b 0) f) (map (fun (b : ℝ) ↦ max b 0) (-f)) : (a : α) → ℝ) a : ℝ)
      ((f : (a : α) → ℝ) a : ℝ)
⊢ HSub.hSub (α := α →ₛ ℝ) (map (fun (b : ℝ) ↦ max b 0) f) (map (fun (b : ℝ) ↦ max b 0) (-f)) = f

Tactic:
ext a
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ HSub.hSub (α := (a : α) → ℝ) (β := (a : α) → ℝ) (⇑(map (fun (b : ℝ) ↦ max b 0) f) : (a : α) → ℝ)
      (⇑(map (fun (b : ℝ) ↦ max b 0) (-f)) : (a : α) → ℝ) a =
    (f : (a : α) → ℝ) a

Tactic:
max_zero_sub_eq_self (f a)

Premises used: max_zero_sub_eq_self, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ HSub.hSub (α := (a : α) → ℝ) (β := (a : α) → ℝ) (⇑(map (fun (b : ℝ) ↦ max b 0) f) : (a : α) → ℝ)
      (⇑(map (fun (b : ℝ) ↦ max b 0) (-f)) : (a : α) → ℝ) a =
    (f : (a : α) → ℝ) a

Tactic:
exact max_zero_sub_eq_self (f a)

Premises used: max_zero_sub_eq_self, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : MeasurableSpace α
μ : Measure α
f : α →ₛ F
⊢ integral μ f = setToSimpleFunc (weightedSMul μ) f

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.integral, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
f : α →ₛ F
⊢ integral μ f = ∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x

Tactic:
simp [integral, setToSimpleFunc, weightedSMul_apply]

Premises used: MeasureTheory.weightedSMul_apply, MeasureTheory.SimpleFunc.setToSimpleFunc, MeasureTheory.SimpleFunc.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
simp_rw :
  setToSimpleFunc (weightedSMul μ) f =
    ∑ x ∈ f.range with x ≠ 0, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x
simp_rw₁ :
  Eq (α := F)
    (∑ x ∈ f.range with x ≠ 0, (weightedSMul μ (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F) x)
    (∑ x ∈ f.range with x ≠ 0, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
⊢ integral μ f = ∑ x ∈ f.range with x ≠ 0, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x

Tactic:
simp_rw [integral_def, setToSimpleFunc_eq_sum_filter, weightedSMul_apply]

Premises used: MeasureTheory.weightedSMul_apply, MeasureTheory.SimpleFunc.integral_def, MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter