Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ ∫ (x : Ω), f (Z x, U x).1 * g (Z x, U x).2 ∂P = (∫ (x : Ω), f (Z x) ∂P) * ∫ (t : H), g t ∂map U P

pp: case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable Z P

pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (⇑f) (map Z P)

pp: case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable (fun ω ↦ (Z ω, U ω)) P

pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun p ↦ f p.1 * g p.2) (map (fun ω ↦ (Z ω, U ω)) P)

Tactic:
integral_map

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ ∫ (x : Ω), f (Z x, U x).1 * g (Z x, U x).2 ∂P = (∫ (x : Ω), f (Z x) ∂P) * ∫ (x : Ω), g (U x) ∂P

case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable U P

case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (⇑g) (map U P)

case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable Z P

case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (⇑f) (map Z P)

case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable (fun ω ↦ (Z ω, U ω)) P

case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun p ↦ f p.1 * g p.2) (map (fun ω ↦ (Z ω, U ω)) P)