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
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)
          (∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P : ℝ) -
      HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) =
    (HMul.hMul (β := ℝ) (P.real A) ((f : (a : ℝ) → ℝ) 1 : ℝ) +
        HMul.hMul (β := ℝ) (1 - P.real A) ((f : (a : ℝ) → ℝ) 0 : ℝ)) *
      ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P

Tactic:
ring
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ) (A.indicator fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) P

Tactic:
(integrable_const _).indicator₀ mA

Premises used: MeasureTheory.Integrable.indicator₀
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ) (A.indicator fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) P

Tactic:
exact (integrable_const _).indicator₀ mA

Premises used: MeasureTheory.Integrable.indicator₀
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ) (Aᶜ.indicator fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) P

Tactic:
(integrable_const _).indicator₀ mA.compl

Premises used: MeasureTheory.NullMeasurableSet.compl, MeasureTheory.Integrable.indicator₀
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ) (Aᶜ.indicator fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) P

Tactic:
exact (integrable_const _).indicator₀ mA.compl

Premises used: MeasureTheory.NullMeasurableSet.compl, MeasureTheory.Integrable.indicator₀
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ)
    (A.indicator fun (ω : Ω) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
    P

Tactic:
hg.indicator₀ mA

Premises used: MeasureTheory.Integrable.indicator₀
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ)
    (A.indicator fun (ω : Ω) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
    P

Tactic:
exact hg.indicator₀ mA

Premises used: MeasureTheory.Integrable.indicator₀
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ)
    (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ x : S, (g x : (a : E x) → ℝ) (X x a) : ℝ)) P

Tactic:
hg
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ)
    (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ x : S, (g x : (a : E x) → ℝ) (X x a) : ℝ)) P

Tactic:
exact hg
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ)
    (fun (x : Ω) ↦
      A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          x +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) : ℝ))
    P

Tactic:
(hg.indicator₀ mA).add hg

Premises used: MeasureTheory.Integrable.indicator₀, MeasureTheory.Integrable.add
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ)
    (fun (x : Ω) ↦
      A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          x +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) : ℝ))
    P

Tactic:
exact (hg.indicator₀ mA).add hg

Premises used: MeasureTheory.Integrable.indicator₀, MeasureTheory.Integrable.add
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ)
    (A.indicator fun (ω : Ω) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
    P

Tactic:
hg.indicator₀ mA

Premises used: MeasureTheory.Integrable.indicator₀
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ Integrable (ε := ℝ)
    (A.indicator fun (ω : Ω) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
    P

Tactic:
exact hg.indicator₀ mA

Premises used: MeasureTheory.Integrable.indicator₀