Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

chore(measure_theory/function/strongly_measurable): use expand_exists for exists_set_sigma_finite #15718

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

chore(measure_theory/function/strongly_measurable): use expand_exists for exists_set_sigma_finite #15718

Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
d0e3a03
exists_set_sigma_finite
RemyDegenne Jul 27, 2022
c251f78
restore protected attribute
RemyDegenne Jul 27, 2022
7ea9c7c
restore instance attribute
RemyDegenne Jul 27, 2022
36e194b
add docstring
RemyDegenne Jul 27, 2022
69a8b59
shorten names
RemyDegenne Jul 27, 2022
98e433e
docstring
RemyDegenne Jul 27, 2022
7b7bf23
remove variables, put them in the lemma
RemyDegenne Jul 27, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 12 additions & 16 deletions src/measure_theory/function/strongly_measurable.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ import measure_theory.integral.mean_inequalities
import topology.continuous_function.compact
import topology.metric_space.metrizable
import measure_theory.function.simple_func_dense
import tactic.expand_exists

/-!
# Strongly measurable and finitely strongly measurable functions
Expand Down Expand Up @@ -1780,9 +1781,14 @@ protected lemma inf [semilattice_inf β] [has_continuous_inf β]

end order

variables [has_zero β] [t2_space β]

lemma exists_set_sigma_finite (hf : ae_fin_strongly_measurable f μ) :
/-- For a `ae_fin_strongly_measurable` function `f`, there exists a measurable set `t` such that
`f =ᵐ[μ.restrict tᶜ] 0` and `sigma_finite (μ.restrict t)`. The attribute `expand_exists` creates a
def for the set and three lemmas for its properties. -/
@[expand_exists measure_theory.ae_fin_strongly_measurable.sigma_finite_set
measure_theory.ae_fin_strongly_measurable.measurable_set
measure_theory.ae_fin_strongly_measurable.ae_eq_zero_compl
measure_theory.ae_fin_strongly_measurable.sigma_finite_restrict]
lemma exists_set_sigma_finite [has_zero β] [t2_space β] (hf : ae_fin_strongly_measurable f μ) :
∃ t, measurable_set t ∧ f =ᵐ[μ.restrict tᶜ] 0 ∧ sigma_finite (μ.restrict t) :=
begin
rcases hf with ⟨g, hg, hfg⟩,
Expand All @@ -1794,20 +1800,10 @@ begin
end

/-- A measurable set `t` such that `f =ᵐ[μ.restrict tᶜ] 0` and `sigma_finite (μ.restrict t)`. -/
def sigma_finite_set (hf : ae_fin_strongly_measurable f μ) : set α :=
hf.exists_set_sigma_finite.some

protected lemma measurable_set (hf : ae_fin_strongly_measurable f μ) :
measurable_set hf.sigma_finite_set :=
hf.exists_set_sigma_finite.some_spec.1

lemma ae_eq_zero_compl (hf : ae_fin_strongly_measurable f μ) :
f =ᵐ[μ.restrict hf.sigma_finite_setᶜ] 0 :=
hf.exists_set_sigma_finite.some_spec.2.1
add_decl_doc sigma_finite_set

instance sigma_finite_restrict (hf : ae_fin_strongly_measurable f μ) :
sigma_finite (μ.restrict hf.sigma_finite_set) :=
hf.exists_set_sigma_finite.some_spec.2.2
attribute [protected] ae_fin_strongly_measurable.measurable_set
attribute [instance] sigma_finite_restrict

end ae_fin_strongly_measurable

Expand Down