α : 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 : Measurable g
hf : AEMeasurable f
⊢ essSup g (Measure.map 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 : Measurable g
hf : AEMeasurable f
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ
refine' le_antisymm _ (essSup_comp_le_essSup_map_measure 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 : Measurable g
hf : AEMeasurable f
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (Measure.ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (Measure.ae (Measure.map f μ)), n ≤ c
α : 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 : Measurable g
hf : AEMeasurable f
⊢ essSup g (Measure.map f μ) ≤ essSup (g ∘ f) μ
refine' limsSup_le_limsSup (by isBoundedDefault) (by isBoundedDefault) (fun c h_le => _)
α : 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 : Measurable g
hf : AEMeasurable f
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
α : 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 : Measurable g
hf : AEMeasurable f
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (Measure.ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (Measure.ae (Measure.map f μ)), n ≤ c
rw [eventually_map] at h_le ⊢
α : 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 : Measurable g
hf : AEMeasurable f
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (x : α) ∂μ, g (f x) ≤ c
α : 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 : Measurable g
hf : AEMeasurable f
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
rw [ae_map_iff hf (measurableSet_le hg measurable_const)]
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 : Measurable g
hf : AEMeasurable f
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (x : α) ∂μ, g (f x) ≤ c
exact h_le
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 : Measurable g
hf : AEMeasurable f
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map g (Measure.ae (Measure.map f μ)))
isBoundedDefault
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 : Measurable g
hf : AEMeasurable f
⊢ IsBounded (fun x x_1 => x ≤ x_1) (map (g ∘ f) (Measure.ae μ))
isBoundedDefault