α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
⊢ t ∈ map g (Measure.ae (Measure.map f μ)) → t ∈ map (g ∘ f) (Measure.ae μ)
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
⊢ essSup (g ∘ f) μ ≤ essSup g (Measure.map f μ)
refine' limsSup_le_limsSup_of_le (fun t => _) (by isBoundedDefault) (by isBoundedDefault)
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
⊢ g ⁻¹' t ∈ Measure.ae (Measure.map f μ) → g ∘ f ⁻¹' t ∈ Measure.ae μ
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
⊢ t ∈ map g (Measure.ae (Measure.map f μ)) → t ∈ map (g ∘ f) (Measure.ae μ)
simp_rw [Filter.mem_map]
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
this : g ∘ f ⁻¹' t = f ⁻¹' (g ⁻¹' t)
⊢ g ⁻¹' t ∈ Measure.ae (Measure.map f μ) → g ∘ f ⁻¹' t ∈ Measure.ae μ
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
⊢ g ⁻¹' t ∈ Measure.ae (Measure.map f μ) → g ∘ f ⁻¹' t ∈ Measure.ae μ
have : g ∘ f ⁻¹' t = f ⁻¹' (g ⁻¹' t) := by
  ext1 x
  simp_rw [Set.mem_preimage, Function.comp]
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
this : g ∘ f ⁻¹' t = f ⁻¹' (g ⁻¹' t)
⊢ g ⁻¹' t ∈ Measure.ae (Measure.map f μ) → f ⁻¹' (g ⁻¹' t) ∈ Measure.ae μ
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
this : g ∘ f ⁻¹' t = f ⁻¹' (g ⁻¹' t)
⊢ g ⁻¹' t ∈ Measure.ae (Measure.map f μ) → g ∘ f ⁻¹' t ∈ Measure.ae μ
rw [this]
no goals
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
this : g ∘ f ⁻¹' t = f ⁻¹' (g ⁻¹' t)
⊢ g ⁻¹' t ∈ Measure.ae (Measure.map f μ) → f ⁻¹' (g ⁻¹' t) ∈ Measure.ae μ
exact fun h => mem_ae_of_mem_ae_map hf h
no goals
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map (g ∘ f) (Measure.ae μ))
isBoundedDefault
no goals
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
⊢ IsBounded (fun x x_1 => x ≤ x_1) (map g (Measure.ae (Measure.map f μ)))
isBoundedDefault
case h
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
x : α
⊢ x ∈ g ∘ f ⁻¹' t ↔ x ∈ f ⁻¹' (g ⁻¹' t)
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
⊢ g ∘ f ⁻¹' t = f ⁻¹' (g ⁻¹' t)
ext1 x
no goals
case h
α : Type u_1
β : Type u_3
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
γ : Type u_2
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
x : α
⊢ x ∈ g ∘ f ⁻¹' t ↔ x ∈ f ⁻¹' (g ⁻¹' t)
simp_rw [Set.mem_preimage, Function.comp]