α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
have : Measurable fun p : α × γ => (f p.1, g p.1 p.2) := (hf.1.comp measurable_fst).prod_mk hgm
case inl
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
hf : MeasurePreserving f
hg : ∀ᵐ (x : α) ∂0, map (g x) μc = μd
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)

case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
rcases eq_or_ne μa 0 with (rfl | ha)
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
have sf : SigmaFinite μc := by
  rcases (ae_neBot.2 ha).nonempty_of_mem hg with ⟨x, hx : map (g x) μc = μd⟩
  exact SigmaFinite.of_map _ hgm.of_uncurry_left.aemeasurable (by rwa [hx])
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map (fun p => (f p.fst, g p.fst p.snd)) (Measure.prod μa μc)) (s ×ˢ t) = ↑↑μb s * ↑↑μd t
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
refine' ⟨this, (prod_eq fun s t hs ht => _).symm⟩
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(Measure.prod μa μc) ((fun p => (f p.fst, g p.fst p.snd)) ⁻¹' s ×ˢ t) = ↑↑μb s * ↑↑μd t
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map (fun p => (f p.fst, g p.fst p.snd)) (Measure.prod μa μc)) (s ×ˢ t) = ↑↑μb s * ↑↑μd t
rw [map_apply this (hs.prod ht)]
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (∫⁻ (x : α), ↑↑μc (Prod.mk x ⁻¹' ((fun p => (f p.fst, g p.fst p.snd)) ⁻¹' s ×ˢ t)) ∂μa) = ↑↑μb s * ↑↑μd t
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(Measure.prod μa μc) ((fun p => (f p.fst, g p.fst p.snd)) ⁻¹' s ×ˢ t) = ↑↑μb s * ↑↑μd t
refine' (prod_apply (this <| hs.prod ht)).trans _
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this✝ : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ᵐ (x : α) ∂μa, ↑↑μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun x => ↑↑μd t) x
⊢ (∫⁻ (x : α), ↑↑μc (Prod.mk x ⁻¹' ((fun p => (f p.fst, g p.fst p.snd)) ⁻¹' s ×ˢ t)) ∂μa) = ↑↑μb s * ↑↑μd t
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (∫⁻ (x : α), ↑↑μc (Prod.mk x ⁻¹' ((fun p => (f p.fst, g p.fst p.snd)) ⁻¹' s ×ˢ t)) ∂μa) = ↑↑μb s * ↑↑μd t
have : ∀ᵐ x ∂μa,
    μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun _ => μd t) x := by
  refine' hg.mono fun x hx => _
  subst hx
  simp only [mk_preimage_prod_right_fn_eq_if, indicator_apply, mem_preimage]
  split_ifs
  exacts [(map_apply hgm.of_uncurry_left ht).symm, measure_empty]
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this✝ : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ᵐ (x : α) ∂μa, ↑↑μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun x => ↑↑μd t) x
⊢ (∫⁻ (x : α), ↑↑μc ((fun x_1 => (f x, g x x_1)) ⁻¹' s ×ˢ t) ∂μa) = ↑↑μb s * ↑↑μd t
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this✝ : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ᵐ (x : α) ∂μa, ↑↑μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun x => ↑↑μd t) x
⊢ (∫⁻ (x : α), ↑↑μc (Prod.mk x ⁻¹' ((fun p => (f p.fst, g p.fst p.snd)) ⁻¹' s ×ˢ t)) ∂μa) = ↑↑μb s * ↑↑μd t
simp only [preimage_preimage]
no goals
case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this✝ : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ᵐ (x : α) ∂μa, ↑↑μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun x => ↑↑μd t) x
⊢ (∫⁻ (x : α), ↑↑μc ((fun x_1 => (f x, g x x_1)) ⁻¹' s ×ˢ t) ∂μa) = ↑↑μb s * ↑↑μd t
rw [lintegral_congr_ae this, lintegral_indicator _ (hf.1 hs), set_lintegral_const,
  hf.measure_preimage hs, mul_comm]
case inl
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
hf : MeasurePreserving f
hg : ∀ᵐ (x : α) ∂0, map (g x) μc = μd
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
case inl
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
hf : MeasurePreserving f
hg : ∀ᵐ (x : α) ∂0, map (g x) μc = μd
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
rw [← hf.map_eq, zero_prod, Measure.map_zero, zero_prod]
no goals
case inl
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
hf : MeasurePreserving f
hg : ∀ᵐ (x : α) ∂0, map (g x) μc = μd
⊢ MeasurePreserving fun p => (f p.fst, g p.fst p.snd)
exact ⟨this, by simp only [Measure.map_zero]⟩
no goals
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
hf : MeasurePreserving f
hg : ∀ᵐ (x : α) ∂0, map (g x) μc = μd
⊢ map (fun p => (f p.fst, g p.fst p.snd)) 0 = 0
simp only [Measure.map_zero]
case intro
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
x : α
hx : map (g x) μc = μd
⊢ SigmaFinite μc
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
⊢ SigmaFinite μc
rcases (ae_neBot.2 ha).nonempty_of_mem hg with ⟨x, hx : map (g x) μc = μd⟩
no goals
case intro
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
x : α
hx : map (g x) μc = μd
⊢ SigmaFinite μc
exact SigmaFinite.of_map _ hgm.of_uncurry_left.aemeasurable (by rwa [hx])
no goals
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
x : α
hx : map (g x) μc = μd
⊢ SigmaFinite (map (g ?m.4503261) μc)
rwa [hx]
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
hx : map (g x) μc = μd
⊢ ↑↑μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun x => ↑↑μd t) x
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (x : α) ∂μa, ↑↑μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun x => ↑↑μd t) x
refine' hg.mono fun x hx => _
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SigmaFinite μb
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
inst✝ : SigmaFinite (map (g x) μc)
hg : ∀ᵐ (x_1 : α) ∂μa, map (g x_1) μc = map (g x) μc
⊢ ↑↑μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun x_1 => ↑↑(map (g x) μc) t) x
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SigmaFinite μb
inst✝ : SigmaFinite μd
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (x : α) ∂μa, map (g x) μc = μd
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
hx : map (g x) μc = μd
⊢ ↑↑μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun x => ↑↑μd t) x
subst hx
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SigmaFinite μb
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
inst✝ : SigmaFinite (map (g x) μc)
hg : ∀ᵐ (x_1 : α) ∂μa, map (g x_1) μc = map (g x) μc
⊢ ↑↑μc (if f x ∈ s then (fun b => g x b) ⁻¹' t else ∅) = if f x ∈ s then ↑↑(map (g x) μc) t else 0
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SigmaFinite μb
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
inst✝ : SigmaFinite (map (g x) μc)
hg : ∀ᵐ (x_1 : α) ∂μa, map (g x_1) μc = map (g x) μc
⊢ ↑↑μc ((fun y => (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (fun x_1 => ↑↑(map (g x) μc) t) x
simp only [mk_preimage_prod_right_fn_eq_if, indicator_apply, mem_preimage]
case inl
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SigmaFinite μb
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
inst✝ : SigmaFinite (map (g x) μc)
hg : ∀ᵐ (x_1 : α) ∂μa, map (g x_1) μc = map (g x) μc
h✝ : f x ∈ s
⊢ ↑↑μc ((fun b => g x b) ⁻¹' t) = ↑↑(map (g x) μc) t

case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SigmaFinite μb
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
inst✝ : SigmaFinite (map (g x) μc)
hg : ∀ᵐ (x_1 : α) ∂μa, map (g x_1) μc = map (g x) μc
h✝ : ¬f x ∈ s
⊢ ↑↑μc ∅ = 0
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SigmaFinite μb
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
inst✝ : SigmaFinite (map (g x) μc)
hg : ∀ᵐ (x_1 : α) ∂μa, map (g x_1) μc = map (g x) μc
⊢ ↑↑μc (if f x ∈ s then (fun b => g x b) ⁻¹' t else ∅) = if f x ∈ s then ↑↑(map (g x) μc) t else 0
split_ifs
no goals
case inl
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SigmaFinite μb
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
inst✝ : SigmaFinite (map (g x) μc)
hg : ∀ᵐ (x_1 : α) ∂μa, map (g x_1) μc = map (g x) μc
h✝ : f x ∈ s
⊢ ↑↑μc ((fun b => g x b) ⁻¹' t) = ↑↑(map (g x) μc) t

case inr
α : Type u_3
α' : Type ?u.4501625
β : Type u_1
β' : Type ?u.4501631
γ : Type u_4
E : Type ?u.4501637
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
δ : Type u_2
inst✝² : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SigmaFinite μb
f : α → β
hf : MeasurePreserving f
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p => (f p.fst, g p.fst p.snd)
ha : μa ≠ 0
sf : SigmaFinite μc
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
x : α
inst✝ : SigmaFinite (map (g x) μc)
hg : ∀ᵐ (x_1 : α) ∂μa, map (g x_1) μc = map (g x) μc
h✝ : ¬f x ∈ s
⊢ ↑↑μc ∅ = 0
exacts [(map_apply hgm.of_uncurry_left ht).symm, measure_empty]