[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
⊢ ↑↑↑f =ᵐ[μ] 0
[PROOFSTEP]
obtain ⟨g, hg_sm, hfg⟩ := lpMeas.ae_fin_strongly_measurable' hm f hp_ne_zero hp_ne_top
[GOAL]
case intro.intro
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ↑↑↑f =ᵐ[μ] g
⊢ ↑↑↑f =ᵐ[μ] 0
[PROOFSTEP]
refine'
  hfg.trans
    _
      -- Porting note: added
[GOAL]
case intro.intro
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ↑↑↑f =ᵐ[μ] g
⊢ g =ᵐ[μ] 0
[PROOFSTEP]
unfold Filter.EventuallyEq at hfg
[GOAL]
case intro.intro
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x
⊢ g =ᵐ[μ] 0
[PROOFSTEP]
refine' ae_eq_zero_of_forall_set_integral_eq_of_finStronglyMeasurable_trim hm _ _ hg_sm
[GOAL]
case intro.intro.refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
[PROOFSTEP]
intro s hs hμs
[GOAL]
case intro.intro.refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ IntegrableOn g s
[PROOFSTEP]
have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg
[GOAL]
case intro.intro.refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hfg_restrict : ↑↑↑f =ᵐ[Measure.restrict μ s] g
⊢ IntegrableOn g s
[PROOFSTEP]
rw [IntegrableOn, integrable_congr hfg_restrict.symm]
[GOAL]
case intro.intro.refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hfg_restrict : ↑↑↑f =ᵐ[Measure.restrict μ s] g
⊢ Integrable ↑↑↑f
[PROOFSTEP]
exact hf_int_finite s hs hμs
[GOAL]
case intro.intro.refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = 0
[PROOFSTEP]
intro s hs hμs
[GOAL]
case intro.intro.refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ∫ (x : α) in s, g x ∂μ = 0
[PROOFSTEP]
have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg
[GOAL]
case intro.intro.refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hfg_restrict : ↑↑↑f =ᵐ[Measure.restrict μ s] g
⊢ ∫ (x : α) in s, g x ∂μ = 0
[PROOFSTEP]
rw [integral_congr_ae hfg_restrict.symm]
[GOAL]
case intro.intro.refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ lpMeas E' 𝕜 m p μ }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (Measure.trim μ hm)
hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hfg_restrict : ↑↑↑f =ᵐ[Measure.restrict μ s] g
⊢ ∫ (a : α) in s, ↑↑↑f a ∂μ = 0
[PROOFSTEP]
exact hf_zero s hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
⊢ ↑↑f =ᵐ[μ] 0
[PROOFSTEP]
let f_meas : lpMeas E' 𝕜 m p μ :=
  ⟨f, hf_meas⟩
    -- Porting note: `simp only` does not call `rfl` to try to close the goal. See https://github.com/leanprover-community/mathlib4/issues/5025
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
⊢ ↑↑f =ᵐ[μ] 0
[PROOFSTEP]
have hf_f_meas : f =ᵐ[μ] f_meas := by simp only [Subtype.coe_mk]; rfl
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
⊢ ↑↑f =ᵐ[μ] ↑↑↑f_meas
[PROOFSTEP]
simp only [Subtype.coe_mk]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
⊢ ↑↑f =ᵐ[μ] ↑↑f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
⊢ ↑↑f =ᵐ[μ] 0
[PROOFSTEP]
refine' hf_f_meas.trans _
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
⊢ ↑↑↑f_meas =ᵐ[μ] 0
[PROOFSTEP]
refine' lpMeas.ae_eq_zero_of_forall_set_integral_eq_zero hm f_meas hp_ne_zero hp_ne_top _ _
[GOAL]
case refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑↑f_meas) s
[PROOFSTEP]
intro s hs hμs
[GOAL]
case refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ IntegrableOn (↑↑↑f_meas) s
[PROOFSTEP]
have hfg_restrict : f =ᵐ[μ.restrict s] f_meas := ae_restrict_of_ae hf_f_meas
[GOAL]
case refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hfg_restrict : ↑↑f =ᵐ[Measure.restrict μ s] ↑↑↑f_meas
⊢ IntegrableOn (↑↑↑f_meas) s
[PROOFSTEP]
rw [IntegrableOn, integrable_congr hfg_restrict.symm]
[GOAL]
case refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hfg_restrict : ↑↑f =ᵐ[Measure.restrict μ s] ↑↑↑f_meas
⊢ Integrable ↑↑f
[PROOFSTEP]
exact hf_int_finite s hs hμs
[GOAL]
case refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f_meas x ∂μ = 0
[PROOFSTEP]
intro s hs hμs
[GOAL]
case refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ∫ (x : α) in s, ↑↑↑f_meas x ∂μ = 0
[PROOFSTEP]
have hfg_restrict : f =ᵐ[μ.restrict s] f_meas := ae_restrict_of_ae hf_f_meas
[GOAL]
case refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hfg_restrict : ↑↑f =ᵐ[Measure.restrict μ s] ↑↑↑f_meas
⊢ ∫ (x : α) in s, ↑↑↑f_meas x ∂μ = 0
[PROOFSTEP]
rw [integral_congr_ae hfg_restrict.symm]
[GOAL]
case refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
f_meas : { x // x ∈ lpMeas E' 𝕜 m p μ } := { val := f, property := hf_meas }
hf_f_meas : ↑↑f =ᵐ[μ] ↑↑↑f_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hfg_restrict : ↑↑f =ᵐ[Measure.restrict μ s] ↑↑↑f_meas
⊢ ∫ (a : α) in s, ↑↑f a ∂μ = 0
[PROOFSTEP]
exact hf_zero s hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
⊢ ↑↑f =ᵐ[μ] ↑↑g
[PROOFSTEP]
suffices h_sub : ⇑(f - g) =ᵐ[μ] 0
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
h_sub : ↑↑(f - g) =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] ↑↑g
[PROOFSTEP]
rw [← sub_ae_eq_zero]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
h_sub : ↑↑(f - g) =ᵐ[μ] 0
⊢ ↑↑f - ↑↑g =ᵐ[μ] 0
[PROOFSTEP]
exact (Lp.coeFn_sub f g).symm.trans h_sub
[GOAL]
case h_sub
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
⊢ ↑↑(f - g) =ᵐ[μ] 0
[PROOFSTEP]
have hfg' : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 :=
  by
  intro s hs hμs
  rw [integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))]
  rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
  exact sub_eq_zero.mpr (hfg s hs hμs)
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
[PROOFSTEP]
intro s hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
[PROOFSTEP]
rw [integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ∫ (a : α) in s, (↑↑f - ↑↑g) a ∂μ = 0
[PROOFSTEP]
rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ∫ (a : α) in s, ↑↑f a ∂μ - ∫ (a : α) in s, ↑↑g a ∂μ = 0
[PROOFSTEP]
exact sub_eq_zero.mpr (hfg s hs hμs)
[GOAL]
case h_sub
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
hfg' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
⊢ ↑↑(f - g) =ᵐ[μ] 0
[PROOFSTEP]
have hfg_int : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn (⇑(f - g)) s μ :=
  by
  intro s hs hμs
  rw [IntegrableOn, integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub f g))]
  exact (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
hfg' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑(f - g)) s
[PROOFSTEP]
intro s hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
hfg' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ IntegrableOn (↑↑(f - g)) s
[PROOFSTEP]
rw [IntegrableOn, integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub f g))]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
hfg' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ Integrable fun x => (↑↑f - ↑↑g) x
[PROOFSTEP]
exact (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
[GOAL]
case h_sub
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
hfg' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
hfg_int : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑(f - g)) s
⊢ ↑↑(f - g) =ᵐ[μ] 0
[PROOFSTEP]
have hfg_meas : AEStronglyMeasurable' m (⇑(f - g)) μ :=
  AEStronglyMeasurable'.congr (hf_meas.sub hg_meas) (Lp.coeFn_sub f g).symm
[GOAL]
case h_sub
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
hm : m ≤ m0
f g : { x // x ∈ Lp E' p }
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑f) s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑g) s
hfg : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable' m (↑↑f) μ
hg_meas : AEStronglyMeasurable' m (↑↑g) μ
hfg' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
hfg_int : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn (↑↑(f - g)) s
hfg_meas : AEStronglyMeasurable' m (↑↑(f - g)) μ
⊢ ↑↑(f - g) =ᵐ[μ] 0
[PROOFSTEP]
exact Lp.ae_eq_zero_of_forall_set_integral_eq_zero' 𝕜 hm (f - g) hp_ne_zero hp_ne_top hfg_int hfg' hfg_meas
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
⊢ f =ᵐ[μ] g
[PROOFSTEP]
rw [← ae_eq_trim_iff_of_aeStronglyMeasurable' hm hfm hgm]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
⊢ AEStronglyMeasurable'.mk f hfm =ᵐ[Measure.trim μ hm] AEStronglyMeasurable'.mk g hgm
[PROOFSTEP]
have hf_mk_int_finite : ∀ s, MeasurableSet[m] s → μ.trim hm s < ∞ → @IntegrableOn _ _ m _ (hfm.mk f) s (μ.trim hm) :=
  by
  intro s hs hμs
  rw [trim_measurableSet_eq hm hs] at hμs
  unfold IntegrableOn
  rw [restrict_trim hm _ hs]
  refine' Integrable.trim hm _ hfm.stronglyMeasurable_mk
  exact Integrable.congr (hf_int_finite s hs hμs) (ae_restrict_of_ae hfm.ae_eq_mk)
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
[PROOFSTEP]
intro s hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim μ hm) s < ⊤
⊢ IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
[PROOFSTEP]
rw [trim_measurableSet_eq hm hs] at hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
[PROOFSTEP]
unfold IntegrableOn
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ Integrable (AEStronglyMeasurable'.mk f hfm)
[PROOFSTEP]
rw [restrict_trim hm _ hs]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ Integrable (AEStronglyMeasurable'.mk f hfm)
[PROOFSTEP]
refine' Integrable.trim hm _ hfm.stronglyMeasurable_mk
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ Integrable (AEStronglyMeasurable'.mk f hfm)
[PROOFSTEP]
exact Integrable.congr (hf_int_finite s hs hμs) (ae_restrict_of_ae hfm.ae_eq_mk)
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
⊢ AEStronglyMeasurable'.mk f hfm =ᵐ[Measure.trim μ hm] AEStronglyMeasurable'.mk g hgm
[PROOFSTEP]
have hg_mk_int_finite : ∀ s, MeasurableSet[m] s → μ.trim hm s < ∞ → @IntegrableOn _ _ m _ (hgm.mk g) s (μ.trim hm) :=
  by
  intro s hs hμs
  rw [trim_measurableSet_eq hm hs] at hμs
  unfold IntegrableOn
  rw [restrict_trim hm _ hs]
  refine' Integrable.trim hm _ hgm.stronglyMeasurable_mk
  exact Integrable.congr (hg_int_finite s hs hμs) (ae_restrict_of_ae hgm.ae_eq_mk)
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk g hgm) s
[PROOFSTEP]
intro s hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim μ hm) s < ⊤
⊢ IntegrableOn (AEStronglyMeasurable'.mk g hgm) s
[PROOFSTEP]
rw [trim_measurableSet_eq hm hs] at hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ IntegrableOn (AEStronglyMeasurable'.mk g hgm) s
[PROOFSTEP]
unfold IntegrableOn
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ Integrable (AEStronglyMeasurable'.mk g hgm)
[PROOFSTEP]
rw [restrict_trim hm _ hs]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ Integrable (AEStronglyMeasurable'.mk g hgm)
[PROOFSTEP]
refine' Integrable.trim hm _ hgm.stronglyMeasurable_mk
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ Integrable (AEStronglyMeasurable'.mk g hgm)
[PROOFSTEP]
exact Integrable.congr (hg_int_finite s hs hμs) (ae_restrict_of_ae hgm.ae_eq_mk)
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk g hgm) s
⊢ AEStronglyMeasurable'.mk f hfm =ᵐ[Measure.trim μ hm] AEStronglyMeasurable'.mk g hgm
[PROOFSTEP]
have hfg_mk_eq :
  ∀ s : Set α,
    MeasurableSet[m] s → μ.trim hm s < ∞ → ∫ x in s, hfm.mk f x ∂μ.trim hm = ∫ x in s, hgm.mk g x ∂μ.trim hm :=
  by
  intro s hs hμs
  rw [trim_measurableSet_eq hm hs] at hμs
  rw [restrict_trim hm _ hs, ← integral_trim hm hfm.stronglyMeasurable_mk, ← integral_trim hm hgm.stronglyMeasurable_mk,
    integral_congr_ae (ae_restrict_of_ae hfm.ae_eq_mk.symm), integral_congr_ae (ae_restrict_of_ae hgm.ae_eq_mk.symm)]
  exact hfg_eq s hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk g hgm) s
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ↑↑(Measure.trim μ hm) s < ⊤ →
        ∫ (x : α) in s, AEStronglyMeasurable'.mk f hfm x ∂Measure.trim μ hm =
          ∫ (x : α) in s, AEStronglyMeasurable'.mk g hgm x ∂Measure.trim μ hm
[PROOFSTEP]
intro s hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk g hgm) s
s : Set α
hs : MeasurableSet s
hμs : ↑↑(Measure.trim μ hm) s < ⊤
⊢ ∫ (x : α) in s, AEStronglyMeasurable'.mk f hfm x ∂Measure.trim μ hm =
    ∫ (x : α) in s, AEStronglyMeasurable'.mk g hgm x ∂Measure.trim μ hm
[PROOFSTEP]
rw [trim_measurableSet_eq hm hs] at hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk g hgm) s
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ∫ (x : α) in s, AEStronglyMeasurable'.mk f hfm x ∂Measure.trim μ hm =
    ∫ (x : α) in s, AEStronglyMeasurable'.mk g hgm x ∂Measure.trim μ hm
[PROOFSTEP]
rw [restrict_trim hm _ hs, ← integral_trim hm hfm.stronglyMeasurable_mk, ← integral_trim hm hgm.stronglyMeasurable_mk,
  integral_congr_ae (ae_restrict_of_ae hfm.ae_eq_mk.symm), integral_congr_ae (ae_restrict_of_ae hgm.ae_eq_mk.symm)]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk g hgm) s
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ∫ (a : α) in s, f a ∂μ = ∫ (a : α) in s, g a ∂μ
[PROOFSTEP]
exact hfg_eq s hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hg_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn g s
hfg_eq : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable' m f μ
hgm : AEStronglyMeasurable' m g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk f hfm) s
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → ↑↑(Measure.trim μ hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable'.mk g hgm) s
hfg_mk_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      ↑↑(Measure.trim μ hm) s < ⊤ →
        ∫ (x : α) in s, AEStronglyMeasurable'.mk f hfm x ∂Measure.trim μ hm =
          ∫ (x : α) in s, AEStronglyMeasurable'.mk g hgm x ∂Measure.trim μ hm
⊢ AEStronglyMeasurable'.mk f hfm =ᵐ[Measure.trim μ hm] AEStronglyMeasurable'.mk g hgm
[PROOFSTEP]
exact ae_eq_of_forall_set_integral_eq_of_sigmaFinite hf_mk_int_finite hg_mk_int_finite hfg_mk_eq
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ ∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
[PROOFSTEP]
rw [integral_norm_eq_pos_sub_neg hgi, integral_norm_eq_pos_sub_neg hfi]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ ∫ (x : α) in {x | 0 ≤ g x}, g x ∂Measure.restrict μ s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂Measure.restrict μ s ≤
    ∫ (x : α) in {x | 0 ≤ f x}, f x ∂Measure.restrict μ s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂Measure.restrict μ s
[PROOFSTEP]
have h_meas_nonneg_g : MeasurableSet[m] {x | 0 ≤ g x} := (@stronglyMeasurable_const _ _ m _ _).measurableSet_le hg
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
⊢ ∫ (x : α) in {x | 0 ≤ g x}, g x ∂Measure.restrict μ s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂Measure.restrict μ s ≤
    ∫ (x : α) in {x | 0 ≤ f x}, f x ∂Measure.restrict μ s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂Measure.restrict μ s
[PROOFSTEP]
have h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x} := stronglyMeasurable_const.measurableSet_le hf
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
⊢ ∫ (x : α) in {x | 0 ≤ g x}, g x ∂Measure.restrict μ s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂Measure.restrict μ s ≤
    ∫ (x : α) in {x | 0 ≤ f x}, f x ∂Measure.restrict μ s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂Measure.restrict μ s
[PROOFSTEP]
have h_meas_nonpos_g : MeasurableSet[m] {x | g x ≤ 0} := hg.measurableSet_le (@stronglyMeasurable_const _ _ m _ _)
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
⊢ ∫ (x : α) in {x | 0 ≤ g x}, g x ∂Measure.restrict μ s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂Measure.restrict μ s ≤
    ∫ (x : α) in {x | 0 ≤ f x}, f x ∂Measure.restrict μ s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂Measure.restrict μ s
[PROOFSTEP]
have h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0} := hf.measurableSet_le stronglyMeasurable_const
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | 0 ≤ g x}, g x ∂Measure.restrict μ s - ∫ (x : α) in {x | g x ≤ 0}, g x ∂Measure.restrict μ s ≤
    ∫ (x : α) in {x | 0 ≤ f x}, f x ∂Measure.restrict μ s - ∫ (x : α) in {x | f x ≤ 0}, f x ∂Measure.restrict μ s
[PROOFSTEP]
refine' sub_le_sub _ _
[GOAL]
case refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | 0 ≤ g x}, g x ∂Measure.restrict μ s ≤ ∫ (x : α) in {x | 0 ≤ f x}, f x ∂Measure.restrict μ s
[PROOFSTEP]
rw [Measure.restrict_restrict (hm _ h_meas_nonneg_g), Measure.restrict_restrict h_meas_nonneg_f,
  hgf _ (@MeasurableSet.inter α m _ _ h_meas_nonneg_g hs)
    ((measure_mono (Set.inter_subset_right _ _)).trans_lt (lt_top_iff_ne_top.mpr hμs)),
  ← Measure.restrict_restrict (hm _ h_meas_nonneg_g), ← Measure.restrict_restrict h_meas_nonneg_f]
[GOAL]
case refine'_1
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | 0 ≤ g x}, f x ∂Measure.restrict μ s ≤ ∫ (x : α) in {x | 0 ≤ f x}, f x ∂Measure.restrict μ s
[PROOFSTEP]
exact set_integral_le_nonneg (hm _ h_meas_nonneg_g) hf hfi
[GOAL]
case refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | f x ≤ 0}, f x ∂Measure.restrict μ s ≤ ∫ (x : α) in {x | g x ≤ 0}, g x ∂Measure.restrict μ s
[PROOFSTEP]
rw [Measure.restrict_restrict (hm _ h_meas_nonpos_g), Measure.restrict_restrict h_meas_nonpos_f,
  hgf _ (@MeasurableSet.inter α m _ _ h_meas_nonpos_g hs)
    ((measure_mono (Set.inter_subset_right _ _)).trans_lt (lt_top_iff_ne_top.mpr hμs)),
  ← Measure.restrict_restrict (hm _ h_meas_nonpos_g), ← Measure.restrict_restrict h_meas_nonpos_f]
[GOAL]
case refine'_2
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | f x ≤ 0}, f x ∂Measure.restrict μ s ≤ ∫ (x : α) in {x | g x ≤ 0}, f x ∂Measure.restrict μ s
[PROOFSTEP]
exact set_integral_nonpos_le (hm _ h_meas_nonpos_g) hf hfi
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ ∫⁻ (x : α) in s, ↑‖g x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ
[PROOFSTEP]
rw [← ofReal_integral_norm_eq_lintegral_nnnorm hfi, ← ofReal_integral_norm_eq_lintegral_nnnorm hgi,
  ENNReal.ofReal_le_ofReal_iff]
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ ∫ (x : α) in s, ‖g x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
[PROOFSTEP]
exact integral_norm_le_of_forall_fin_meas_integral_eq hm hf hfi hg hgi hgf hs hμs
[GOAL]
α : Type u_1
E' : Type u_2
F' : Type u_3
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
inst✝⁵ : CompleteSpace E'
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : CompleteSpace F'
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s
hg : StronglyMeasurable g
hgi : IntegrableOn g s
hgf : ∀ (t : Set α), MeasurableSet t → ↑↑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ 0 ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
[PROOFSTEP]
exact integral_nonneg fun x => norm_nonneg _