α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
⊢ (∫⁻ (x : α), f x ∂μ) ≤ C
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
⊢ (∫⁻ (x : α), f x ∂μ) ≤ C
have : (∫⁻ x in univ, f x ∂μ) = ∫⁻ x, f x ∂μ := by simp only [Measure.restrict_univ]
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
⊢ (∫⁻ (x : α) in univ, f x ∂μ) ≤ C
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
⊢ (∫⁻ (x : α), f x ∂μ) ≤ C
rw [← this]
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ (∫⁻ (x : α) in ⋃ (n : ℕ), S n, f x ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
⊢ (∫⁻ (x : α) in univ, f x ∂μ) ≤ C
refine' univ_le_of_forall_fin_meas_le hm C hf fun S hS_meas hS_mono => _
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ (∫⁻ (a : α), indicator (⋃ (n : ℕ), S n) (fun x => f x) a ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ

case hs
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ MeasurableSet (⋃ (n : ℕ), S n)
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ (∫⁻ (x : α) in ⋃ (n : ℕ), S n, f x ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ
rw [← lintegral_indicator]
case hs
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ MeasurableSet (⋃ (n : ℕ), S n)

α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ (∫⁻ (a : α), indicator (⋃ (n : ℕ), S n) (fun x => f x) a ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ (∫⁻ (a : α), indicator (⋃ (n : ℕ), S n) (fun x => f x) a ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ

case hs
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ MeasurableSet (⋃ (n : ℕ), S n)
swap
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
⊢ (∫⁻ (a : α), indicator (⋃ (n : ℕ), S n) (fun x => f x) a ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ (∫⁻ (a : α), indicator (⋃ (n : ℕ), S n) (fun x => f x) a ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ
have h_integral_indicator : (⨆ n, ∫⁻ x in S n, f x ∂μ) = ⨆ n, ∫⁻ x, (S n).indicator f x ∂μ := by
  congr
  ext1 n
  rw [lintegral_indicator _ (hm _ (hS_meas n))]
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
⊢ (∫⁻ (a : α), indicator (⋃ (n : ℕ), S n) (fun x => f x) a ∂μ) ≤ ∫⁻ (a : α), ⨆ (n : ℕ), indicator (S n) f a ∂μ

case hf
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
⊢ ∀ (n : ℕ), Measurable fun x => indicator (S n) f x

case h_mono
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
⊢ Monotone fun n x => indicator (S n) f x
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
⊢ (∫⁻ (a : α), indicator (⋃ (n : ℕ), S n) (fun x => f x) a ∂μ) ≤ ⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ
rw [h_integral_indicator, ← lintegral_iSup]
no goals
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
⊢ (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
simp only [Measure.restrict_univ]
no goals
case hs
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ MeasurableSet (⋃ (n : ℕ), S n)
exact hm (⋃ n, S n) (@MeasurableSet.iUnion _ _ m _ _ hS_meas)
case e_s
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ (fun n => ∫⁻ (x : α) in S n, f x ∂μ) = fun n => ∫⁻ (x : α), indicator (S n) f x ∂μ
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
congr
case e_s.h
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
n : ℕ
⊢ (∫⁻ (x : α) in S n, f x ∂μ) = ∫⁻ (x : α), indicator (S n) f x ∂μ
case e_s
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
⊢ (fun n => ∫⁻ (x : α) in S n, f x ∂μ) = fun n => ∫⁻ (x : α), indicator (S n) f x ∂μ
ext1 n
no goals
case e_s.h
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
n : ℕ
⊢ (∫⁻ (x : α) in S n, f x ∂μ) = ∫⁻ (x : α), indicator (S n) f x ∂μ
rw [lintegral_indicator _ (hm _ (hS_meas n))]
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
⊢ indicator (⋃ (n : ℕ), S n) (fun x => f x) x = ⨆ (n : ℕ), indicator (S n) f x
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
⊢ (∫⁻ (a : α), indicator (⋃ (n : ℕ), S n) (fun x => f x) a ∂μ) ≤ ∫⁻ (a : α), ⨆ (n : ℕ), indicator (S n) f a ∂μ
refine' le_of_eq (lintegral_congr fun x => _)
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
⊢ (if x ∈ ⋃ (n : ℕ), S n then f x else 0) = ⨆ (n : ℕ), if x ∈ S n then f x else 0
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
⊢ indicator (⋃ (n : ℕ), S n) (fun x => f x) x = ⨆ (n : ℕ), indicator (S n) f x
simp_rw [indicator_apply]
case pos
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
⊢ (if x ∈ ⋃ (n : ℕ), S n then f x else 0) = ⨆ (n : ℕ), if x ∈ S n then f x else 0

case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ¬x ∈ iUnion S
⊢ (if x ∈ ⋃ (n : ℕ), S n then f x else 0) = ⨆ (n : ℕ), if x ∈ S n then f x else 0
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
⊢ (if x ∈ ⋃ (n : ℕ), S n then f x else 0) = ⨆ (n : ℕ), if x ∈ S n then f x else 0
by_cases hx_mem : x ∈ iUnion S
case pos
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
⊢ f x = ⨆ (n : ℕ), if x ∈ S n then f x else 0
case pos
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
⊢ (if x ∈ ⋃ (n : ℕ), S n then f x else 0) = ⨆ (n : ℕ), if x ∈ S n then f x else 0
simp only [hx_mem, if_true]
case pos.intro
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
n : ℕ
hxn : x ∈ S n
⊢ f x = ⨆ (n : ℕ), if x ∈ S n then f x else 0
case pos
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
⊢ f x = ⨆ (n : ℕ), if x ∈ S n then f x else 0
obtain ⟨n, hxn⟩ := mem_iUnion.mp hx_mem
case pos.intro.refine'_1
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
n : ℕ
hxn : x ∈ S n
⊢ f x ≤ if x ∈ S n then f x else 0

case pos.intro.refine'_2
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
n : ℕ
hxn : x ∈ S n
i : ℕ
⊢ (if x ∈ S i then f x else 0) ≤ f x
case pos.intro
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
n : ℕ
hxn : x ∈ S n
⊢ f x = ⨆ (n : ℕ), if x ∈ S n then f x else 0
refine' le_antisymm (_root_.trans _ (le_iSup _ n)) (iSup_le fun i => _)
no goals
case pos.intro.refine'_1
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
n : ℕ
hxn : x ∈ S n
⊢ f x ≤ if x ∈ S n then f x else 0
simp only [hxn, le_refl, if_true]
no goals
case pos.intro.refine'_2
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : x ∈ iUnion S
n : ℕ
hxn : x ∈ S n
i : ℕ
⊢ (if x ∈ S i then f x else 0) ≤ f x
by_cases hxi : x ∈ S i <;> simp [hxi]
case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ¬x ∈ iUnion S
⊢ 0 = ⨆ (n : ℕ), if x ∈ S n then f x else 0
case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ¬x ∈ iUnion S
⊢ (if x ∈ ⋃ (n : ℕ), S n then f x else 0) = ⨆ (n : ℕ), if x ∈ S n then f x else 0
simp only [hx_mem, if_false]
case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ¬∃ i, x ∈ S i
⊢ 0 = ⨆ (n : ℕ), if x ∈ S n then f x else 0
case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ¬x ∈ iUnion S
⊢ 0 = ⨆ (n : ℕ), if x ∈ S n then f x else 0
rw [mem_iUnion] at hx_mem
case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ∀ (i : ℕ), ¬x ∈ S i
⊢ 0 = ⨆ (n : ℕ), if x ∈ S n then f x else 0
case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ¬∃ i, x ∈ S i
⊢ 0 = ⨆ (n : ℕ), if x ∈ S n then f x else 0
push_neg  at hx_mem
case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ∀ (i : ℕ), ¬x ∈ S i
n : ℕ
⊢ (if x ∈ S n then f x else 0) ≤ 0
case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ∀ (i : ℕ), ¬x ∈ S i
⊢ 0 = ⨆ (n : ℕ), if x ∈ S n then f x else 0
refine' le_antisymm (zero_le _) (iSup_le fun n => _)
no goals
case neg
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
x : α
hx_mem : ∀ (i : ℕ), ¬x ∈ S i
n : ℕ
⊢ (if x ∈ S n then f x else 0) ≤ 0
simp only [hx_mem n, if_false, nonpos_iff_eq_zero]
no goals
case hf
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
⊢ ∀ (n : ℕ), Measurable fun x => indicator (S n) f x
exact fun n => hf_meas.indicator (hm _ (hS_meas n))
case h_mono
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
⊢ (fun n x => indicator (S n) f x) n₁ a ≤ (fun n x => indicator (S n) f x) n₂ a
case h_mono
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
⊢ Monotone fun n x => indicator (S n) f x
intro n₁ n₂ hn₁₂ a
case h_mono
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
⊢ (if a ∈ S n₁ then f a else 0) ≤ if a ∈ S n₂ then f a else 0
case h_mono
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
⊢ (fun n x => indicator (S n) f x) n₁ a ≤ (fun n x => indicator (S n) f x) n₂ a
simp_rw [indicator_apply]
case h_mono.inl.inl
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
h : a ∈ S n₁
h_1 : a ∈ S n₂
⊢ f a ≤ f a

case h_mono.inl.inr
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
h : a ∈ S n₁
h_1 : ¬a ∈ S n₂
⊢ f a ≤ 0

case h_mono.inr.inl
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
h : ¬a ∈ S n₁
h✝ : a ∈ S n₂
⊢ 0 ≤ f a

case h_mono.inr.inr
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
h : ¬a ∈ S n₁
h✝ : ¬a ∈ S n₂
⊢ 0 ≤ 0
case h_mono
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
⊢ (if a ∈ S n₁ then f a else 0) ≤ if a ∈ S n₂ then f a else 0
split_ifs with h h_1
no goals
case h_mono.inl.inl
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
h : a ∈ S n₁
h_1 : a ∈ S n₂
⊢ f a ≤ f a
exact le_rfl
no goals
case h_mono.inl.inr
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
h : a ∈ S n₁
h_1 : ¬a ∈ S n₂
⊢ f a ≤ 0
exact absurd (mem_of_mem_of_subset h (hS_mono hn₁₂)) h_1
no goals
case h_mono.inr.inl
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
h : ¬a ∈ S n₁
h✝ : a ∈ S n₂
⊢ 0 ≤ f a
exact zero_le _
no goals
case h_mono.inr.inr
α : Type u_1
β : Type ?u.1825244
γ : Type ?u.1825247
δ : Type ?u.1825250
m m0 : MeasurableSpace α
E : Type ?u.1825259
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (Measure.trim μ hm)
C : ℝ≥0∞
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≠ ⊤ → (∫⁻ (x : α) in s, f x ∂μ) ≤ C
this : (∫⁻ (x : α) in univ, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
S : ℕ → Set α
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
hS_mono : Monotone S
h_integral_indicator : (⨆ (n : ℕ), ∫⁻ (x : α) in S n, f x ∂μ) = ⨆ (n : ℕ), ∫⁻ (x : α), indicator (S n) f x ∂μ
n₁ n₂ : ℕ
hn₁₂ : n₁ ≤ n₂
a : α
h : ¬a ∈ S n₁
h✝ : ¬a ∈ S n₂
⊢ 0 ≤ 0
exact le_rfl