α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
⊢ (fun a => max (f a) (g a)) ∈ measurableLE μ ν
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
⊢ (fun a => f a ⊔ g a) ∈ measurableLE μ ν
simp_rw [ENNReal.sup_eq_max]
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (x : α) in A, (fun a => max (f a) (g a)) x ∂μ) ≤ ↑↑ν A
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
⊢ (fun a => max (f a) (g a)) ∈ measurableLE μ ν
refine' ⟨Measurable.max hf.1 hg.1, fun A hA => _⟩
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
⊢ (∫⁻ (x : α) in A, (fun a => max (f a) (g a)) x ∂μ) ≤ ↑↑ν A
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
⊢ (∫⁻ (x : α) in A, (fun a => max (f a) (g a)) x ∂μ) ≤ ↑↑ν A
have h₁ := hA.inter (measurableSet_le hf.1 hg.1)
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ (∫⁻ (x : α) in A, (fun a => max (f a) (g a)) x ∂μ) ≤ ↑↑ν A
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
⊢ (∫⁻ (x : α) in A, (fun a => max (f a) (g a)) x ∂μ) ≤ ↑↑ν A
have h₂ := hA.inter (measurableSet_lt hg.1 hf.1)
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ((∫⁻ (x : α) in A ∩ {x | f x ≤ g x}, g x ∂μ) + ∫⁻ (x : α) in A ∩ {x | g x < f x}, f x ∂μ) ≤ ↑↑ν A
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ (∫⁻ (x : α) in A, (fun a => max (f a) (g a)) x ∂μ) ≤ ↑↑ν A
rw [set_lintegral_max hf.1 hg.1]
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ↑↑ν (A ∩ {a | f a ≤ g a}) + ↑↑ν (A ∩ {a | g a < f a}) = ↑↑ν A
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ((∫⁻ (x : α) in A ∩ {x | f x ≤ g x}, g x ∂μ) + ∫⁻ (x : α) in A ∩ {x | g x < f x}, f x ∂μ) ≤ ↑↑ν A
refine' (add_le_add (hg.2 _ h₁) (hf.2 _ h₂)).trans_eq _
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ↑↑ν (A ∩ {a | f a ≤ g a}) + ↑↑ν (A \ {a | f a ≤ g a}) = ↑↑ν A
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ↑↑ν (A ∩ {a | f a ≤ g a}) + ↑↑ν (A ∩ {a | g a < f a}) = ↑↑ν A
simp only [← not_le, ← compl_setOf, ← diff_eq]
no goals
α : Type u_1
β : Type ?u.88456
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hf : f ∈ measurableLE μ ν
hg : g ∈ measurableLE μ ν
A : Set α
hA : MeasurableSet A
h₁ : MeasurableSet (A ∩ {a | f a ≤ g a})
h₂ : MeasurableSet (A ∩ {a | g a < f a})
⊢ ↑↑ν (A ∩ {a | f a ≤ g a}) + ↑↑ν (A \ {a | f a ≤ g a}) = ↑↑ν A
exact measure_inter_add_diff _ (measurableSet_le hf.1 hg.1)