[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : HasCountableSeparatingOn X MeasurableSet s
f : α → α
g : α → X
h : QuasiErgodic f
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
refine exists_eventuallyEq_const_of_eventually_mem_of_forall_separating MeasurableSet hs ?_
[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : HasCountableSeparatingOn X MeasurableSet s
f : α → α
g : α → X
h : QuasiErgodic f
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∀ (U : Set X), MeasurableSet U → (∀ᵐ (x : α) ∂μ, g x ∈ U) ∨ ∀ᵐ (x : α) ∂μ, ¬g x ∈ U
[PROOFSTEP]
refine fun U hU ↦ h.ae_mem_or_ae_nmem₀ (s := g ⁻¹' U) (hgm hU) ?_b
[GOAL]
case _b
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : HasCountableSeparatingOn X MeasurableSet s
f : α → α
g : α → X
h : QuasiErgodic f
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g
hg_eq : g ∘ f =ᵐ[μ] g
U : Set X
hU : MeasurableSet U
⊢ f ⁻¹' (g ⁻¹' U) =ᵐ[μ] g ⁻¹' U
[PROOFSTEP]
refine (hg_eq.mono fun x hx ↦ ?_).set_eq
[GOAL]
case _b
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : HasCountableSeparatingOn X MeasurableSet s
f : α → α
g : α → X
h : QuasiErgodic f
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g
hg_eq : g ∘ f =ᵐ[μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
⊢ x ∈ f ⁻¹' (g ⁻¹' U) ↔ x ∈ g ⁻¹' U
[PROOFSTEP]
rw [← preimage_comp, mem_preimage, mem_preimage, hx]
[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
inst✝ : HasCountableSeparatingOn X MeasurableSet univ
f : α → α
g : α → X
h : PreErgodic f
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
⊢ f ⁻¹' (g ⁻¹' U) = g ⁻¹' U
[PROOFSTEP]
rw [← preimage_comp, hg_eq]
[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
borelize X
[GOAL]
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
rcases hgm.isSeparable_ae_range with ⟨t, ht, hgt⟩
[GOAL]
case intro.intro
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
haveI := ht.secondCountableTopology
[GOAL]
case intro.intro
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
this : SecondCountableTopology ↑t
⊢ ∃ c, g =ᵐ[μ] const α c
[PROOFSTEP]
exact h.ae_eq_const_of_ae_eq_comp_of_ae_range₀ hgt hgm.aemeasurable.nullMeasurable hg_eq
