[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝ : ConditionallyCompleteLinearOrder β
x : β
f✝ : α → β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ essSup f μ = sInf {a | ↑↑μ {x | a < f x} = 0}
[PROOFSTEP]
dsimp [essSup, limsup, limsSup]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝ : ConditionallyCompleteLinearOrder β
x : β
f✝ : α → β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ sInf {a | ∀ᶠ (n : β) in map f (Measure.ae μ), n ≤ a} = sInf {a | ↑↑μ {x | a < f x} = 0}
[PROOFSTEP]
simp only [eventually_map, ae_iff, not_le]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝ : ConditionallyCompleteLinearOrder β
x : β
f✝ : α → β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ essInf f μ = sSup {a | ↑↑μ {x | f x < a} = 0}
[PROOFSTEP]
dsimp [essInf, liminf, limsInf]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝ : ConditionallyCompleteLinearOrder β
x : β
f✝ : α → β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ sSup {a | ∀ᶠ (n : β) in map f (Measure.ae μ), a ≤ n} = sSup {a | ↑↑μ {x | f x < a} = 0}
[PROOFSTEP]
simp only [eventually_map, ae_iff, not_le]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
x : β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f) _auto✝
⊢ ↑↑μ {y | essSup f μ < f y} = 0
[PROOFSTEP]
simp_rw [← not_le]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
x : β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f) _auto✝
⊢ ↑↑μ {y | ¬f y ≤ essSup f μ} = 0
[PROOFSTEP]
exact ae_le_essSup hf
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
x : β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f) _auto✝
⊢ ↑↑μ {y | f y < essInf f μ} = 0
[PROOFSTEP]
simp_rw [← not_le]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
x : β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f) _auto✝
⊢ ↑↑μ {y | ¬essInf f μ ≤ f y} = 0
[PROOFSTEP]
exact ae_essInf_le hf
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
m : MeasurableSpace α
f : α → β
⊢ ⊥ ∈ {a | ∀ᶠ (n : β) in map f (Measure.ae 0), n ≤ a}
[PROOFSTEP]
simp [Set.mem_setOf_eq, EventuallyLE, ae_iff]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
⊢ essSup f μ ≤ c
[PROOFSTEP]
refine' (essSup_mono_ae hf).trans _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
⊢ essSup (fun x => c) μ ≤ c
[PROOFSTEP]
by_cases hμ : μ = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
hμ : μ = 0
⊢ essSup (fun x => c) μ ≤ c
[PROOFSTEP]
simp [hμ]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : β
hf : f ≤ᵐ[μ] fun x => c
hμ : ¬μ = 0
⊢ essSup (fun x => c) μ ≤ c
[PROOFSTEP]
rwa [essSup_const]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ ↑g (essSup f μ) = essSup (fun x => ↑g (f x)) μ
[PROOFSTEP]
refine' OrderIso.limsup_apply g _ _ _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
case refine'_2
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
case refine'_3
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) fun x => ↑g (f x)
case refine'_4
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) fun x => ↑g (f x)
[PROOFSTEP]
all_goals isBoundedDefault
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
[PROOFSTEP]
isBoundedDefault
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
[PROOFSTEP]
isBoundedDefault
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) fun x => ↑g (f x)
[PROOFSTEP]
isBoundedDefault
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) fun x => ↑g (f x)
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ essSup f ν ≤ essSup f μ
[PROOFSTEP]
refine' limsup_le_limsup_of_le (Measure.ae_le_iff_absolutelyContinuous.mpr hμν) _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae ν) f
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
[PROOFSTEP]
all_goals isBoundedDefault
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae ν) f
[PROOFSTEP]
isBoundedDefault
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : ν ≪ μ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ essInf f ν ≤ essInf f μ
[PROOFSTEP]
refine' liminf_le_liminf_of_le (Measure.ae_le_iff_absolutelyContinuous.mpr hμν) _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsBoundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae ν) f
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsCoboundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f
[PROOFSTEP]
all_goals isBoundedDefault
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsBoundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae ν) f
[PROOFSTEP]
isBoundedDefault
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsCoboundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ essSup f (c • μ) = essSup f μ
[PROOFSTEP]
simp_rw [essSup]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ limsup f (Measure.ae (c • μ)) = limsup f (Measure.ae μ)
[PROOFSTEP]
suffices h_smul : (c • μ).ae = μ.ae
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
h_smul : Measure.ae (c • μ) = Measure.ae μ
⊢ limsup f (Measure.ae (c • μ)) = limsup f (Measure.ae μ)
[PROOFSTEP]
rw [h_smul]
[GOAL]
case h_smul
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ Measure.ae (c • μ) = Measure.ae μ
[PROOFSTEP]
ext1
[GOAL]
case h_smul.a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
s✝ : Set α
⊢ s✝ ∈ Measure.ae (c • μ) ↔ s✝ ∈ Measure.ae μ
[PROOFSTEP]
simp_rw [mem_ae_iff]
[GOAL]
case h_smul.a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
s✝ : Set α
⊢ ↑↑(c • μ) s✝ᶜ = 0 ↔ ↑↑μ s✝ᶜ = 0
[PROOFSTEP]
simp [hc]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
⊢ essSup (g ∘ f) μ ≤ essSup g (Measure.map f μ)
[PROOFSTEP]
refine' limsSup_le_limsSup_of_le (fun t => _) (by isBoundedDefault) (by isBoundedDefault)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map (g ∘ f) (Measure.ae μ))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
⊢ IsBounded (fun x x_1 => x ≤ x_1) (map g (Measure.ae (Measure.map f μ)))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
⊢ t ∈ map g (Measure.ae (Measure.map f μ)) → t ∈ map (g ∘ f) (Measure.ae μ)
[PROOFSTEP]
simp_rw [Filter.mem_map]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
⊢ g ⁻¹' t ∈ Measure.ae (Measure.map f μ) → g ∘ f ⁻¹' t ∈ Measure.ae μ
[PROOFSTEP]
have : g ∘ f ⁻¹' t = f ⁻¹' (g ⁻¹' t) := by
  ext1 x
  simp_rw [Set.mem_preimage, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
⊢ g ∘ f ⁻¹' t = f ⁻¹' (g ⁻¹' t)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f
t : Set β
x : α
⊢ x ∈ g ∘ f ⁻¹' t ↔ x ∈ f ⁻¹' (g ⁻¹' t)
[PROOFSTEP]
simp_rw [Set.mem_preimage, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
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 μ
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
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 μ
[PROOFSTEP]
exact fun h => mem_ae_of_mem_ae_map hf h
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ
[PROOFSTEP]
refine' le_antisymm _ (essSup_comp_le_essSup_map_measure hf.measurable.aemeasurable)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
⊢ essSup g (Measure.map f μ) ≤ essSup (g ∘ f) μ
[PROOFSTEP]
refine' limsSup_le_limsSup (by isBoundedDefault) (by isBoundedDefault) (fun c h_le => _)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map g (Measure.ae (Measure.map f μ)))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
⊢ IsBounded (fun x x_1 => x ≤ x_1) (map (g ∘ f) (Measure.ae μ))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (Measure.ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (Measure.ae (Measure.map f μ)), n ≤ c
[PROOFSTEP]
rw [eventually_map] at h_le ⊢
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
[PROOFSTEP]
exact hf.ae_map_iff.mpr h_le
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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) μ
[PROOFSTEP]
refine' le_antisymm _ (essSup_comp_le_essSup_map_measure hf)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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) μ
[PROOFSTEP]
refine' limsSup_le_limsSup (by isBoundedDefault) (by isBoundedDefault) (fun c h_le => _)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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 μ)))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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 μ))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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
[PROOFSTEP]
rw [eventually_map] at h_le ⊢
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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
[PROOFSTEP]
rw [ae_map_iff hf (measurableSet_le hg measurable_const)]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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
[PROOFSTEP]
exact h_le
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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) μ
[PROOFSTEP]
rw [essSup_congr_ae hg.ae_eq_mk, essSup_map_measure_of_measurable hg.measurable_mk hf]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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) μ
[PROOFSTEP]
refine' essSup_congr_ae _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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
[PROOFSTEP]
have h_eq := ae_of_ae_map hf hg.ae_eq_mk
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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
[PROOFSTEP]
rw [← EventuallyEq] at h_eq
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
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
[PROOFSTEP]
exact h_eq.symm
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ essSup (indicator s f) μ = essSup f (Measure.restrict μ s)
[PROOFSTEP]
refine'
  le_antisymm _
    (limsSup_le_limsSup_of_le (map_restrict_ae_le_map_indicator_ae hs) (by isBoundedDefault) (by isBoundedDefault))
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map f (Measure.ae (Measure.restrict μ s)))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ IsBounded (fun x x_1 => x ≤ x_1) (map (indicator s f) (Measure.ae μ))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ essSup (indicator s f) μ ≤ essSup f (Measure.restrict μ s)
[PROOFSTEP]
refine' limsSup_le_limsSup (by isBoundedDefault) (by isBoundedDefault) (fun c h_restrict_le => _)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ IsCobounded (fun x x_1 => x ≤ x_1) (map (indicator s f) (Measure.ae μ))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
⊢ IsBounded (fun x x_1 => x ≤ x_1) (map f (Measure.ae (Measure.restrict μ s)))
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᶠ (n : β) in map f (Measure.ae (Measure.restrict μ s)), n ≤ c
⊢ ∀ᶠ (n : β) in map (indicator s f) (Measure.ae μ), n ≤ c
[PROOFSTEP]
rw [eventually_map] at h_restrict_le ⊢
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (a : α) ∂Measure.restrict μ s, f a ≤ c
⊢ ∀ᵐ (a : α) ∂μ, indicator s f a ≤ c
[PROOFSTEP]
rw [ae_restrict_iff' hs] at h_restrict_le
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∀ᵐ (a : α) ∂μ, indicator s f a ≤ c
[PROOFSTEP]
have hc : 0 ≤ c := by
  rsuffices ⟨x, hx⟩ : ∃ x, 0 ≤ f x ∧ f x ≤ c
  exact hx.1.trans hx.2
  refine' Frequently.exists _
  · exact μ.ae
  rw [EventuallyLE, ae_restrict_iff' hs] at hf
  have hs' : ∃ᵐ x ∂μ, x ∈ s := by
    contrapose! hs_not_null
    rw [not_frequently, ae_iff] at hs_not_null
    suffices {a : α | ¬a ∉ s} = s by rwa [← this]
    simp
  refine' hs'.mp (hf.mp (h_restrict_le.mono fun x hxs_imp_c hxf_nonneg hxs => _))
  rw [Pi.zero_apply] at hxf_nonneg
  exact ⟨hxf_nonneg hxs, hxs_imp_c hxs⟩
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ 0 ≤ c
[PROOFSTEP]
rsuffices ⟨x, hx⟩ : ∃ x, 0 ≤ f x ∧ f x ≤ c
[GOAL]
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
x : α
hx : 0 ≤ f x ∧ f x ≤ c
⊢ 0 ≤ c
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ x, 0 ≤ f x ∧ f x ≤ c
[PROOFSTEP]
exact hx.1.trans hx.2
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ x, 0 ≤ f x ∧ f x ≤ c
[PROOFSTEP]
refine' Frequently.exists _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ Filter α
[PROOFSTEP]
exact μ.ae
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ᵐ (x : α) ∂μ, 0 ≤ f x ∧ f x ≤ c
[PROOFSTEP]
rw [EventuallyLE, ae_restrict_iff' hs] at hf
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ᵐ (x : α) ∂μ, 0 ≤ f x ∧ f x ≤ c
[PROOFSTEP]
have hs' : ∃ᵐ x ∂μ, x ∈ s := by
  contrapose! hs_not_null
  rw [not_frequently, ae_iff] at hs_not_null
  suffices {a : α | ¬a ∉ s} = s by rwa [← this]
  simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
⊢ ∃ᵐ (x : α) ∂μ, x ∈ s
[PROOFSTEP]
contrapose! hs_not_null
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ¬∃ᵐ (x : α) ∂μ, x ∈ s
⊢ ↑↑μ s = 0
[PROOFSTEP]
rw [not_frequently, ae_iff] at hs_not_null
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ↑↑μ {a | ¬¬a ∈ s} = 0
⊢ ↑↑μ s = 0
[PROOFSTEP]
suffices {a : α | ¬a ∉ s} = s by rwa [← this]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ↑↑μ {a | ¬¬a ∈ s} = 0
this : {a | ¬¬a ∈ s} = s
⊢ ↑↑μ s = 0
[PROOFSTEP]
rwa [← this]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs_not_null : ↑↑μ {a | ¬¬a ∈ s} = 0
⊢ {a | ¬¬a ∈ s} = s
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs' : ∃ᵐ (x : α) ∂μ, x ∈ s
⊢ ∃ᵐ (x : α) ∂μ, 0 ≤ f x ∧ f x ≤ c
[PROOFSTEP]
refine' hs'.mp (hf.mp (h_restrict_le.mono fun x hxs_imp_c hxf_nonneg hxs => _))
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs' : ∃ᵐ (x : α) ∂μ, x ∈ s
x : α
hxs_imp_c : x ∈ s → f x ≤ c
hxf_nonneg : x ∈ s → OfNat.ofNat 0 x ≤ f x
hxs : x ∈ s
⊢ 0 ≤ f x ∧ f x ≤ c
[PROOFSTEP]
rw [Pi.zero_apply] at hxf_nonneg
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → OfNat.ofNat 0 x ≤ f x
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hs' : ∃ᵐ (x : α) ∂μ, x ∈ s
x : α
hxs_imp_c : x ∈ s → f x ≤ c
hxf_nonneg : x ∈ s → 0 ≤ f x
hxs : x ∈ s
⊢ 0 ≤ f x ∧ f x ≤ c
[PROOFSTEP]
exact ⟨hxf_nonneg hxs, hxs_imp_c hxs⟩
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
⊢ ∀ᵐ (a : α) ∂μ, indicator s f a ≤ c
[PROOFSTEP]
refine' h_restrict_le.mono fun x hxc => _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
x : α
hxc : x ∈ s → f x ≤ c
⊢ indicator s f x ≤ c
[PROOFSTEP]
by_cases hxs : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
x : α
hxc : x ∈ s → f x ≤ c
hxs : x ∈ s
⊢ indicator s f x ≤ c
[PROOFSTEP]
simpa [hxs] using hxc hxs
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : CompleteLinearOrder β
inst✝ : Zero β
s : Set α
f : α → β
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hs : MeasurableSet s
hs_not_null : ↑↑μ s ≠ 0
c : β
h_restrict_le : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ c
hc : 0 ≤ c
x : α
hxc : x ∈ s → f x ≤ c
hxs : ¬x ∈ s
⊢ indicator s f x ≤ c
[PROOFSTEP]
simpa [hxs] using hc
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
f✝ : α → ℝ≥0∞
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → ℝ≥0∞
⊢ essSup (fun x => liminf (fun n => f n x) atTop) μ ≤ liminf (fun n => essSup (fun x => f n x) μ) atTop
[PROOFSTEP]
simp_rw [essSup]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
f✝ : α → ℝ≥0∞
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → ℝ≥0∞
⊢ limsup (fun x => liminf (fun n => f n x) atTop) (Measure.ae μ) ≤
    liminf (fun n => limsup (fun x => f n x) (Measure.ae μ)) atTop
[PROOFSTEP]
exact ENNReal.limsup_liminf_le_liminf_limsup fun a b => f b a
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
f✝ : α → ℝ≥0∞
f : α → ℝ≥0
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
r : ℝ≥0∞
⊢ r ≤
      ⨅ (a : ℝ≥0) (_ : a ∈ fun x => sets (map f (Measure.ae μ)) {x_1 | (fun x_2 => (fun x x_3 => x ≤ x_3) x_2 x) x_1}),
        ↑a ↔
    r ≤ essSup (fun x => ↑(f x)) μ
[PROOFSTEP]
simp [essSup, limsup, limsSup, eventually_map, ENNReal.forall_ennreal]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
f✝ : α → ℝ≥0∞
f : α → ℝ≥0
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
r : ℝ≥0∞
⊢ (∀ (i : ℝ≥0), (i ∈ fun x => sets (map f (Measure.ae μ)) {x_1 | x_1 ≤ x}) → r ≤ ↑i) ↔
    ∀ (r_1 : ℝ≥0), (∀ᵐ (a : α) ∂μ, f a ≤ r_1) → r ≤ ↑r_1
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : TopologicalSpace.SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
⊢ AEMeasurable fun x => Inner.inner (f x) (g x)
[PROOFSTEP]
refine' ⟨fun x => ⟪hf.mk f x, hg.mk g x⟫, hf.measurable_mk.inner hg.measurable_mk, _⟩
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : TopologicalSpace.SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
⊢ (fun x => Inner.inner (f x) (g x)) =ᶠ[MeasureTheory.Measure.ae μ] fun x => Inner.inner (mk f hf x) (mk g hg x)
[PROOFSTEP]
refine' hf.ae_eq_mk.mp (hg.ae_eq_mk.mono fun x hxg hxf => _)
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : TopologicalSpace.SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hxg : g x = mk g hg x
hxf : f x = mk f hf x
⊢ (fun x => Inner.inner (f x) (g x)) x = (fun x => Inner.inner (mk f hf x) (mk g hg x)) x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : TopologicalSpace.SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hxg : g x = mk g hg x
hxf : f x = mk f hf x
⊢ Inner.inner (f x) (g x) = Inner.inner (mk f hf x) (mk g hg x)
[PROOFSTEP]
congr