awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : Fintype S
inst_9 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
funProp : ∀ (i : S), Membership.mem (γ := Finset S) Finset.univ i → inst_1 i ≤ inst_1 i
funProp₁ :
  ∀ (i : S),
    Membership.mem (γ := Finset S) Finset.univ i →
      MeasurableEmbedding (β := ℝ) fun (a1 : E i) ↦ (f i : (a : E i) → ℝ) a1
funProp₂ : inst_5 ≤ inst_5
funProp₃ : MeasurableEmbedding (β := ℝ) fun (a0 : H) ↦ (g : (a : H) → ℝ) a0
⊢ Measurable (β := ℝ) fun (p : ((i : S) → E i) × H) ↦
    HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i) : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : Fintype S
inst_9 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Prod.instMeasurableSpace)
    (fun (p : ((i : S) → E i) × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i) : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ))
    (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, U ω)) P)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsFiniteMeasure P
inst_9 : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)
              ((g : (a : H) → ℝ) (U ω) : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
have : ∀ (this : Fintype S), (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] U
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] U

Tactic:
have := Fintype.ofFinite S
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsFiniteMeasure P
inst_9 : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)
              ((g : (a : H) → ℝ) (U ω) : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
this : Fintype S
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] U

Tactic:
pi_indepFun_of_prod_bcf mX mU fun f g ↦ ?_

Premises used: pi_indepFun_of_prod_bcf
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsFiniteMeasure P
inst_9 : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)
              ((g : (a : H) → ℝ) (U ω) : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
this : Fintype S
refine :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] U

Tactic:
refine pi_indepFun_of_prod_bcf mX mU fun f g ↦ ?_

Premises used: pi_indepFun_of_prod_bcf
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsFiniteMeasure P
inst_9 : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)
              ((g : (a : H) → ℝ) (U ω) : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
g : H →ᵇ ℝ
s : S
⊢ Continuous (X := (s : S) → E s) (Function.eval (β := E) s)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsFiniteMeasure P
inst_9 : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)
              ((g : (a : H) → ℝ) (U ω) : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
g : H →ᵇ ℝ
h₁ :
  ∀ (x x : Ω),
    HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x =
      HMul.hMul (α := ℝ) (β := ℝ)
        ((∏ s : S, (f s).compContinuous { toFun := Function.eval (β := E) s, continuous_toFun := ⋯ } :
              (a : (s : S) → E s) → ℝ)
            fun (x_1 : S) ↦ X x_1 x :
          ℝ)
        ((g : (a : H) → ℝ) (U x) : ℝ)
h₂ :
  ∀ (x x : Ω),
    Eq (α := ℝ) ((∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x : ℝ)
      ((∏ s : S, (f s).compContinuous { toFun := Function.eval (β := E) s, continuous_toFun := ⋯ } :
            (a : (s : S) → E s) → ℝ)
          fun (x_1 : S) ↦ X x_1 x :
        ℝ)
⊢ ∫ (x : Ω),
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
      (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)

Tactic:
convert! h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩) g

Premises used: Finset.univ, ContinuousMap.mk, Function.eval, BoundedContinuousFunction.compContinuous, Finset.prod
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsFiniteMeasure P
inst_9 : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)
              ((g : (a : H) → ℝ) (U ω) : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
g : H →ᵇ ℝ
x x_1 : Ω
⊢ HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x_1 =
    HMul.hMul (α := ℝ) (β := ℝ)
      ((∏ s : S, (f s).compContinuous { toFun := Function.eval (β := E) s, continuous_toFun := ⋯ } :
            (a : (s : S) → E s) → ℝ)
          fun (x : S) ↦ X x x_1 :
        ℝ)
      ((g : (a : H) → ℝ) (U x_1) : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : IsFiniteMeasure P
inst_9 : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)
              ((g : (a : H) → ℝ) (U ω) : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω : ℝ)) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
g : H →ᵇ ℝ
x x_1 : Ω
⊢ Eq (α := ℝ) ((∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x_1 : ℝ)
    ((∏ s : S, (f s).compContinuous { toFun := Function.eval (β := E) s, continuous_toFun := ⋯ } :
          (a : (s : S) → E s) → ℝ)
        fun (x : S) ↦ X x x_1 :
      ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
rw : Eq (α := Measure (G × H)) (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) (Measure.prod (map Z P) (map U P))
⊢ Z ⟂ᵢ[P] U

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map mZ mU]

Premises used: ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
⊢ Eq (α := Measure (G × H)) (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) (Measure.prod (map Z P) (map U P))

Tactic:
eq_prod_of_integral_mul_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.eq_prod_of_integral_mul_boundedContinuousFunction
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
refine :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) fun (p : G × H) ↦
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
      HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_1 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
        (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
⊢ Eq (α := Measure (G × H)) (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) (Measure.prod (map Z P) (map U P))

Tactic:
refine eq_prod_of_integral_mul_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.eq_prod_of_integral_mul_boundedContinuousFunction
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
rw :
  ∫ (x : Ω), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, U x).1 : ℝ) ((g : (a : H) → ℝ) (Z x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂P) (∫ (x : Ω), (g : (a : H) → ℝ) (U x) ∂P)
hφ : AEMeasurable U P
hfm : AEStronglyMeasurable (β := ℝ) (m₀ := inst_5) (⇑g : (a : H) → ℝ) (map U P)
hφ₁ : AEMeasurable Z P
hfm₁ : AEStronglyMeasurable (β := ℝ) (m₀ := inst_1) (⇑f : (a : G) → ℝ) (map Z P)
hφ₂ : AEMeasurable (β := G × H) (fun (ω : Ω) ↦ (Z ω, U ω)) P
hfm₂ :
  AEStronglyMeasurable (β := ℝ) (m₀ := Prod.instMeasurableSpace)
    (fun (p : G × H) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ))
    (map (fun (ω : Ω) ↦ (Z ω, U ω)) P)
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) fun (p : G × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_1 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)

Tactic:
rw [integral_map, integral_map, integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ ∫ (x : Ω), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, U x).1 : ℝ) ((g : (a : H) → ℝ) (Z x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂P) (∫ (x : Ω), (g : (a : H) → ℝ) (U x) ∂P)

Tactic:
h f g
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ ∫ (x : Ω), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, U x).1 : ℝ) ((g : (a : H) → ℝ) (Z x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂P) (∫ (x : Ω), (g : (a : H) → ℝ) (U x) ∂P)

Tactic:
exact h f g
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable U P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := inst_5) (⇑g : (a : H) → ℝ) (map U P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable Z P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := inst_1) (⇑f : (a : G) → ℝ) (map Z P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable (β := G × H) (fun (ω : Ω) ↦ (Z ω, U ω)) P

Tactic:
fun_prop