α : Type u_3
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_1
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g
hf : AEMeasurable f
⊢ essSup (AEMeasurable.mk g hg ∘ f) μ = essSup (g ∘ f) μ
α : Type u_3
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_1
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g
hf : AEMeasurable f
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ
rw [essSup_congr_ae hg.ae_eq_mk, essSup_map_measure_of_measurable hg.measurable_mk hf]
α : Type u_3
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_1
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g
hf : AEMeasurable f
⊢ AEMeasurable.mk g hg ∘ f =ᵐ[μ] g ∘ f
α : Type u_3
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_1
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g
hf : AEMeasurable f
⊢ essSup (AEMeasurable.mk g hg ∘ f) μ = essSup (g ∘ f) μ
refine' essSup_congr_ae _
α : Type u_3
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_1
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g
hf : AEMeasurable f
h_eq : ∀ᵐ (x : α) ∂μ, g (f x) = AEMeasurable.mk g hg (f x)
⊢ AEMeasurable.mk g hg ∘ f =ᵐ[μ] g ∘ f
α : Type u_3
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_1
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g
hf : AEMeasurable f
⊢ AEMeasurable.mk g hg ∘ f =ᵐ[μ] g ∘ f
have h_eq := ae_of_ae_map hf hg.ae_eq_mk
α : Type u_3
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_1
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g
hf : AEMeasurable f
h_eq : (fun x => g (f x)) =ᵐ[μ] fun x => AEMeasurable.mk g hg (f x)
⊢ AEMeasurable.mk g hg ∘ f =ᵐ[μ] g ∘ f
α : Type u_3
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_1
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g
hf : AEMeasurable f
h_eq : ∀ᵐ (x : α) ∂μ, g (f x) = AEMeasurable.mk g hg (f x)
⊢ AEMeasurable.mk g hg ∘ f =ᵐ[μ] g ∘ f
rw [← EventuallyEq] at h_eq
no goals
α : Type u_3
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_1
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g
hf : AEMeasurable f
h_eq : (fun x => g (f x)) =ᵐ[μ] fun x => AEMeasurable.mk g hg (f x)
⊢ AEMeasurable.mk g hg ∘ f =ᵐ[μ] g ∘ f
exact h_eq.symm