α : Type u_1
β : Type ?u.985899
γ : Type ?u.985902
δ : Type ?u.985905
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hμ : ¬↑↑μ univ = 0
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ (∫⁻ (x : α), f x ∂μ) < ∫⁻ (x : α), g x ∂μ
α : Type u_1
β : Type ?u.985899
γ : Type ?u.985902
δ : Type ?u.985905
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hμ : μ ≠ 0
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ (∫⁻ (x : α), f x ∂μ) < ∫⁻ (x : α), g x ∂μ
rw [Ne.def, ← Measure.measure_univ_eq_zero] at hμ
α : Type u_1
β : Type ?u.985899
γ : Type ?u.985902
δ : Type ?u.985905
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hμ : ¬↑↑μ univ = 0
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ → f x < g x
α : Type u_1
β : Type ?u.985899
γ : Type ?u.985902
δ : Type ?u.985905
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hμ : ¬↑↑μ univ = 0
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ (∫⁻ (x : α), f x ∂μ) < ∫⁻ (x : α), g x ∂μ
refine' lintegral_strict_mono_of_ae_le_of_ae_lt_on hg hfi (ae_le_of_ae_lt h) hμ _
no goals
α : Type u_1
β : Type ?u.985899
γ : Type ?u.985902
δ : Type ?u.985905
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hμ : ¬↑↑μ univ = 0
hg : AEMeasurable g
hfi : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ → f x < g x
simpa using h