[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g
hu : AEMeasurable u
⊢ AEMeasurable (u ∘ g)
[PROOFSTEP]
rw [h.map_eq] at hu
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g
hu : AEMeasurable u
⊢ AEMeasurable (u ∘ g)
[PROOFSTEP]
exact hu.comp_aemeasurable h.aemeasurable_snd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g
hu : AEMeasurable u
⊢ Measure.map (u ∘ f) μ = Measure.map (u ∘ g) ν
[PROOFSTEP]
rw [← AEMeasurable.map_map_of_aemeasurable hu h.aemeasurable_fst, ←
  AEMeasurable.map_map_of_aemeasurable _ h.aemeasurable_snd, h.map_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g
hu : AEMeasurable u
⊢ AEMeasurable u
[PROOFSTEP]
rwa [← h.map_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g
s : Set γ
hs : MeasurableSet s
⊢ ↑↑μ (f ⁻¹' s) = ↑↑ν (g ⁻¹' s)
[PROOFSTEP]
rw [← Measure.map_apply_of_aemeasurable h.aemeasurable_fst hs, ←
  Measure.map_apply_of_aemeasurable h.aemeasurable_snd hs, h.map_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g
p : γ → Prop
pmeas : MeasurableSet {x | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (x : β) ∂ν, p (g x)
[PROOFSTEP]
apply (ae_map_iff h.aemeasurable_snd pmeas).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g
p : γ → Prop
pmeas : MeasurableSet {x | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (y : γ) ∂Measure.map g ν, p y
[PROOFSTEP]
rw [← h.map_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g
p : γ → Prop
pmeas : MeasurableSet {x | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (y : γ) ∂Measure.map f μ, p y
[PROOFSTEP]
exact (ae_map_iff h.aemeasurable_fst pmeas).2 hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : TopologicalSpace γ
inst✝¹ : MetrizableSpace γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable g ν
[PROOFSTEP]
refine' aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨h.aemeasurable_snd, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : TopologicalSpace γ
inst✝¹ : MetrizableSpace γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
[PROOFSTEP]
rcases(aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : TopologicalSpace γ
inst✝¹ : MetrizableSpace γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
[PROOFSTEP]
refine' ⟨closure t, t_sep.closure, _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : TopologicalSpace γ
inst✝¹ : MetrizableSpace γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : β) ∂ν, g x ∈ closure t
[PROOFSTEP]
apply h.ae_mem_snd isClosed_closure.measurableSet
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : TopologicalSpace γ
inst✝¹ : MetrizableSpace γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure t
[PROOFSTEP]
filter_upwards [ht] with x hx using subset_closure hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g
⊢ essSup f μ = essSup g ν
[PROOFSTEP]
have I : ∀ a, μ {x : α | a < f x} = ν {x : β | a < g x} := fun a => h.measure_mem_eq measurableSet_Ioi
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝³ : ConditionallyCompleteLinearOrder γ
inst✝² : TopologicalSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : OrderClosedTopology γ
h : IdentDistrib f g
I : ∀ (a : γ), ↑↑μ {x | a < f x} = ↑↑ν {x | a < g x}
⊢ essSup f μ = essSup g ν
[PROOFSTEP]
simp_rw [essSup_eq_sInf, I]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f✝ : α → γ
g✝ : β → γ
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : β), g x ∂ν
[PROOFSTEP]
change ∫⁻ x, id (f x) ∂μ = ∫⁻ x, id (g x) ∂ν
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f✝ : α → γ
g✝ : β → γ
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g
⊢ ∫⁻ (x : α), id (f x) ∂μ = ∫⁻ (x : β), id (g x) ∂ν
[PROOFSTEP]
rw [← lintegral_map' aemeasurable_id h.aemeasurable_fst, ← lintegral_map' aemeasurable_id h.aemeasurable_snd, h.map_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
⊢ ∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν
[PROOFSTEP]
by_cases hf : AEStronglyMeasurable f μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν
[PROOFSTEP]
have A : AEStronglyMeasurable id (Measure.map f μ) :=
  by
  rw [aestronglyMeasurable_iff_aemeasurable_separable]
  rcases(aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
  refine' ⟨aemeasurable_id, ⟨closure t, t_sep.closure, _⟩⟩
  rw [ae_map_iff h.aemeasurable_fst]
  · filter_upwards [ht] with x hx using subset_closure hx
  · exact isClosed_closure.measurableSet
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable id (Measure.map f μ)
[PROOFSTEP]
rw [aestronglyMeasurable_iff_aemeasurable_separable]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
⊢ AEMeasurable id ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t
[PROOFSTEP]
rcases(aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEMeasurable id ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t
[PROOFSTEP]
refine' ⟨aemeasurable_id, ⟨closure t, t_sep.closure, _⟩⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ closure t
[PROOFSTEP]
rw [ae_map_iff h.aemeasurable_fst]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, id (f x) ∈ closure t
[PROOFSTEP]
filter_upwards [ht] with x hx using subset_closure hx
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ MeasurableSet {x | id x ∈ closure t}
[PROOFSTEP]
exact isClosed_closure.measurableSet
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable id (Measure.map f μ)
⊢ ∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν
[PROOFSTEP]
change ∫ x, id (f x) ∂μ = ∫ x, id (g x) ∂ν
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable id (Measure.map f μ)
⊢ ∫ (x : α), id (f x) ∂μ = ∫ (x : β), id (g x) ∂ν
[PROOFSTEP]
rw [← integral_map h.aemeasurable_fst A]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable id (Measure.map f μ)
⊢ ∫ (y : γ), id y ∂Measure.map f μ = ∫ (x : β), id (g x) ∂ν
[PROOFSTEP]
rw [h.map_eq] at A
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable id (Measure.map g ν)
⊢ ∫ (y : γ), id y ∂Measure.map f μ = ∫ (x : β), id (g x) ∂ν
[PROOFSTEP]
rw [← integral_map h.aemeasurable_snd A, h.map_eq]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : ¬AEStronglyMeasurable f μ
⊢ ∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν
[PROOFSTEP]
rw [integral_non_aestronglyMeasurable hf]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : ¬AEStronglyMeasurable f μ
⊢ 0 = ∫ (x : β), g x ∂ν
[PROOFSTEP]
rw [h.aestronglyMeasurable_iff] at hf
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
inst✝³ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : ¬AEStronglyMeasurable g ν
⊢ 0 = ∫ (x : β), g x ∂ν
[PROOFSTEP]
rw [integral_non_aestronglyMeasurable hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
⊢ snorm f p μ = snorm g p ν
[PROOFSTEP]
by_cases h0 : p = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
h0 : p = 0
⊢ snorm f p μ = snorm g p ν
[PROOFSTEP]
simp [h0]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
h0 : ¬p = 0
⊢ snorm f p μ = snorm g p ν
[PROOFSTEP]
by_cases h_top : p = ∞
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ⊤
⊢ snorm f p μ = snorm g p ν
[PROOFSTEP]
simp only [h_top, snorm, snormEssSup, ENNReal.top_ne_zero, eq_self_iff_true, if_true, if_false]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ⊤
⊢ essSup (fun x => ↑‖f x‖₊) μ = essSup (fun x => ↑‖g x‖₊) ν
[PROOFSTEP]
apply essSup_eq
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ⊤
⊢ IdentDistrib (fun x => ↑‖f x‖₊) fun x => ↑‖g x‖₊
[PROOFSTEP]
exact h.comp (measurable_coe_nnreal_ennreal.comp measurable_nnnorm)
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ snorm f p μ = snorm g p ν
[PROOFSTEP]
simp only [snorm_eq_snorm' h0 h_top, snorm', one_div]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ) ^ (ENNReal.toReal p)⁻¹ =
    (∫⁻ (a : β), ↑‖g a‖₊ ^ ENNReal.toReal p ∂ν) ^ (ENNReal.toReal p)⁻¹
[PROOFSTEP]
congr 1
[GOAL]
case neg.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ^ ENNReal.toReal p ∂μ = ∫⁻ (a : β), ↑‖g a‖₊ ^ ENNReal.toReal p ∂ν
[PROOFSTEP]
apply lintegral_eq
[GOAL]
case neg.e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : OpensMeasurableSpace γ
h : IdentDistrib f g
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ IdentDistrib (fun x => ↑‖f x‖₊ ^ ENNReal.toReal p) fun x => ↑‖g x‖₊ ^ ENNReal.toReal p
[PROOFSTEP]
exact h.comp (Measurable.pow_const (measurable_coe_nnreal_ennreal.comp measurable_nnnorm) p.toReal)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g
hf : Memℒp f p
⊢ Memℒp g p
[PROOFSTEP]
refine' ⟨h.aestronglyMeasurable_snd hf.aestronglyMeasurable, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g
hf : Memℒp f p
⊢ snorm g p ν < ⊤
[PROOFSTEP]
rw [← h.snorm_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
p : ℝ≥0∞
h : IdentDistrib f g
hf : Memℒp f p
⊢ snorm f p μ < ⊤
[PROOFSTEP]
exact hf.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : Integrable f
⊢ Integrable g
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
h : IdentDistrib f g
hf : Memℒp f 1
⊢ Memℒp g 1
[PROOFSTEP]
exact h.memℒp_snd hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f✝ : α → γ
g✝ : β → γ
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g
⊢ evariance f μ = evariance g ν
[PROOFSTEP]
convert (h.sub_const (∫ x, f x ∂μ)).nnnorm.coe_nnreal_ennreal.sq.lintegral_eq
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f✝ : α → γ
g✝ : β → γ
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g
⊢ evariance g ν = ∫⁻ (x : β), ↑‖g x - ∫ (x : α), f x ∂μ‖₊ ^ 2 ∂ν
[PROOFSTEP]
rw [h.integral_eq]
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f✝ : α → γ
g✝ : β → γ
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g
⊢ evariance g ν = ∫⁻ (x : β), ↑‖g x - ∫ (x : β), g x ∂ν‖₊ ^ 2 ∂ν
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f✝ : α → γ
g✝ : β → γ
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g
⊢ variance f μ = variance g ν
[PROOFSTEP]
rw [variance, h.evariance_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f✝ : α → γ
g✝ : β → γ
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g
⊢ ENNReal.toReal (evariance g ν) = variance g ν
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
⊢ UniformIntegrable f p μ
[PROOFSTEP]
refine' uniformIntegrable_of' hp hp' hfmeas fun ε hε => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
by_cases hι : Nonempty ι
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : ¬Nonempty ι
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
exact ⟨0, fun i => False.elim (hι <| Nonempty.intro i)⟩
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
obtain ⟨C, hC₁, hC₂⟩ := hℒp.snorm_indicator_norm_ge_pos_le μ (hfmeas _) hε
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
refine' ⟨⟨C, hC₁.le⟩, fun i => le_trans (le_of_eq _) hC₂⟩
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ snorm (Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i)) p μ =
    snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ
[PROOFSTEP]
have :
  {x : α | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖f i x‖₊}.indicator (f i) =
    (fun x : E => if (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖x‖₊ then x else 0) ∘ f i :=
  by
  ext x
  simp only [Set.indicator, Set.mem_setOf_eq]; norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i) =
    (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i) x =
    ((fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i) x
[PROOFSTEP]
simp only [Set.indicator, Set.mem_setOf_eq]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ (if { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊ then f i x else 0) =
    ((fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i) x
[PROOFSTEP]
norm_cast
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this :
  Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i) =
    (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i
⊢ snorm (Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i)) p μ =
    snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ
[PROOFSTEP]
simp_rw [coe_nnnorm, this]
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this :
  Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i) =
    (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i
⊢ snorm ((fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i) p μ =
    snorm (Set.indicator {x | C ≤ ‖f j x‖} (f j)) p μ
[PROOFSTEP]
rw [← snorm_map_measure _ (hf i).aemeasurable_fst, (hf i).map_eq, snorm_map_measure _ (hf j).aemeasurable_fst]
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this :
  Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i) =
    (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i
⊢ snorm ((fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f j) p μ =
    snorm (Set.indicator {x | C ≤ ‖f j x‖} (f j)) p μ
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this :
  Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i) =
    (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i
⊢ AEStronglyMeasurable (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) (Measure.map (f j) μ)
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this :
  Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i) =
    (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i
⊢ AEStronglyMeasurable (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) (Measure.map (f i) μ)
[PROOFSTEP]
all_goals exact_mod_cast aestronglyMeasurable_id.indicator (measurableSet_le measurable_const measurable_nnnorm)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this :
  Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i) =
    (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i
⊢ AEStronglyMeasurable (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) (Measure.map (f j) μ)
[PROOFSTEP]
exact_mod_cast aestronglyMeasurable_id.indicator (measurableSet_le measurable_const measurable_nnnorm)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : snorm (Set.indicator {x | C ≤ ↑‖f j x‖₊} (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this :
  Set.indicator {x | { val := C, property := (_ : 0 ≤ C) } ≤ ‖f i x‖₊} (f i) =
    (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) ∘ f i
⊢ AEStronglyMeasurable (fun x => if { val := C, property := (_ : 0 ≤ C) } ≤ ‖x‖₊ then x else 0) (Measure.map (f i) μ)
[PROOFSTEP]
exact_mod_cast aestronglyMeasurable_id.indicator (measurableSet_le measurable_const measurable_nnnorm)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
⊢ UniformIntegrable f p μ
[PROOFSTEP]
have hfmeas : ∀ i, AEStronglyMeasurable (f i) μ := fun i => (hf i).aestronglyMeasurable_iff.2 hℒp.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ UniformIntegrable f p μ
[PROOFSTEP]
set g : ι → α → E := fun i => (hfmeas i).choose
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
⊢ UniformIntegrable f p μ
[PROOFSTEP]
have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfmeas i).1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
⊢ UniformIntegrable f p μ
[PROOFSTEP]
have hgeq : ∀ i, g i =ᵐ[μ] f i := fun i => (Exists.choose_spec <| hfmeas i).2.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
⊢ UniformIntegrable f p μ
[PROOFSTEP]
have hgℒp : Memℒp (g j) p μ := hℒp.ae_eq (hgeq j).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : MeasurableSpace δ
E : Type u_5
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
hℒp : Memℒp (f j) p
hf : ∀ (i : ι), IdentDistrib (f i) (f j)
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
g : ι → α → E := fun i => Exists.choose (_ : AEStronglyMeasurable (f i) μ)
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
hgℒp : Memℒp (g j) p
⊢ UniformIntegrable f p μ
[PROOFSTEP]
exact
  UniformIntegrable.ae_eq
    (Memℒp.uniformIntegrable_of_identDistrib_aux hp hp' hgℒp hgmeas fun i =>
      (IdentDistrib.of_ae_eq (hgmeas i).aemeasurable (hgeq i)).trans
        ((hf i).trans <| IdentDistrib.of_ae_eq (hfmeas j).aemeasurable (hgeq j).symm))
    hgeq


[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f g : Filtration ι m
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
g : Filtration ι m
seq✝ : ι → MeasurableSpace Ω
mono'✝ : Monotone seq✝
le'✝ : ∀ (i : ι), seq✝ i ≤ m
h : ↑{ seq := seq✝, mono' := mono'✝, le' := le'✝ } = ↑g
⊢ { seq := seq✝, mono' := mono'✝, le' := le'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
seq✝¹ : ι → MeasurableSpace Ω
mono'✝¹ : Monotone seq✝¹
le'✝¹ : ∀ (i : ι), seq✝¹ i ≤ m
seq✝ : ι → MeasurableSpace Ω
mono'✝ : Monotone seq✝
le'✝ : ∀ (i : ι), seq✝ i ≤ m
h : ↑{ seq := seq✝¹, mono' := mono'✝¹, le' := le'✝¹ } = ↑{ seq := seq✝, mono' := mono'✝, le' := le'✝ }
⊢ { seq := seq✝¹, mono' := mono'✝¹, le' := le'✝¹ } = { seq := seq✝, mono' := mono'✝, le' := le'✝ }
[PROOFSTEP]
congr
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
⊢ (fun i => sSup ((fun f => ↑f i) '' s)) i ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
refine' sSup_le fun m' hm' => _
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : m' ∈ (fun f => ↑f i) '' s
⊢ m' ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
rw [Set.mem_image] at hm'
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : ∃ x, x ∈ s ∧ ↑x i = m'
⊢ m' ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
obtain ⟨f, hf_mem, hfm'⟩ := hm'
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ m' ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
rw [← hfm']
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
refine' (f.mono hij).trans _
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f j ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
have hfj_mem : f j ∈ (fun g : Filtration ι m => g j) '' s := ⟨f, hf_mem, rfl⟩
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
hfj_mem : ↑f j ∈ (fun g => ↑g j) '' s
⊢ ↑f j ≤ (fun i => sSup ((fun f => ↑f i) '' s)) j
[PROOFSTEP]
exact le_sSup hfj_mem
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ (fun i => sSup ((fun f => ↑f i) '' s)) i ≤ m
[PROOFSTEP]
refine' sSup_le fun m' hm' => _
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' : m' ∈ (fun f => ↑f i) '' s
⊢ m' ≤ m
[PROOFSTEP]
rw [Set.mem_image] at hm'
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' : ∃ x, x ∈ s ∧ ↑x i = m'
⊢ m' ≤ m
[PROOFSTEP]
obtain ⟨f, _, hfm'⟩ := hm'
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left✝ : f ∈ s
hfm' : ↑f i = m'
⊢ m' ≤ m
[PROOFSTEP]
rw [← hfm']
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left✝ : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ m
[PROOFSTEP]
exact f.le i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
[PROOFSTEP]
by_cases h_nonempty : Set.Nonempty s
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : ¬Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
[PROOFSTEP]
swap
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : ¬Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
[PROOFSTEP]
simp only [h_nonempty, Set.nonempty_image_iff, if_false, le_refl]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤
    (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) j
[PROOFSTEP]
simp only [h_nonempty, if_true, le_sInf_iff, Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
⊢ ∀ (a : Filtration ι m), a ∈ s → sInf ((fun f => ↑f i) '' s) ≤ ↑a j
[PROOFSTEP]
refine' fun f hf_mem => le_trans _ (f.mono hij)
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
f : Filtration ι m
hf_mem : f ∈ s
⊢ sInf ((fun f => ↑f i) '' s) ≤ ↑f i
[PROOFSTEP]
have hfi_mem : f i ∈ (fun g : Filtration ι m => g i) '' s := ⟨f, hf_mem, rfl⟩
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : Set.Nonempty s
f : Filtration ι m
hf_mem : f ∈ s
hfi_mem : ↑f i ∈ (fun g => ↑g i) '' s
⊢ sInf ((fun f => ↑f i) '' s) ≤ ↑f i
[PROOFSTEP]
exact sInf_le hfi_mem
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
[PROOFSTEP]
by_cases h_nonempty : Set.Nonempty s
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : ¬Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
[PROOFSTEP]
swap
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : ¬Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
[PROOFSTEP]
simp only [h_nonempty, if_false, le_refl]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : Set.Nonempty s
⊢ (fun i => if Set.Nonempty s then sInf ((fun f => ↑f i) '' s) else m) i ≤ m
[PROOFSTEP]
simp only [h_nonempty, if_true]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : Set.Nonempty s
⊢ sInf ((fun f => ↑f i) '' s) ≤ m
[PROOFSTEP]
obtain ⟨f, hf_mem⟩ := h_nonempty
[GOAL]
case pos.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
f : Filtration ι m
hf_mem : f ∈ s
⊢ sInf ((fun f => ↑f i) '' s) ≤ m
[PROOFSTEP]
exact le_trans (sInf_le ⟨f, hf_mem, rfl⟩) (f.le i)
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → b ≤ f
i : ι
m' : MeasurableSpace Ω
hm' : m' ∈ (fun f => ↑f i) '' s
⊢ m' ≤ ↑f i
[PROOFSTEP]
obtain ⟨g, hg_mem, hfm'⟩ := hm'
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → b ≤ f
i : ι
m' : MeasurableSpace Ω
g : Filtration ι m
hg_mem : g ∈ s
hfm' : (fun f => ↑f i) g = m'
⊢ m' ≤ ↑f i
[PROOFSTEP]
rw [← hfm']
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → b ≤ f
i : ι
m' : MeasurableSpace Ω
g : Filtration ι m
hg_mem : g ∈ s
hfm' : (fun f => ↑f i) g = m'
⊢ (fun f => ↑f i) g ≤ ↑f i
[PROOFSTEP]
exact h_forall g hg_mem i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
hf_mem : f ∈ s
i : ι
⊢ ↑(sInf s) i ≤ ↑f i
[PROOFSTEP]
have hs : s.Nonempty := ⟨f, hf_mem⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
hf_mem : f ∈ s
i : ι
hs : Set.Nonempty s
⊢ ↑(sInf s) i ≤ ↑f i
[PROOFSTEP]
simp only [sInf_def, hs, if_true]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
hf_mem : f ∈ s
i : ι
hs : Set.Nonempty s
⊢ sInf ((fun f => ↑f i) '' s) ≤ ↑f i
[PROOFSTEP]
exact sInf_le ⟨f, hf_mem, rfl⟩
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
⊢ ↑f i ≤ ↑(sInf s) i
[PROOFSTEP]
by_cases hs : s.Nonempty
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : Set.Nonempty s
⊢ ↑f i ≤ ↑(sInf s) i
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : ¬Set.Nonempty s
⊢ ↑f i ≤ ↑(sInf s) i
[PROOFSTEP]
swap
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : ¬Set.Nonempty s
⊢ ↑f i ≤ ↑(sInf s) i
[PROOFSTEP]
simp only [sInf_def, hs, if_false]
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : ¬Set.Nonempty s
⊢ ↑f i ≤ m
[PROOFSTEP]
exact f.le i
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : Set.Nonempty s
⊢ ↑f i ≤ ↑(sInf s) i
[PROOFSTEP]
simp only [sInf_def, hs, if_true, le_sInf_iff, Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
f : Filtration ι m
h_forall : ∀ (b : Filtration ι m), b ∈ s → f ≤ b
i : ι
hs : Set.Nonempty s
⊢ ∀ (a : Filtration ι m), a ∈ s → ↑f i ≤ ↑a i
[PROOFSTEP]
exact fun g hg_mem => h_forall g hg_mem i
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
μ : Measure Ω
f : Filtration ι m
inst✝ : IsFiniteMeasure μ
n : ι
⊢ SigmaFinite (Measure.trim μ (_ : ↑f n ≤ m))
[PROOFSTEP]
infer_instance
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : MetrizableSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
inst✝ : Preorder ι
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ (fun i => ⨆ (j : ι) (_ : j ≤ i), MeasurableSpace.comap (u j) mβ) i ≤ m
[PROOFSTEP]
refine' iSup₂_le _
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : MetrizableSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
inst✝ : Preorder ι
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ ∀ (i_1 : ι), i_1 ≤ i → MeasurableSpace.comap (u i_1) mβ ≤ m
[PROOFSTEP]
rintro j _ s ⟨t, ht, rfl⟩
[GOAL]
case intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : MetrizableSpace β
mβ : MeasurableSpace β
inst✝¹ : BorelSpace β
inst✝ : Preorder ι
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i j : ι
j✝ : j ≤ i
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (u j ⁻¹' t)
[PROOFSTEP]
exact (hum j).measurable ht
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
⊢ filtrationOfSet hsm =
    natural (fun i => Set.indicator (s i) fun x => 1) (_ : ∀ (i : ι), StronglyMeasurable (Set.indicator (s i) 1))
[PROOFSTEP]
simp [natural, filtrationOfSet, measurableSpace_iSup_eq]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
⊢ (fun i => MeasurableSpace.generateFrom {t | ∃ j, j ≤ i ∧ s j = t}) = fun i =>
    MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}
[PROOFSTEP]
ext1 i
[GOAL]
case h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ MeasurableSpace.generateFrom {t | ∃ j, j ≤ i ∧ s j = t} = MeasurableSpace.generateFrom {s_1 | ∃ n, MeasurableSet s_1}
[PROOFSTEP]
refine' le_antisymm (generateFrom_le _) (generateFrom_le _)
[GOAL]
case h.refine'_1
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ ∀ (t : Set Ω), t ∈ {t | ∃ j, j ≤ i ∧ s j = t} → MeasurableSet t
[PROOFSTEP]
rintro _ ⟨j, hij, rfl⟩
[GOAL]
case h.refine'_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)
[PROOFSTEP]
refine' measurableSet_generateFrom ⟨j, measurableSet_generateFrom ⟨hij, _⟩⟩
[GOAL]
case h.refine'_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)
[PROOFSTEP]
rw [comap_eq_generateFrom]
[GOAL]
case h.refine'_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ MeasurableSet (s j)
[PROOFSTEP]
refine' measurableSet_generateFrom ⟨{1}, measurableSet_singleton 1, _⟩
[GOAL]
case h.refine'_1.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
⊢ (Set.indicator (s j) fun x => 1) ⁻¹' {1} = s j
[PROOFSTEP]
ext x
[GOAL]
case h.refine'_1.intro.intro.h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i j : ι
hij : j ≤ i
x : Ω
⊢ x ∈ (Set.indicator (s j) fun x => 1) ⁻¹' {1} ↔ x ∈ s j
[PROOFSTEP]
simp [Set.indicator_const_preimage_eq_union]
[GOAL]
case h.refine'_2
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
⊢ ∀ (t : Set Ω), t ∈ {s_1 | ∃ n, MeasurableSet s_1} → MeasurableSet t
[PROOFSTEP]
rintro t ⟨n, ht⟩
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ MeasurableSet t
[PROOFSTEP]
suffices
  MeasurableSpace.generateFrom
      {t | n ≤ i ∧ MeasurableSet[MeasurableSpace.comap ((s n).indicator (fun _ => 1 : Ω → β)) mβ] t} ≤
    MeasurableSpace.generateFrom {t | ∃ (j : ι), j ≤ i ∧ s j = t}
  by exact this _ ht
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
this :
  MeasurableSpace.generateFrom {t | n ≤ i ∧ MeasurableSet t} ≤ MeasurableSpace.generateFrom {t | ∃ j, j ≤ i ∧ s j = t}
⊢ MeasurableSet t
[PROOFSTEP]
exact this _ ht
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ MeasurableSpace.generateFrom {t | n ≤ i ∧ MeasurableSet t} ≤ MeasurableSpace.generateFrom {t | ∃ j, j ≤ i ∧ s j = t}
[PROOFSTEP]
refine' generateFrom_le _
[GOAL]
case h.refine'_2.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ ∀ (t : Set Ω), t ∈ {t | n ≤ i ∧ MeasurableSet t} → MeasurableSet t
[PROOFSTEP]
rintro t ⟨hn, u, _, hu'⟩
[GOAL]
case h.refine'_2.intro.intro.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
⊢ MeasurableSet t
[PROOFSTEP]
obtain heq | heq | heq | heq := Set.indicator_const_preimage (s n) u (1 : β)
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u ∈ {∅}
⊢ MeasurableSet t
[PROOFSTEP]
pick_goal 4
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u ∈ {∅}
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
[PROOFSTEP]
rw [Set.mem_singleton_iff] at heq
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
[PROOFSTEP]
all_goals rw [heq] at hu' ; rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t
[PROOFSTEP]
rw [heq] at hu'
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ∅ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet t
[PROOFSTEP]
rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
[PROOFSTEP]
rw [heq] at hu'
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t
[PROOFSTEP]
rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
[PROOFSTEP]
rw [heq] at hu'
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : s n = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet t
[PROOFSTEP]
rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (Set.indicator (s n) fun x => 1) ⁻¹' u = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
[PROOFSTEP]
rw [heq] at hu'
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t
[PROOFSTEP]
rw [← hu']
[GOAL]
case h.refine'_2.intro.intro.intro.intro.inr.inr.inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : ∅ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = ∅
⊢ MeasurableSet ∅
case h.refine'_2.intro.intro.intro.intro.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = Set.univ
⊢ MeasurableSet Set.univ
case h.refine'_2.intro.intro.intro.intro.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : s n = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = s n
⊢ MeasurableSet (s n)
case h.refine'_2.intro.intro.intro.intro.inr.inr.inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set β
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : (Set.indicator (s n) fun x => 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet (s n)ᶜ
[PROOFSTEP]
exacts [measurableSet_empty _, MeasurableSet.univ, measurableSet_generateFrom ⟨n, hn, rfl⟩,
  MeasurableSet.compl (measurableSet_generateFrom ⟨n, hn, rfl⟩)]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable (limitProcess f ℱ μ)
[PROOFSTEP]
rw [limitProcess]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
⊢ StronglyMeasurable
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable (Classical.choose h)
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
E : Type u_4
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ℱ : Filtration ι m
f : ι → Ω → E
μ : Measure Ω
h : ¬∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ StronglyMeasurable 0
[PROOFSTEP]
exacts [(Classical.choose_spec h).1, stronglyMeasurable_zero]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
⊢ Memℒp (limitProcess f ℱ μ) p
[PROOFSTEP]
rw [limitProcess]
[GOAL]
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
⊢ Memℒp
    (if h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) then Classical.choose h
    else 0)
    p
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ Memℒp (Classical.choose h) p
[PROOFSTEP]
refine'
  ⟨StronglyMeasurable.aestronglyMeasurable ((Classical.choose_spec h).1.mono (sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _)),
    lt_of_le_of_lt (Lp.snorm_lim_le_liminf_snorm hfm _ (Classical.choose_spec h).2)
      (lt_of_le_of_lt _ (ENNReal.coe_lt_top : ↑R < ∞))⟩
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ liminf (fun n => snorm (f n) p μ) atTop ≤ ↑R
[PROOFSTEP]
simp_rw [liminf_eq, eventually_atTop]
[GOAL]
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ sSup {a | ∃ a_1, ∀ (b : ℕ), b ≥ a_1 → a ≤ snorm (f b) p μ} ≤ ↑R
[PROOFSTEP]
exact sSup_le fun b ⟨a, ha⟩ => (ha a le_rfl).trans (hbdd _)
[GOAL]
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : TopologicalSpace β
inst✝⁵ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : Preorder ι
E : Type u_4
inst✝² : Zero E
inst✝¹ : TopologicalSpace E
ℱ✝ : Filtration ι m
f✝ : ι → Ω → E
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
h : ¬∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))
⊢ Memℒp 0 p
[PROOFSTEP]
exact zero_memℒp


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ : { x // x ∈ kernel α β }
⊢ Measure.bind (μ + ν) ↑κ = Measure.bind μ ↑κ + Measure.bind ν ↑κ
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ : { x // x ∈ kernel α β }
s : Set β
hs : MeasurableSet s
⊢ ↑↑(Measure.bind (μ + ν) ↑κ) s = ↑↑(Measure.bind μ ↑κ + Measure.bind ν ↑κ) s
[PROOFSTEP]
rw [Measure.bind_apply hs (kernel.measurable _), lintegral_add_measure, Measure.coe_add, Pi.add_apply,
  Measure.bind_apply hs (kernel.measurable _), Measure.bind_apply hs (kernel.measurable _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
r : ℝ≥0∞
⊢ Measure.bind (r • μ) ↑κ = r • Measure.bind μ ↑κ
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
r : ℝ≥0∞
s : Set β
hs : MeasurableSet s
⊢ ↑↑(Measure.bind (r • μ) ↑κ) s = ↑↑(r • Measure.bind μ ↑κ) s
[PROOFSTEP]
rw [Measure.bind_apply hs (kernel.measurable _), lintegral_smul_measure, Measure.coe_smul, Pi.smul_apply,
  Measure.bind_apply hs (kernel.measurable _), smul_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
⊢ const α (Measure.bind μ ↑κ) = κ ∘ₖ const α μ
[PROOFSTEP]
ext a s hs
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(const α (Measure.bind μ ↑κ)) a) s = ↑↑(↑(κ ∘ₖ const α μ) a) s
[PROOFSTEP]
simp_rw [comp_apply' _ _ _ hs, const_apply, Measure.bind_apply hs (kernel.measurable _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : { x // x ∈ kernel α β }
μ : Measure α
a : α
⊢ ↑(κ ∘ₖ const α μ) a = Measure.bind μ ↑κ
[PROOFSTEP]
rw [← const_apply (μ.bind κ) a, const_bind_eq_comp_const κ μ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : { x // x ∈ kernel α α }
μ : Measure α
hκ : Invariant κ μ
⊢ κ ∘ₖ const α μ = const α μ
[PROOFSTEP]
rw [← const_bind_eq_comp_const κ μ, hκ.def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : { x // x ∈ kernel α α }
μ : Measure α
inst✝ : IsSFiniteKernel κ
hκ : Invariant κ μ
hη : Invariant η μ
⊢ Invariant (κ ∘ₖ η) μ
[PROOFSTEP]
cases' isEmpty_or_nonempty α with _ hα
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : { x // x ∈ kernel α α }
μ : Measure α
inst✝ : IsSFiniteKernel κ
hκ : Invariant κ μ
hη : Invariant η μ
h✝ : IsEmpty α
⊢ Invariant (κ ∘ₖ η) μ
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : { x // x ∈ kernel α α }
μ : Measure α
inst✝ : IsSFiniteKernel κ
hκ : Invariant κ μ
hη : Invariant η μ
hα : Nonempty α
⊢ Invariant (κ ∘ₖ η) μ
[PROOFSTEP]
simp_rw [Invariant, ← comp_const_apply_eq_bind (κ ∘ₖ η) μ hα.some, comp_assoc, hη.comp_const, hκ.comp_const,
  const_apply]