awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (hypothesis)
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 →ᵇ ℝ
⊢ ∫ (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)
have 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 ω) : ℝ))
        ω
Tactic: have h1 ω : f (A.indicator 1 ω) * ∏ s, g s (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, g s (X s ω)) ω +
      f 0 * ∏ s, g s (X s ω) - A.indicator (fun ω ↦ f 0 * ∏ s, g s (X s ω)) ω := by
    classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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) ω)
have rw : (f : (a : ℝ) → ℝ) (if ω ∈ A then 1 ω else 0) =
  HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
    (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
Tactic: rw [Set.indicator_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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 : ℝ) → ℝ) (if ω ∈ A then 1 ω else 0) =
    HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
      (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
have pos : ω ∈ A →
  (f : (a : ℝ) → ℝ) (1 ω) =
    HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
      (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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 ω) : ℝ))
          ω
ω : Ω
pos :
  ω ∈ A →
    (f : (a : ℝ) → ℝ) (1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
⊢ (f : (a : ℝ) → ℝ) (if ω ∈ A then 1 ω else 0) =
    HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
      (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
have neg : ω ∉ A →
  (f : (a : ℝ) → ℝ) 0 =
    HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
      (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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) ω)
have rw : (f : (a : ℝ) → ℝ) (if ω ∈ A then 1 ω else 0) =
  HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
    (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
Tactic: classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (hypothesis)
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 ω) : ℝ))
          ω
⊢ ∫ (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)
have h2 : ∀ (ω : Ω),
  (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
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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
have refine_1 : AEStronglyMeasurable (β := ℝ) (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 ω ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
have refine_2 : ∀ (ω : Ω), ‖c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)‖ ≤ ‖c‖ * ∏ s : S, ‖g s‖
Tactic: refine Integrable.of_bound ?_ (‖c‖ * ∏ s, ‖g s‖) (ae_of_all _ fun ω ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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 : ℝ
ω : Ω
⊢ ‖c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)‖ ≤ ‖c‖ * ∏ s : S, ‖g s‖
have refine_2 : ‖c‖ * ∏ b : S, norm (E := ℝ) ((g b : (a : E b) → ℝ) (X b ω) : ℝ) ≤ ‖c‖ * ∏ s : S, ‖g s‖
Tactic: rw [norm_mul, norm_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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 : ℝ
ω : Ω
⊢ ‖c‖ * ∏ b : S, norm (E := ℝ) ((g b : (a : E b) → ℝ) (X b ω) : ℝ) ≤ ‖c‖ * ∏ s : S, ‖g s‖
have refine_2 : ∀ (s : S), Membership.mem (γ := Finset S) Finset.univ s → norm (E := ℝ) ((g s : (a : E s) → ℝ) (X s ω) : ℝ) ≤ ‖g s‖
Tactic: gcongr with s
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (hypothesis)
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) ω)
⊢ ∫ (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)
have hg : ∀ {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 _
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
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
⊢ ∫ (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)
have 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)
Tactic: simp_rw [Pi.mul_apply, Finset.prod_apply, Function.comp_apply, h1, h2]