case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (Measure.restrict μ (tᶜ))] 0 ∧ SigmaFinite (Measure.restrict μ t)
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
hf : AEFinStronglyMeasurable f μ
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (Measure.restrict μ (tᶜ))] 0 ∧ SigmaFinite (Measure.restrict μ t)
rcases hf with ⟨g, hg, hfg⟩
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ (x : α), x ∈ tᶜ → g x = 0
htμ : SigmaFinite (Measure.restrict μ t)
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (Measure.restrict μ (tᶜ))] 0 ∧ SigmaFinite (Measure.restrict μ t)
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (Measure.restrict μ (tᶜ))] 0 ∧ SigmaFinite (Measure.restrict μ t)
obtain ⟨t, ht, hgt_zero, htμ⟩ := hg.exists_set_sigmaFinite
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ (x : α), x ∈ tᶜ → g x = 0
htμ : SigmaFinite (Measure.restrict μ t)
⊢ f =ᶠ[ae (Measure.restrict μ (tᶜ))] 0
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ (x : α), x ∈ tᶜ → g x = 0
htμ : SigmaFinite (Measure.restrict μ t)
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (Measure.restrict μ (tᶜ))] 0 ∧ SigmaFinite (Measure.restrict μ t)
refine' ⟨t, ht, _, htμ⟩
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ (x : α), x ∈ tᶜ → g x = 0
htμ : SigmaFinite (Measure.restrict μ t)
⊢ (fun x => g x) =ᶠ[ae (Measure.restrict μ (tᶜ))] 0
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ (x : α), x ∈ tᶜ → g x = 0
htμ : SigmaFinite (Measure.restrict μ t)
⊢ f =ᶠ[ae (Measure.restrict μ (tᶜ))] 0
refine' EventuallyEq.trans (ae_restrict_of_ae hfg) _
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ (x : α), x ∈ tᶜ → g x = 0
htμ : SigmaFinite (Measure.restrict μ t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = OfNat.ofNat 0 x
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ (x : α), x ∈ tᶜ → g x = 0
htμ : SigmaFinite (Measure.restrict μ t)
⊢ (fun x => g x) =ᶠ[ae (Measure.restrict μ (tᶜ))] 0
rw [EventuallyEq, ae_restrict_iff' ht.compl]
no goals
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.549973
ι : Type ?u.549976
inst✝³ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f g✝ : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ (x : α), x ∈ tᶜ → g x = 0
htμ : SigmaFinite (Measure.restrict μ t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = OfNat.ofNat 0 x
exact eventually_of_forall hgt_zero