α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ 0 < ↑↑μ ((support fun a => f a - R) ∩ {x | R < f x})

case hf
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ 0 ≤ᵐ[Measure.restrict μ {x | R < f x}] fun a => f a - R

case hfi
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ IntegrableOn (fun a => f a - R) {x | R < f x}
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ ENNReal.toReal (↑↑μ {x | R < f x}) * R < ∫ (x : α) in {x | R < f x}, f x ∂μ
rw [← sub_pos, ← smul_eq_mul, ← set_integral_const, ← integral_sub hfint this,
  set_integral_pos_iff_support_of_nonneg_ae]
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
⊢ (∫⁻ (a : α) in {x | R < f x}, ↑‖(fun x => R) a‖₊ ∂μ) ≤ ∫⁻ (a : α) in {x | R < f x}, ↑‖f a‖₊ ∂μ
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
⊢ IntegrableOn (fun x => R) {x | R < f x}
refine' ⟨aestronglyMeasurable_const, lt_of_le_of_lt _ hfint.2⟩
case refine'_1
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
⊢ Measurable fun a => (fun x => R) a

case refine'_2
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
x : α
hx : x ∈ {x | R < f x}
⊢ ↑‖(fun x => R) x‖₊ ≤ ↑‖f x‖₊
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
⊢ (∫⁻ (a : α) in {x | R < f x}, ↑‖(fun x => R) a‖₊ ∂μ) ≤ ∫⁻ (a : α) in {x | R < f x}, ↑‖f a‖₊ ∂μ
refine'
  set_lintegral_mono (Measurable.nnnorm _).coe_nnreal_ennreal hfm.nnnorm.coe_nnreal_ennreal
    fun x hx => _
no goals
case refine'_1
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
⊢ Measurable fun a => (fun x => R) a
exact measurable_const
case refine'_2
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
x : α
hx : x ∈ {x | R < f x}
⊢ { val := R, property := hR } ≤ { val := f x, property := (_ : 0 ≤ f x) }
case refine'_2
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
x : α
hx : x ∈ {x | R < f x}
⊢ ↑‖(fun x => R) x‖₊ ≤ ↑‖f x‖₊
simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR,
  Real.nnnorm_of_nonneg (hR.trans <| le_of_lt hx), Subtype.mk_le_mk]
no goals
case refine'_2
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
x : α
hx : x ∈ {x | R < f x}
⊢ { val := R, property := hR } ≤ { val := f x, property := (_ : 0 ≤ f x) }
exact le_of_lt hx
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : 0 < ↑↑μ {x | R < f x}
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ 0 < ↑↑μ ((support fun a => f a - R) ∩ {x | R < f x})
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ 0 < ↑↑μ ((support fun a => f a - R) ∩ {x | R < f x})
rw [← zero_lt_iff] at hμ
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : 0 < ↑↑μ {x | R < f x}
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ {x | R < f x} ⊆ support fun a => f a - R
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : 0 < ↑↑μ {x | R < f x}
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ 0 < ↑↑μ ((support fun a => f a - R) ∩ {x | R < f x})
rwa [Set.inter_eq_self_of_subset_right]
no goals
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : 0 < ↑↑μ {x | R < f x}
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ {x | R < f x} ⊆ support fun a => f a - R
exact fun x hx => Ne.symm (ne_of_lt <| sub_pos.2 hx)
case hf
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | R < f x}, OfNat.ofNat 0 x ≤ (fun a => f a - R) x
case hf
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ 0 ≤ᵐ[Measure.restrict μ {x | R < f x}] fun a => f a - R
change ∀ᵐ x ∂μ.restrict _, _
case hf
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | R < f x} → OfNat.ofNat 0 x ≤ (fun a => f a - R) x

case hf
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ MeasurableSet {x | OfNat.ofNat 0 x ≤ (fun a => f a - R) x}
case hf
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | R < f x}, OfNat.ofNat 0 x ≤ (fun a => f a - R) x
rw [ae_restrict_iff]
no goals
case hf
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | R < f x} → OfNat.ofNat 0 x ≤ (fun a => f a - R) x
exact eventually_of_forall fun x hx => sub_nonneg.2 <| le_of_lt hx
no goals
case hf
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ MeasurableSet {x | OfNat.ofNat 0 x ≤ (fun a => f a - R) x}
exact measurableSet_le measurable_zero (hfm.sub measurable_const)
no goals
case hfi
α : Type u_1
β : Type ?u.264063
E : Type ?u.264066
F : Type ?u.264069
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
R : ℝ
f : α → ℝ
hR : 0 ≤ R
hfm : Measurable f
hfint : IntegrableOn f {x | R < f x}
hμ : ↑↑μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x => R) {x | R < f x}
⊢ IntegrableOn (fun a => f a - R) {x | R < f x}
exact Integrable.sub hfint this