[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
