awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ∫⁻ (ω : Ω), HMul.hMul (α := ℝ≥0∞) ((fun (x : Ω) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) ω) (T.indicator (fun (x : Ω) ↦ c) ω) ∂μ =
    (∫⁻ (ω : Ω), (fun (x : Ω) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have iSup : ∫⁻ (ω : Ω), ⨆ (i : ℕ), f i ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
  (∫⁻ (ω : Ω), ⨆ (n : ℕ), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
Tactic: simp_rw [iSup_mul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ∫⁻ (ω : Ω), ⨆ (i : ℕ), f i ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), ⨆ (n : ℕ), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have iSup : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : Ω), f n a * T.indicator (fun (x : Ω) ↦ c) a ∂μ)
  (⨆ (i : ℕ), (∫⁻ (a : Ω), f i a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ)
Tactic: rw [lintegral_iSup h_measM_f h_mono_f, lintegral_iSup, iSup_mul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
iSup :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : Ω), f n a * T.indicator (fun (x : Ω) ↦ c) a ∂μ)
    (⨆ (i : ℕ), (∫⁻ (a : Ω), f i a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ)
⊢ ∫⁻ (ω : Ω), ⨆ (i : ℕ), f i ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), ⨆ (n : ℕ), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have iSup₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (ω : Ω) ↦ f n ω * T.indicator (fun (x : Ω) ↦ c) ω
Tactic: rw [lintegral_iSup h_measM_f h_mono_f, lintegral_iSup, iSup_mul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
iSup :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : Ω), f n a * T.indicator (fun (x : Ω) ↦ c) a ∂μ)
    (⨆ (i : ℕ), (∫⁻ (a : Ω), f i a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ)
iSup₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (ω : Ω) ↦ f n ω * T.indicator (fun (x : Ω) ↦ c) ω
⊢ ∫⁻ (ω : Ω), ⨆ (i : ℕ), f i ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), ⨆ (n : ℕ), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
have iSup₂ : Monotone.{0, u_1} (β := Ω → ℝ≥0∞) fun (i : ℕ) (ω : Ω) ↦ f i ω * T.indicator (fun (x : Ω) ↦ c) ω
Tactic: rw [lintegral_iSup h_measM_f h_mono_f, lintegral_iSup, iSup_mul]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f g : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_meas_g : Measurable g
⊢ ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
have revert : ∀ {g : Ω → ℝ≥0∞} (h_meas_g : Measurable g), ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
Tactic: revert g
Cleared hypotheses: g, h_meas_g
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
⊢ ∀ {g : Ω → ℝ≥0∞} (h_meas_g : Measurable g), ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
have h_measM_f : Measurable f
Tactic: have h_measM_f : Measurable f := h_meas_f.mono hMf le_rfl
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
⊢ ∀ {g : Ω → ℝ≥0∞} (h_meas_g : Measurable g), ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
have indicator : ∀ (c : ℝ≥0∞) ⦃s : Set Ω⦄,
  MeasurableSet s →
    ∫⁻ (ω : Ω), f ω * s.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c) ω ∂μ
Tactic: apply @Measurable.ennreal_induction _ Mg
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), f ω * s.indicator (fun (x : Ω) ↦ c) ω ∂μ =
        (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c) ω ∂μ
⊢ ∀ {g : Ω → ℝ≥0∞} (h_meas_g : Measurable g), ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
have add : ∀ ⦃f_1 g : Ω → ℝ≥0∞⦄,
  Disjoint (Function.support f_1) (Function.support g) →
    Measurable f_1 →
      Measurable g →
        ∫⁻ (ω : Ω), f ω * f_1 ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 ω ∂μ →
          ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
            ∫⁻ (ω : Ω), f ω * (f_1 + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f_1 + g) ω ∂μ
Tactic: apply @Measurable.ennreal_induction _ Mg
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), f ω * s.indicator (fun (x : Ω) ↦ c) ω ∂μ =
        (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c) ω ∂μ
add :
  ∀ ⦃f_1 g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * f_1 ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 ω ∂μ →
            ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
              ∫⁻ (ω : Ω), f ω * (f_1 + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f_1 + g) ω ∂μ
⊢ ∀ {g : Ω → ℝ≥0∞} (h_meas_g : Measurable g), ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
have iSup : ∀ ⦃f_1 : ℕ → Ω → ℝ≥0∞⦄,
  (∀ (n : ℕ), Measurable (f_1 n)) →
    Monotone f_1 →
      (∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f_1 n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 n ω ∂μ) →
        ∫⁻ (ω : Ω), f ω * (fun (x : Ω) ↦ (⨆ (n : ℕ), f_1 n x : ℝ≥0∞)) ω ∂μ =
          (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun (x : Ω) ↦ (⨆ (n : ℕ), f_1 n x : ℝ≥0∞)) ω ∂μ
Tactic: apply @Measurable.ennreal_induction _ Mg
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ ∫⁻ (ω : Ω), f ω * s.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c) ω ∂μ
have apply : IndepSets {s : Set Ω | MeasurableSet s} {s} μ
Tactic: apply lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator hMf _ (hMg _ h_s) _ h_meas_f
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ IndepSets {s : Set Ω | MeasurableSet s} {s} μ
have apply : Subset (α := Set (Set Ω)) {s} {s : Set Ω | MeasurableSet s}
Tactic: apply indepSets_of_indepSets_of_le_right h_ind
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ Subset (α := Set (Set Ω)) {s} {s : Set Ω | MeasurableSet s}
have rwa : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
Tactic: rwa [singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
h_1 : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
⊢ ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ
have h_measM_f' : Measurable f'
Tactic: have h_measM_f' : Measurable f' := h_measMg_f'.mono hMg le_rfl
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
h_1 : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ
have add : ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
Tactic: simp_rw [Pi.add_apply, left_distrib]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
h_1 : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
have add : ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ)
Tactic: rw [lintegral_add_left h_measM_f', lintegral_add_left (h_measM_f.mul h_measM_f'), left_distrib,
      h_ind_f', h_ind_g']
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
h_1 : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
add : ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ)
⊢ ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
have add₁ : ∫⁻ (a : Ω), f a * f' a ∂μ + ∫⁻ (a : Ω), f a * g a ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ)
Tactic: rw [lintegral_add_left h_measM_f', lintegral_add_left (h_measM_f.mul h_measM_f'), left_distrib,
      h_ind_f', h_ind_g']
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
h_1 : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
add : ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ)
add₁ :
  ∫⁻ (a : Ω), f a * f' a ∂μ + ∫⁻ (a : Ω), f a * g a ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ)
⊢ ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
have add₂ : ∫⁻ (a : Ω), f a * f' a ∂μ + ∫⁻ (a : Ω), f a * g a ∂μ =
  (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' a ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), g a ∂μ
Tactic: rw [lintegral_add_left h_measM_f', lintegral_add_left (h_measM_f.mul h_measM_f'), left_distrib,
      h_ind_f', h_ind_g']
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
h_1 : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
add : ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ)
add₁ :
  ∫⁻ (a : Ω), f a * f' a ∂μ + ∫⁻ (a : Ω), f a * g a ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ)
add₂ :
  ∫⁻ (a : Ω), f a * f' a ∂μ + ∫⁻ (a : Ω), f a * g a ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' a ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), g a ∂μ
⊢ ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
have add₃ : (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ + ∫⁻ (a : Ω), f a * g a ∂μ =
  (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' a ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), g a ∂μ
Tactic: rw [lintegral_add_left h_measM_f', lintegral_add_left (h_measM_f.mul h_measM_f'), left_distrib,
      h_ind_f', h_ind_g']
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
h : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
h_1 : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
add : ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ)
add₁ :
  ∫⁻ (a : Ω), f a * f' a ∂μ + ∫⁻ (a : Ω), f a * g a ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * (∫⁻ (a : Ω), f' a ∂μ + ∫⁻ (a : Ω), g a ∂μ)
add₂ :
  ∫⁻ (a : Ω), f a * f' a ∂μ + ∫⁻ (a : Ω), f a * g a ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' a ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), g a ∂μ
add₃ :
  (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ + ∫⁻ (a : Ω), f a * g a ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' a ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), g a ∂μ
⊢ ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
have add₄ : (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ =
  (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' a ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), g a ∂μ
Tactic: rw [lintegral_add_left h_measM_f', lintegral_add_left (h_measM_f.mul h_measM_f'), left_distrib,
      h_ind_f', h_ind_g']
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
⊢ ∫⁻ (ω : Ω), f ω * (fun (x : Ω) ↦ (⨆ (n : ℕ), f' n x : ℝ≥0∞)) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun (x : Ω) ↦ (⨆ (n : ℕ), f' n x : ℝ≥0∞)) ω ∂μ
have h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
Tactic: have h_measM_f' : ∀ n, Measurable (f' n) := fun n => (h_meas_f' n).mono hMg le_rfl
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ∫⁻ (ω : Ω), f ω * (fun (x : Ω) ↦ (⨆ (n : ℕ), f' n x : ℝ≥0∞)) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun (x : Ω) ↦ (⨆ (n : ℕ), f' n x : ℝ≥0∞)) ω ∂μ
have iSup : ∫⁻ (ω : Ω), ⨆ (i : ℕ), f ω * f' i ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), ⨆ (n : ℕ), f' n ω ∂μ
Tactic: simp_rw [mul_iSup]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ∫⁻ (ω : Ω), ⨆ (i : ℕ), f ω * f' i ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), ⨆ (n : ℕ), f' n ω ∂μ
have iSup : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : Ω), f a * f' n a ∂μ) (⨆ (i : ℕ), (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' i a ∂μ)
Tactic: rw [lintegral_iSup, lintegral_iSup h_measM_f' h_mono_f', mul_iSup]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
iSup : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : Ω), f a * f' n a ∂μ) (⨆ (i : ℕ), (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' i a ∂μ)
⊢ ∫⁻ (ω : Ω), ⨆ (i : ℕ), f ω * f' i ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), ⨆ (n : ℕ), f' n ω ∂μ
have iSup₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (ω : Ω) ↦ f ω * f' n ω
Tactic: rw [lintegral_iSup, lintegral_iSup h_measM_f' h_mono_f', mul_iSup]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
iSup : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : Ω), f a * f' n a ∂μ) (⨆ (i : ℕ), (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' i a ∂μ)
iSup₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (ω : Ω) ↦ f ω * f' n ω
⊢ ∫⁻ (ω : Ω), ⨆ (i : ℕ), f ω * f' i ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), ⨆ (n : ℕ), f' n ω ∂μ
have iSup₂ : Monotone.{0, u_1} (β := Ω → ℝ≥0∞) fun (i : ℕ) (ω : Ω) ↦ f ω * f' i ω
Tactic: rw [lintegral_iSup, lintegral_iSup h_measM_f' h_mono_f', mul_iSup]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : f ⟂ᵢ[μ] g
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
have fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
Tactic: have fg_ae : f * g =ᵐ[μ] h_meas_f.mk _ * h_meas_g.mk _ := h_meas_f.ae_eq_mk.mul h_meas_g.ae_eq_mk
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : f ⟂ᵢ[μ] g
fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
have rw : ∫⁻ (a : Ω), (AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g) a ∂μ =
  (∫⁻ (a : Ω), AEMeasurable.mk f h_meas_f a ∂μ) * ∫⁻ (a : Ω), AEMeasurable.mk g h_meas_g a ∂μ
Tactic: rw [lintegral_congr_ae h_meas_f.ae_eq_mk, lintegral_congr_ae h_meas_g.ae_eq_mk,
    lintegral_congr_ae fg_ae]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : f ⟂ᵢ[μ] g
fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (a : Ω), (AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g) a ∂μ =
    (∫⁻ (a : Ω), AEMeasurable.mk f h_meas_f a ∂μ) * ∫⁻ (a : Ω), AEMeasurable.mk g h_meas_g a ∂μ
have apply : AEMeasurable.mk f h_meas_f ⟂ᵢ[μ] AEMeasurable.mk g h_meas_g
Tactic: apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun h_meas_f.measurable_mk
      h_meas_g.measurable_mk
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
s : Finset ι
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
⊢ ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure μ := hX.isProbabilityMeasure