α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
⊢ (∫⁻ (x : α), f x ∂μ) ≤ C
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
⊢ (∫⁻ (x : α), f x ∂μ) ≤ C
let f' := hf_meas.mk f
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
hf' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f' x ∂μ) ≤ C
⊢ (∫⁻ (x : α), f x ∂μ) ≤ C
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
⊢ (∫⁻ (x : α), f x ∂μ) ≤ C
have hf' : ∀ s, MeasurableSet[m] s → μ s ≠ ∞ → (∫⁻ x in s, f' x ∂μ) ≤ C := by
  refine' fun s hs hμs => (le_of_eq _).trans (hf s hs hμs)
  refine' lintegral_congr_ae (ae_restrict_of_ae (hf_meas.ae_eq_mk.mono fun x hx => _))
  dsimp only
  rw [hx]
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
hf' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f' x ∂μ) ≤ C
⊢ (∫⁻ (a : α), AEMeasurable.mk f hf_meas a ∂μ) ≤ C
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
hf' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f' x ∂μ) ≤ C
⊢ (∫⁻ (x : α), f x ∂μ) ≤ C
rw [lintegral_congr_ae hf_meas.ae_eq_mk]
no goals
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
hf' : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f' x ∂μ) ≤ C
⊢ (∫⁻ (a : α), AEMeasurable.mk f hf_meas a ∂μ) ≤ C
exact lintegral_le_of_forall_fin_meas_le_of_measurable hm C hf_meas.measurable_mk hf'
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ (∫⁻ (x : α) in s, f' x ∂μ) = ∫⁻ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f' x ∂μ) ≤ C
refine' fun s hs hμs => (le_of_eq _).trans (hf s hs hμs)
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : α
hx : f x = AEMeasurable.mk f hf_meas x
⊢ (fun x => f' x) x = (fun x => f x) x
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ (∫⁻ (x : α) in s, f' x ∂μ) = ∫⁻ (x : α) in s, f x ∂μ
refine' lintegral_congr_ae (ae_restrict_of_ae (hf_meas.ae_eq_mk.mono fun x hx => _))
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : α
hx : f x = AEMeasurable.mk f hf_meas x
⊢ AEMeasurable.mk f hf_meas x = f x
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : α
hx : f x = AEMeasurable.mk f hf_meas x
⊢ (fun x => f' x) x = (fun x => f x) x
dsimp only
no goals
α : Type u_1
β : Type ?u.1830921
γ : Type ?u.1830924
δ : Type ?u.1830927
m m0 : MeasurableSpace α
E : Type ?u.1830936
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : AEMeasurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf_meas
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : α
hx : f x = AEMeasurable.mk f hf_meas x
⊢ AEMeasurable.mk f hf_meas x = f x
rw [hx]