[GOAL]
G : Type u_1
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableMul G
g : G
⊢ Measurable fun h => h / g
[PROOFSTEP]
simp_rw [div_eq_mul_inv, measurable_mul_const]
[GOAL]
M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
n : ℕ
⊢ Measurable fun x => (x, n).fst ^ (x, n).snd
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
⊢ Measurable fun x => (x, Nat.zero).fst ^ (x, Nat.zero).snd
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, ← Pi.one_def, measurable_one]
[GOAL]
case succ
M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
n : ℕ
ih : Measurable fun x => (x, n).fst ^ (x, n).snd
⊢ Measurable fun x => (x, Nat.succ n).fst ^ (x, Nat.succ n).snd
[PROOFSTEP]
simp only [pow_succ]
[GOAL]
case succ
M : Type u_1
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
n : ℕ
ih : Measurable fun x => (x, n).fst ^ (x, n).snd
⊢ Measurable fun x => x * x ^ n
[PROOFSTEP]
exact measurable_id.mul ih
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ MeasurableSet {x | f x = g x}
[PROOFSTEP]
suffices h_set_eq : {x : α | f x = g x} = {x | (f - g) x = (0 : E)}
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
h_set_eq : {x | f x = g x} = {x | (f - g) x = 0}
⊢ MeasurableSet {x | f x = g x}
[PROOFSTEP]
rw [h_set_eq]
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
h_set_eq : {x | f x = g x} = {x | (f - g) x = 0}
⊢ MeasurableSet {x | (f - g) x = 0}
[PROOFSTEP]
exact (hf.sub hg) measurableSet_eq
[GOAL]
case h_set_eq
G : Type u_1
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ {x | f x = g x} = {x | (f - g) x = 0}
[PROOFSTEP]
ext
[GOAL]
case h_set_eq.h
G : Type u_1
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : Measurable f
hg : Measurable g
x✝ : α
⊢ x✝ ∈ {x | f x = g x} ↔ x✝ ∈ {x | (f - g) x = 0}
[PROOFSTEP]
simp_rw [Set.mem_setOf_eq, Pi.sub_apply, sub_eq_zero]
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
⊢ NullMeasurableSet {x | f x = g x}
[PROOFSTEP]
apply (measurableSet_eq_fun hf.measurable_mk hg.measurable_mk).nullMeasurableSet.congr
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
⊢ {x | AEMeasurable.mk f hf x = AEMeasurable.mk g hg x} =ᵐ[μ] {x | f x = g x}
[PROOFSTEP]
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx
[GOAL]
case h
G : Type u_1
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ setOf (fun x => AEMeasurable.mk f hf x = AEMeasurable.mk g hg x) x = setOf (fun x => f x = g x) x
[PROOFSTEP]
change (hf.mk f x = hg.mk g x) = (f x = g x)
[GOAL]
case h
G : Type u_1
α : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f
hg : AEMeasurable g
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ (AEMeasurable.mk f hf x = AEMeasurable.mk g hg x) = (f x = g x)
[PROOFSTEP]
simp only [hfx, hgx]
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ MeasurableSet {x | f x = g x}
[PROOFSTEP]
have : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j} :=
  by
  ext1 x
  simp only [Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff, exists_eq_right']
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
⊢ {x | f x = g x} = ⋃ (j : E), {x | f x = j} ∩ {x | g x = j}
[PROOFSTEP]
ext1 x
[GOAL]
case h
G : Type u_1
α : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
x : α
⊢ x ∈ {x | f x = g x} ↔ x ∈ ⋃ (j : E), {x | f x = j} ∩ {x | g x = j}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff, exists_eq_right']
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ (j : E), {x | f x = j} ∩ {x | g x = j}
⊢ MeasurableSet {x | f x = g x}
[PROOFSTEP]
rw [this]
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ (j : E), {x | f x = j} ∩ {x | g x = j}
⊢ MeasurableSet (⋃ (j : E), {x | f x = j} ∩ {x | g x = j})
[PROOFSTEP]
refine' MeasurableSet.iUnion fun j => MeasurableSet.inter _ _
[GOAL]
case refine'_1
G : Type u_1
α : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ (j : E), {x | f x = j} ∩ {x | g x = j}
j : E
⊢ MeasurableSet {x | f x = j}
[PROOFSTEP]
exact hf (measurableSet_singleton j)
[GOAL]
case refine'_2
G : Type u_1
α : Type u_2
inst✝⁴ : MeasurableSpace G
inst✝³ : Div G
m✝ : MeasurableSpace α
f✝ g✝ : α → G
μ : Measure α
m : MeasurableSpace α
E : Type u_3
inst✝² : MeasurableSpace E
inst✝¹ : MeasurableSingletonClass E
inst✝ : Countable E
f g : α → E
hf : Measurable f
hg : Measurable g
this : {x | f x = g x} = ⋃ (j : E), {x | f x = j} ∩ {x | g x = j}
j : E
⊢ MeasurableSet {x | g x = j}
[PROOFSTEP]
exact hg (measurableSet_singleton j)
[GOAL]
G : Type u_1
α✝ : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α✝
f✝ g✝ : α✝ → G
μ✝ : Measure α✝
α : Type u_3
E : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
hm : m ≤ m0
f g : α → E
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ f =ᵐ[Measure.trim μ hm] g
[PROOFSTEP]
rwa [Filter.EventuallyEq, @ae_iff _ m, trim_measurableSet_eq hm _]
[GOAL]
G : Type u_1
α✝ : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Div G
m✝ : MeasurableSpace α✝
f✝ g✝ : α✝ → G
μ✝ : Measure α✝
α : Type u_3
E : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
hm : m ≤ m0
f g : α → E
hf : Measurable f
hg : Measurable g
hfg : f =ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a = g a}
[PROOFSTEP]
exact @MeasurableSet.compl α _ m (@measurableSet_eq_fun α m E _ _ _ _ _ _ hf hg)
[GOAL]
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c : G
⊢ Measurable fun x => c / x
[PROOFSTEP]
convert measurable_inv.const_mul c using 1
[GOAL]
case h.e'_5
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c : G
⊢ (fun x => c / x) = fun x => c * x⁻¹
[PROOFSTEP]
ext1
[GOAL]
case h.e'_5.h
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c x✝ : G
⊢ c / x✝ = c * x✝⁻¹
[PROOFSTEP]
apply div_eq_mul_inv
[GOAL]
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c : G
⊢ Measurable fun x => x / c
[PROOFSTEP]
convert measurable_id.mul_const c⁻¹ using 1
[GOAL]
case h.e'_5
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c : G
⊢ (fun x => x / c) = fun x => id x * c⁻¹
[PROOFSTEP]
ext1
[GOAL]
case h.e'_5.h
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul G
inst✝ : MeasurableInv G
c x✝ : G
⊢ x✝ / c = id x✝ * c⁻¹
[PROOFSTEP]
apply div_eq_mul_inv
[GOAL]
G✝ : Type u_1
α : Type u_2
inst✝⁵ : Inv G✝
inst✝⁴ : MeasurableSpace G✝
inst✝³ : MeasurableInv G✝
m : MeasurableSpace α
f✝ : α → G✝
μ : Measure α
G : Type u_3
inst✝² : Group G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableInv G
f : α → G
h : Measurable fun x => (f x)⁻¹
⊢ Measurable f
[PROOFSTEP]
simpa only [inv_inv] using h.inv
[GOAL]
G✝ : Type u_1
α : Type u_2
inst✝⁵ : Inv G✝
inst✝⁴ : MeasurableSpace G✝
inst✝³ : MeasurableInv G✝
m : MeasurableSpace α
f✝ : α → G✝
μ : Measure α
G : Type u_3
inst✝² : Group G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableInv G
f : α → G
h : AEMeasurable fun x => (f x)⁻¹
⊢ AEMeasurable f
[PROOFSTEP]
simpa only [inv_inv] using h.inv
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁵ : Inv G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableInv G
m : MeasurableSpace α
f✝ : α → G
μ : Measure α
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : MeasurableSpace G₀
inst✝ : MeasurableInv G₀
f : α → G₀
h : Measurable fun x => (f x)⁻¹
⊢ Measurable f
[PROOFSTEP]
simpa only [inv_inv] using h.inv
[GOAL]
G : Type u_1
α : Type u_2
inst✝⁵ : Inv G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableInv G
m : MeasurableSpace α
f✝ : α → G
μ : Measure α
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : MeasurableSpace G₀
inst✝ : MeasurableInv G₀
f : α → G₀
h : AEMeasurable fun x => (f x)⁻¹
⊢ AEMeasurable f
[PROOFSTEP]
simpa only [inv_inv] using h.inv
[GOAL]
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℤ
⊢ Measurable fun x => (x, n).fst ^ (x, n).snd
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x => (x, Int.ofNat n).fst ^ (x, Int.ofNat n).snd
[PROOFSTEP]
simp_rw [Int.ofNat_eq_coe, zpow_ofNat]
[GOAL]
case ofNat
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x => x ^ n
[PROOFSTEP]
exact measurable_id.pow_const _
[GOAL]
case negSucc
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x => (x, Int.negSucc n).fst ^ (x, Int.negSucc n).snd
[PROOFSTEP]
simp_rw [zpow_negSucc]
[GOAL]
case negSucc
G : Type u
inst✝³ : DivInvMonoid G
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
n : ℕ
⊢ Measurable fun x => (x ^ (n + 1))⁻¹
[PROOFSTEP]
exact (measurable_id.pow_const (n + 1)).inv
[GOAL]
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
⊢ Measurable fun p => p.fst / p.snd
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableMul₂ G
inst✝ : MeasurableInv G
⊢ Measurable fun p => p.fst * p.snd⁻¹
[PROOFSTEP]
exact measurable_fst.mul measurable_snd.inv
[GOAL]
M : Type ?u.442912
α : Type ?u.442915
inst✝⁴ : MeasurableSpace M
inst✝³ : MeasurableSpace α
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : MeasurableSMul M α
s : Submonoid M
c : { x // x ∈ s }
⊢ Measurable ((fun x x_1 => x • x_1) c)
[PROOFSTEP]
simpa only using measurable_const_smul (c : M)
[GOAL]
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁶ : MeasurableSpace M✝
inst✝⁵ : MeasurableSpace β
inst✝⁴ : _root_.SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝³ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
⊢ Measurable (Function.uncurry fun x x_1 => x • x_1)
[PROOFSTEP]
suffices Measurable fun p : M × ℕ => p.2 • p.1 by apply this.comp measurable_swap
[GOAL]
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁶ : MeasurableSpace M✝
inst✝⁵ : MeasurableSpace β
inst✝⁴ : _root_.SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝³ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
this : Measurable fun p => p.snd • p.fst
⊢ Measurable (Function.uncurry fun x x_1 => x • x_1)
[PROOFSTEP]
apply this.comp measurable_swap
[GOAL]
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁶ : MeasurableSpace M✝
inst✝⁵ : MeasurableSpace β
inst✝⁴ : _root_.SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝³ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
⊢ Measurable fun p => p.snd • p.fst
[PROOFSTEP]
refine' measurable_from_prod_countable fun n => _
[GOAL]
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁶ : MeasurableSpace M✝
inst✝⁵ : MeasurableSpace β
inst✝⁴ : _root_.SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝³ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
n : ℕ
⊢ Measurable fun x => (x, n).snd • (x, n).fst
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁶ : MeasurableSpace M✝
inst✝⁵ : MeasurableSpace β
inst✝⁴ : _root_.SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝³ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
⊢ Measurable fun x => (x, Nat.zero).snd • (x, Nat.zero).fst
[PROOFSTEP]
simp only [Nat.zero_eq, zero_smul, ← Pi.zero_def, measurable_zero]
[GOAL]
case succ
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁶ : MeasurableSpace M✝
inst✝⁵ : MeasurableSpace β
inst✝⁴ : _root_.SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝³ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
n : ℕ
ih : Measurable fun x => (x, n).snd • (x, n).fst
⊢ Measurable fun x => (x, Nat.succ n).snd • (x, Nat.succ n).fst
[PROOFSTEP]
simp only [succ_nsmul]
[GOAL]
case succ
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁶ : MeasurableSpace M✝
inst✝⁵ : MeasurableSpace β
inst✝⁴ : _root_.SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝³ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableAdd₂ M
n : ℕ
ih : Measurable fun x => (x, n).snd • (x, n).fst
⊢ Measurable fun x => x + n • x
[PROOFSTEP]
exact measurable_id.add ih
[GOAL]
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁷ : MeasurableSpace M✝
inst✝⁶ : MeasurableSpace β
inst✝⁵ : SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝⁴ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
⊢ Measurable (Function.uncurry fun x x_1 => x • x_1)
[PROOFSTEP]
suffices Measurable fun p : M × ℤ => p.2 • p.1 by apply this.comp measurable_swap
[GOAL]
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁷ : MeasurableSpace M✝
inst✝⁶ : MeasurableSpace β
inst✝⁵ : SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝⁴ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
this : Measurable fun p => p.snd • p.fst
⊢ Measurable (Function.uncurry fun x x_1 => x • x_1)
[PROOFSTEP]
apply this.comp measurable_swap
[GOAL]
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁷ : MeasurableSpace M✝
inst✝⁶ : MeasurableSpace β
inst✝⁵ : SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝⁴ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
⊢ Measurable fun p => p.snd • p.fst
[PROOFSTEP]
refine' measurable_from_prod_countable fun n => _
[GOAL]
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁷ : MeasurableSpace M✝
inst✝⁶ : MeasurableSpace β
inst✝⁵ : SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝⁴ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
n : ℤ
⊢ Measurable fun x => (x, n).snd • (x, n).fst
[PROOFSTEP]
induction' n with n n ih
[GOAL]
case ofNat
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁷ : MeasurableSpace M✝
inst✝⁶ : MeasurableSpace β
inst✝⁵ : SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝⁴ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
n : ℕ
⊢ Measurable fun x => (x, Int.ofNat n).snd • (x, Int.ofNat n).fst
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, ofNat_zsmul]
[GOAL]
case ofNat
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁷ : MeasurableSpace M✝
inst✝⁶ : MeasurableSpace β
inst✝⁵ : SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝⁴ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
n : ℕ
⊢ Measurable fun x => n • x
[PROOFSTEP]
exact measurable_const_smul _
[GOAL]
case negSucc
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁷ : MeasurableSpace M✝
inst✝⁶ : MeasurableSpace β
inst✝⁵ : SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝⁴ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
n : ℕ
⊢ Measurable fun x => (x, Int.negSucc n).snd • (x, Int.negSucc n).fst
[PROOFSTEP]
simp only [negSucc_zsmul]
[GOAL]
case negSucc
M✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝⁷ : MeasurableSpace M✝
inst✝⁶ : MeasurableSpace β
inst✝⁵ : SMul M✝ β
m : MeasurableSpace α
f : α → M✝
g : α → β
inst✝⁴ : MeasurableSMul M✝ β
μ : Measure α
M : Type u_4
inst✝³ : SubNegMonoid M
inst✝² : MeasurableSpace M
inst✝¹ : MeasurableAdd₂ M
inst✝ : MeasurableNeg M
n : ℕ
⊢ Measurable fun x => -((n + 1) • x)
[PROOFSTEP]
exact (measurable_const_smul _).neg
[GOAL]
M : Type u_1
β : Type u_2
α : Type u_3
inst✝⁹ : MeasurableSpace M
inst✝⁸ : MeasurableSpace β
inst✝⁷ : Monoid M
inst✝⁶ : MulAction M β
inst✝⁵ : MeasurableSMul M β
inst✝⁴ : MeasurableSpace α
f : α → β
μ : Measure α
G : Type u_4
inst✝³ : Group G
inst✝² : MeasurableSpace G
inst✝¹ : MulAction G β
inst✝ : MeasurableSMul G β
c : G
h : Measurable fun x => c • f x
⊢ Measurable f
[PROOFSTEP]
simpa only [inv_smul_smul] using h.const_smul' c⁻¹
[GOAL]
M : Type u_1
β : Type u_2
α : Type u_3
inst✝⁹ : MeasurableSpace M
inst✝⁸ : MeasurableSpace β
inst✝⁷ : Monoid M
inst✝⁶ : MulAction M β
inst✝⁵ : MeasurableSMul M β
inst✝⁴ : MeasurableSpace α
f : α → β
μ : Measure α
G : Type u_4
inst✝³ : Group G
inst✝² : MeasurableSpace G
inst✝¹ : MulAction G β
inst✝ : MeasurableSMul G β
c : G
h : AEMeasurable fun x => c • f x
⊢ AEMeasurable f
[PROOFSTEP]
simpa only [inv_smul_smul] using h.const_smul' c⁻¹
[GOAL]
M : Type ?u.567803
α : Type ?u.567806
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : SMul M α
inst✝² : SMul Mᵐᵒᵖ α
inst✝¹ : IsCentralScalar M α
inst✝ : MeasurableSMul M α
c : M
⊢ Measurable fun x => MulOpposite.op c • x
[PROOFSTEP]
simpa only [op_smul_eq_smul] using measurable_const_smul c
[GOAL]
M : Type ?u.567803
α : Type ?u.567806
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : SMul M α
inst✝² : SMul Mᵐᵒᵖ α
inst✝¹ : IsCentralScalar M α
inst✝ : MeasurableSMul M α
x : α
⊢ Measurable fun c => MulOpposite.op (unop c) • x
[PROOFSTEP]
simpa only [op_smul_eq_smul] using (measurable_smul_const x).comp measurable_mul_unop
[GOAL]
M : Type ?u.570007
α : Type ?u.570010
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : SMul M α
inst✝² : SMul Mᵐᵒᵖ α
inst✝¹ : IsCentralScalar M α
inst✝ : MeasurableSMul₂ M α
⊢ Measurable fun x => MulOpposite.op (unop x.fst) • x.snd
[PROOFSTEP]
simp_rw [op_smul_eq_smul]
[GOAL]
M : Type ?u.570007
α : Type ?u.570010
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : SMul M α
inst✝² : SMul Mᵐᵒᵖ α
inst✝¹ : IsCentralScalar M α
inst✝ : MeasurableSMul₂ M α
⊢ Measurable fun x => unop x.fst • x.snd
[PROOFSTEP]
refine' (measurable_mul_unop.comp measurable_fst).smul measurable_snd
[GOAL]
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ (f : α → M), f ∈ l → Measurable f
⊢ Measurable (prod l)
[PROOFSTEP]
induction' l with f l ihl
[GOAL]
case nil
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l → Measurable f
hl : ∀ (f : α → M), f ∈ [] → Measurable f
⊢ Measurable (prod [])
[PROOFSTEP]
exact measurable_one
[GOAL]
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → Measurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → Measurable f) → Measurable (prod l)
hl : ∀ (f_1 : α → M), f_1 ∈ f :: l → Measurable f_1
⊢ Measurable (prod (f :: l))
[PROOFSTEP]
rw [List.forall_mem_cons] at hl
[GOAL]
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → Measurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → Measurable f) → Measurable (prod l)
hl : Measurable f ∧ ∀ (x : α → M), x ∈ l → Measurable x
⊢ Measurable (prod (f :: l))
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → Measurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → Measurable f) → Measurable (prod l)
hl : Measurable f ∧ ∀ (x : α → M), x ∈ l → Measurable x
⊢ Measurable (f * prod l)
[PROOFSTEP]
exact hl.1.mul (ihl hl.2)
[GOAL]
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ (f : α → M), f ∈ l → AEMeasurable f
⊢ AEMeasurable (prod l)
[PROOFSTEP]
induction' l with f l ihl
[GOAL]
case nil
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l → AEMeasurable f
hl : ∀ (f : α → M), f ∈ [] → AEMeasurable f
⊢ AEMeasurable (prod [])
[PROOFSTEP]
exact aemeasurable_one
[GOAL]
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → AEMeasurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → AEMeasurable f) → AEMeasurable (prod l)
hl : ∀ (f_1 : α → M), f_1 ∈ f :: l → AEMeasurable f_1
⊢ AEMeasurable (prod (f :: l))
[PROOFSTEP]
rw [List.forall_mem_cons] at hl
[GOAL]
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → AEMeasurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → AEMeasurable f) → AEMeasurable (prod l)
hl : AEMeasurable f ∧ ∀ (x : α → M), x ∈ l → AEMeasurable x
⊢ AEMeasurable (prod (f :: l))
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
case cons
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l✝ : List (α → M)
hl✝ : ∀ (f : α → M), f ∈ l✝ → AEMeasurable f
f : α → M
l : List (α → M)
ihl : (∀ (f : α → M), f ∈ l → AEMeasurable f) → AEMeasurable (prod l)
hl : AEMeasurable f ∧ ∀ (x : α → M), x ∈ l → AEMeasurable x
⊢ AEMeasurable (f * prod l)
[PROOFSTEP]
exact hl.1.mul (ihl hl.2)
[GOAL]
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ (f : α → M), f ∈ l → Measurable f
⊢ Measurable fun x => prod (map (fun f => f x) l)
[PROOFSTEP]
simpa only [← Pi.list_prod_apply] using l.measurable_prod' hl
[GOAL]
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ (f : α → M), f ∈ l → AEMeasurable f
⊢ AEMeasurable fun x => prod (map (fun f => f x) l)
[PROOFSTEP]
simpa only [← Pi.list_prod_apply] using l.aemeasurable_prod' hl
[GOAL]
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
l : Multiset (α → M)
hl : ∀ (f : α → M), f ∈ l → Measurable f
⊢ Measurable (prod l)
[PROOFSTEP]
rcases l with ⟨l⟩
[GOAL]
case mk
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → Measurable f
⊢ Measurable (prod (Quot.mk Setoid.r l))
[PROOFSTEP]
simpa using l.measurable_prod' (by simpa using hl)
[GOAL]
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → Measurable f
⊢ ∀ (f : α → M), f ∈ l → Measurable f
[PROOFSTEP]
simpa using hl
[GOAL]
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
l : Multiset (α → M)
hl : ∀ (f : α → M), f ∈ l → AEMeasurable f
⊢ AEMeasurable (prod l)
[PROOFSTEP]
rcases l with ⟨l⟩
[GOAL]
case mk
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → AEMeasurable f
⊢ AEMeasurable (prod (Quot.mk Setoid.r l))
[PROOFSTEP]
simpa using l.aemeasurable_prod' (by simpa using hl)
[GOAL]
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ (f : α → M), f ∈ Quot.mk Setoid.r l → AEMeasurable f
⊢ ∀ (f : α → M), f ∈ l → AEMeasurable f
[PROOFSTEP]
simpa using hl
[GOAL]
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
s : Multiset (α → M)
hs : ∀ (f : α → M), f ∈ s → Measurable f
⊢ Measurable fun x => prod (map (fun f => f x) s)
[PROOFSTEP]
simpa only [← Pi.multiset_prod_apply] using s.measurable_prod' hs
[GOAL]
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
s : Multiset (α → M)
hs : ∀ (f : α → M), f ∈ s → AEMeasurable f
⊢ AEMeasurable fun x => prod (map (fun f => f x) s)
[PROOFSTEP]
simpa only [← Pi.multiset_prod_apply] using s.aemeasurable_prod' hs
[GOAL]
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
s : Finset ι
hf : ∀ (i : ι), i ∈ s → Measurable (f i)
⊢ Measurable fun a => ∏ i in s, f i a
[PROOFSTEP]
simpa only [← Finset.prod_apply] using s.measurable_prod' hf
[GOAL]
M : Type u_1
ι : Type u_2
α : Type u_3
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
s : Finset ι
hf : ∀ (i : ι), i ∈ s → AEMeasurable (f i)
⊢ AEMeasurable fun a => ∏ i in s, f i a
[PROOFSTEP]
simpa only [← Finset.prod_apply] using s.aemeasurable_prod' hf