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 ω) : ℝ))
          ω
⊢ ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)

Tactic:
have h2 ω : f (A.indicator 1 ω) =
      A.indicator (fun _ ↦ f 1) ω + Aᶜ.indicator (fun _ ↦ f 0) ω := by
    classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all
-- 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) ω)
c : ℝ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P

Tactic:
Integrable.of_bound ?_ (‖c‖ * ∏ s, ‖g s‖) (ae_of_all _ fun ω ↦ ?_)

Premises used: Norm.norm, HMul.hMul, Finset.univ, Finset.prod, MeasureTheory.ae_of_all, MeasureTheory.Integrable.of_bound
-- 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) ω)
c : ℝ
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
refine_2 : ∀ (ω : Ω), ‖c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)‖ ≤ ‖c‖ * ∏ s : S, ‖g s‖
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P

Tactic:
refine Integrable.of_bound ?_ (‖c‖ * ∏ s, ‖g s‖) (ae_of_all _ fun ω ↦ ?_)

Premises used: Norm.norm, HMul.hMul, Finset.univ, Finset.prod, MeasureTheory.ae_of_all, MeasureTheory.Integrable.of_bound
-- 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) ω)
c : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P

Tactic:
(Finset.aestronglyMeasurable_fun_prod _ fun s _ ↦
        (g s).continuous.aestronglyMeasurable.comp_aemeasurable (mX s)).const_mul _

Premises used: MeasureTheory.AEStronglyMeasurable.const_mul, BoundedContinuousFunction.continuous, MeasureTheory.AEStronglyMeasurable.comp_aemeasurable, Continuous.aestronglyMeasurable, Finset.aestronglyMeasurable_fun_prod
-- 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) ω)
c : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P

Tactic:
exact (Finset.aestronglyMeasurable_fun_prod _ fun s _ ↦
        (g s).continuous.aestronglyMeasurable.comp_aemeasurable (mX s)).const_mul _

Premises used: MeasureTheory.AEStronglyMeasurable.const_mul, BoundedContinuousFunction.continuous, MeasureTheory.AEStronglyMeasurable.comp_aemeasurable, Continuous.aestronglyMeasurable, Finset.aestronglyMeasurable_fun_prod
-- 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) ω)
c : ℝ
ω : Ω
refine_2 : ‖c‖ * ∏ b : S, norm (E := ℝ) ((g b : (a : E b) → ℝ) (X b ω) : ℝ) ≤ ‖c‖ * ∏ s : S, ‖g s‖
⊢ ‖c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)‖ ≤ ‖c‖ * ∏ s : S, ‖g s‖

Tactic:
rw [norm_mul, norm_prod]

Premises used: norm_mul, norm_prod
-- 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) ω)
c : ℝ
ω : Ω
refine_2 :
  ∀ (s : S), Membership.mem (γ := Finset S) Finset.univ s → norm (E := ℝ) ((g s : (a : E s) → ℝ) (X s ω) : ℝ) ≤ ‖g s‖
⊢ ‖c‖ * ∏ b : S, norm (E := ℝ) ((g b : (a : E b) → ℝ) (X b ω) : ℝ) ≤ ‖c‖ * ∏ s : S, ‖g s‖

Tactic:
gcongr with s
-- 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) ω)
c : ℝ
ω : Ω
s : S
h_1 : Membership.mem (γ := Finset S) Finset.univ s
⊢ norm (E := ℝ) ((g s : (a : E s) → ℝ) (X s ω) : ℝ) ≤ ‖g s‖

Tactic:
(g s).norm_coe_le_norm _

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- 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) ω)
c : ℝ
ω : Ω
s : S
h_1 : Membership.mem (γ := Finset S) Finset.univ s
⊢ norm (E := ℝ) ((g s : (a : E s) → ℝ) (X s ω) : ℝ) ≤ ‖g s‖

Tactic:
exact (g s).norm_coe_le_norm _

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- 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) ω)
⊢ ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P

Tactic:
have hg {c : ℝ} : Integrable (fun ω ↦ c * ∏ s, g s (X s ω)) P := by
    refine Integrable.of_bound ?_ (‖c‖ * ∏ s, ‖g s‖) (ae_of_all _ fun ω ↦ ?_)
    · exact (Finset.aestronglyMeasurable_fun_prod _ fun s _ ↦
        (g s).continuous.aestronglyMeasurable.comp_aemeasurable (mX s)).const_mul _
    · rw [norm_mul, norm_prod]
      gcongr with s
      exact (g s).norm_coe_le_norm _
-- 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
simp_rw :
  ∫ (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) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          x ∂P =
    HMul.hMul (α := ℝ)
      (∫ (x : Ω),
        HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) x)
          (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) x) ∂P)
      (∫ (x : Ω), ∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) ∂P)
⊢ ∫ (x : Ω),
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (Function.comp (β := ℝ) (⇑f : (a : ℝ) → ℝ) (A.indicator 1))
        (∏ t : S, (⇑(g t) : (a : E t) → ℝ) ∘ X t) x ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), Function.comp (β := ℝ) (⇑f : (a : ℝ) → ℝ) (A.indicator 1) x ∂P)
      (∫ (x : Ω), (∏ t : S, (⇑(g t) : (a : E t) → ℝ) ∘ X t) x ∂P)

Tactic:
simp_rw [Pi.mul_apply, Finset.prod_apply, Function.comp_apply, h1, h2]

Premises used: Pi.mul_apply, Finset.prod_apply, Function.comp_apply
-- 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
simp :
  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
⊢ HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)
          (∫ (a : Ω), ∏ x : S, (g x : (a : E x) → ℝ) (X x a) ∂P : ℝ) -
      HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) =
    (HSMul.hSMul (β := ℝ) ((P.restrict A).real Set.univ) ((f : (a : ℝ) → ℝ) 1 : ℝ) +
        HSMul.hSMul (β := ℝ) ((P.restrict Aᶜ).real Set.univ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) *
      ∫ (x : Ω), ∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) ∂P

Tactic:
simp [measureReal_compl₀ mA]

Premises used: MeasureTheory.measureReal_compl₀