α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ essSup (indicator s f) μ ≤ essSup f (Measure.restrict μ s)
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ essSup (indicator s f) μ = essSup f (Measure.restrict μ s)
refine'
  le_antisymm _
    (limsSup_le_limsSup_of_le (map_restrict_ae_le_map_indicator_ae hs)
      (by isBoundedDefault) (by isBoundedDefault) )
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᶠ (n : β) in map f (Measure.ae (Measure.restrict μ s)), n ≤ c
⊢ ∀ᶠ (n : β) in map (indicator s f) (Measure.ae μ), n ≤ c
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ essSup (indicator s f) μ ≤ essSup f (Measure.restrict μ s)
refine' limsSup_le_limsSup (by isBoundedDefault) (by isBoundedDefault) (fun c h_restrict_le => _)
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (a : α) ∂Measure.restrict μ s, f a ≤ c
⊢ ∀ᵐ (a : α) ∂μ, indicator s f a ≤ c
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᶠ (n : β) in map f (Measure.ae (Measure.restrict μ s)), n ≤ c
⊢ ∀ᶠ (n : β) in map (indicator s f) (Measure.ae μ), n ≤ c
rw [eventually_map] at h_restrict_le⊢
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∀ᵐ (a : α) ∂μ, indicator s f a ≤ c
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (a : α) ∂Measure.restrict μ s, f a ≤ c
⊢ ∀ᵐ (a : α) ∂μ, indicator s f a ≤ c
rw [ae_restrict_iff' hs] at h_restrict_le
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
x : α
hxc : x ∈ s → f x ≤ c
⊢ indicator s f x ≤ c
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
⊢ ∀ᵐ (a : α) ∂μ, indicator s f a ≤ c
refine' h_restrict_le.mono fun x hxc => _
case pos
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
x : α
hxc : x ∈ s → f x ≤ c
hxs : x ∈ s
⊢ indicator s f x ≤ c

case neg
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
x : α
hxc : x ∈ s → f x ≤ c
hxs : ¬x ∈ s
⊢ indicator s f x ≤ c
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
x : α
hxc : x ∈ s → f x ≤ c
⊢ indicator s f x ≤ c
by_cases hxs : x ∈ s
no goals
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map f (Measure.ae (Measure.restrict μ s)))
isBoundedDefault
no goals
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ IsBounded (fun x x_1 => x ≤ x_1) (map (indicator s f) (Measure.ae μ))
isBoundedDefault
no goals
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map (indicator s f) (Measure.ae μ))
isBoundedDefault
no goals
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ IsBounded (fun x x_1 => x ≤ x_1) (map f (Measure.ae (Measure.restrict μ s)))
isBoundedDefault
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
x : α
hx : 0 ≤ f x ∧ f x ≤ c
⊢ 0 ≤ c

α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ x, 0 ≤ f x ∧ f x ≤ c
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ 0 ≤ c
rsuffices ⟨x, hx⟩ : ∃ x, 0 ≤ f x ∧ f x ≤ c
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ x, 0 ≤ f x ∧ f x ≤ c
case intro
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
x : α
hx : 0 ≤ f x ∧ f x ≤ c
⊢ 0 ≤ c

α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ x, 0 ≤ f x ∧ f x ≤ c
exact hx.1.trans hx.2
case refine'_1
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ Filter α

case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ᶠ (x : α) in ?refine'_1, 0 ≤ f x ∧ f x ≤ c
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ x, 0 ≤ f x ∧ f x ≤ c
refine' Frequently.exists _
case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ᵐ (x : α) ∂μ, 0 ≤ f x ∧ f x ≤ c
case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ᵐ (x : α) ∂μ, 0 ≤ f x ∧ f x ≤ c
rw [EventuallyLE, ae_restrict_iff' hs] at hf
case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs' : ∃ᵐ (x : α) ∂μ, x ∈ s
⊢ ∃ᵐ (x : α) ∂μ, 0 ≤ f x ∧ f x ≤ c
case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ᵐ (x : α) ∂μ, 0 ≤ f x ∧ f x ≤ c
have hs' : ∃ᵐ x ∂μ, x ∈ s := by
  contrapose! hs_not_null
  rw [not_frequently, ae_iff] at hs_not_null
  suffices { a : α | ¬a ∉ s } = s by rwa [← this]
  simp
case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs' : ∃ᵐ (x : α) ∂μ, x ∈ s
x : α
hxs_imp_c : x ∈ s → f x ≤ c
hxf_nonneg : x ∈ s → OfNat.ofNat 0 x ≤ f x
hxs : x ∈ s
⊢ 0 ≤ f x ∧ f x ≤ c
case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs' : ∃ᵐ (x : α) ∂μ, x ∈ s
⊢ ∃ᵐ (x : α) ∂μ, 0 ≤ f x ∧ f x ≤ c
refine' hs'.mp (hf.mp (h_restrict_le.mono fun x hxs_imp_c hxf_nonneg hxs => _))
case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs' : ∃ᵐ (x : α) ∂μ, x ∈ s
x : α
hxs_imp_c : x ∈ s → f x ≤ c
hxf_nonneg : x ∈ s → 0 ≤ f x
hxs : x ∈ s
⊢ 0 ≤ f x ∧ f x ≤ c
case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs' : ∃ᵐ (x : α) ∂μ, x ∈ s
x : α
hxs_imp_c : x ∈ s → f x ≤ c
hxf_nonneg : x ∈ s → OfNat.ofNat 0 x ≤ f x
hxs : x ∈ s
⊢ 0 ≤ f x ∧ f x ≤ c
rw [Pi.zero_apply] at hxf_nonneg
no goals
case refine'_2
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs' : ∃ᵐ (x : α) ∂μ, x ∈ s
x : α
hxs_imp_c : x ∈ s → f x ≤ c
hxf_nonneg : x ∈ s → 0 ≤ f x
hxs : x ∈ s
⊢ 0 ≤ f x ∧ f x ≤ c
exact ⟨hxf_nonneg hxs, hxs_imp_c hxs⟩
no goals
case refine'_1
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ Filter α
exact μ.ae
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ¬∃ᵐ (x : α) ∂μ, x ∈ s
⊢ ↑↑μ s = 0
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ᵐ (x : α) ∂μ, x ∈ s
contrapose! hs_not_null
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ↑↑μ {a | ¬¬a ∈ s} = 0
⊢ ↑↑μ s = 0
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ¬∃ᵐ (x : α) ∂μ, x ∈ s
⊢ ↑↑μ s = 0
rw [not_frequently, ae_iff] at hs_not_null
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ↑↑μ {a | ¬¬a ∈ s} = 0
⊢ {a | ¬¬a ∈ s} = s
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ↑↑μ {a | ¬¬a ∈ s} = 0
⊢ ↑↑μ s = 0
suffices { a : α | ¬a ∉ s } = s by rwa [← this]
no goals
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ↑↑μ {a | ¬¬a ∈ s} = 0
⊢ {a | ¬¬a ∈ s} = s
simp
no goals
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ↑↑μ {a | ¬¬a ∈ s} = 0
this : {a | ¬¬a ∈ s} = s
⊢ ↑↑μ s = 0
rwa [← this]
no goals
case pos
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
x : α
hxc : x ∈ s → f x ≤ c
hxs : x ∈ s
⊢ indicator s f x ≤ c
simpa [hxs] using hxc hxs
no goals
case neg
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
x : α
hxc : x ∈ s → f x ≤ c
hxs : ¬x ∈ s
⊢ indicator s f x ≤ c
simpa [hxs] using hc