awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Integration
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 ∂μ
add₄ add₅ :
  (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' a ∂μ + (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), g a ∂μ
⊢ ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ

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']

Premises used: Measurable.mul, MeasureTheory.lintegral_add_left, left_distrib
-- Module: Mathlib.Probability.Independence.Integration
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 ω ∂μ
⊢ ∀ (n : ℕ), Measurable (f' n)

Tactic:
have h_measM_f' : ∀ n, Measurable (f' n) := fun n => (h_meas_f' n).mono hMg le_rfl
-- Module: Mathlib.Probability.Independence.Integration
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 : ∫⁻ (ω : Ω), ⨆ (i : ℕ), f ω * f' i ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), ⨆ (n : ℕ), f' n ω ∂μ
⊢ ∫⁻ (ω : Ω), f ω * (fun (x : Ω) ↦ (⨆ (n : ℕ), f' n x : ℝ≥0∞)) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun (x : Ω) ↦ (⨆ (n : ℕ), f' n x : ℝ≥0∞)) ω ∂μ

Tactic:
simp_rw [mul_iSup]

Premises used: ENNReal.mul_iSup
-- Module: Mathlib.Probability.Independence.Integration
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 ω
iSup₂ : Monotone.{0, u_1} (β := Ω → ℝ≥0∞) fun (i : ℕ) (ω : Ω) ↦ f ω * f' i ω
⊢ ∫⁻ (ω : Ω), ⨆ (i : ℕ), f ω * f' i ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), ⨆ (n : ℕ), f' n ω ∂μ

Tactic:
rw [lintegral_iSup, lintegral_iSup h_measM_f' h_mono_f', mul_iSup]

Premises used: MeasureTheory.lintegral_iSup, ENNReal.mul_iSup
-- Module: Mathlib.Probability.Independence.Integration
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)
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : Ω), f a * f' n a ∂μ) (⨆ (i : ℕ), (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' i a ∂μ)

Tactic:
simp_rw [← h_ind_f']
-- Module: Mathlib.Probability.Independence.Integration
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)
⊢ ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (ω : Ω) ↦ f ω * f' n ω

Tactic:
fun n => h_measM_f.mul (h_measM_f' n)

Premises used: Measurable.mul
-- Module: Mathlib.Probability.Independence.Integration
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)
⊢ ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (ω : Ω) ↦ f ω * f' n ω

Tactic:
exact fun n => h_measM_f.mul (h_measM_f' n)

Premises used: Measurable.mul
-- Module: Mathlib.Probability.Independence.Integration
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)
⊢ Monotone.{0, u_1} (β := Ω → ℝ≥0∞) fun (i : ℕ) (ω : Ω) ↦ f ω * f' i ω

Tactic:
fun n m (h_le : n ≤ m) a => mul_le_mul_right (h_mono_f' h_le a) _

Premises used: Monotone, mul_le_mul_right
-- Module: Mathlib.Probability.Independence.Integration
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)
⊢ Monotone.{0, u_1} (β := Ω → ℝ≥0∞) fun (i : ℕ) (ω : Ω) ↦ f ω * f' i ω

Tactic:
exact fun n m (h_le : n ≤ m) a => mul_le_mul_right (h_mono_f' h_le a) _

Premises used: mul_le_mul_right
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : Measurable f
h_meas_g : Measurable g
h_indep_fun : f ⟂ᵢ[μ] g
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

Tactic:
lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace
    (measurable_iff_comap_le.1 h_meas_f) (measurable_iff_comap_le.1 h_meas_g) h_indep_fun
    (Measurable.of_comap_le le_rfl) (Measurable.of_comap_le le_rfl)

Premises used: le_rfl, Measurable.of_comap_le, measurable_iff_comap_le, Iff.mp, ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace
-- Module: Mathlib.Probability.Independence.Integration
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 =ᶠ[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
-- Module: Mathlib.Probability.Independence.Integration
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
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 ∂μ
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

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]

Premises used: MeasureTheory.lintegral_congr_ae, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Integration
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
apply : 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 ∂μ

Tactic:
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun h_meas_f.measurable_mk
      h_meas_g.measurable_mk

Premises used: ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun, AEMeasurable.measurable_mk
-- Module: Mathlib.Probability.Independence.Integration
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
⊢ AEMeasurable.mk f h_meas_f ⟂ᵢ[μ] AEMeasurable.mk g h_meas_g

Tactic:
h_indep_fun.congr h_meas_f.ae_eq_mk h_meas_g.ae_eq_mk

Premises used: ProbabilityTheory.IndepFun.congr, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Integration
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
⊢ AEMeasurable.mk f h_meas_f ⟂ᵢ[μ] AEMeasurable.mk g h_meas_g

Tactic:
exact h_indep_fun.congr h_meas_f.ae_eq_mk h_meas_g.ae_eq_mk

Premises used: ProbabilityTheory.IndepFun.congr, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Independence.Integration
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 ω ∂μ

Tactic:
lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' h_meas_f h_meas_g h_indep_fun

Premises used: ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'
-- Module: Mathlib.Probability.Independence.Integration
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)
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ := hX.isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ ∅, X i ω ∂μ = ∏ i ∈ ∅, ∫⁻ (ω : Ω), X i ω ∂μ

Tactic:
simp only [Finset.prod_empty, lintegral_const, measure_univ, mul_one]

Premises used: MeasureTheory.lintegral_const, Finset.prod_empty, MeasureTheory.IsProbabilityMeasure.measure_univ, mul_one
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
cons :
  ∫⁻ (ω : Ω), HMul.hMul (β := (a : Ω) → ℝ≥0∞) (X j) (∏ c ∈ s, X c) ω ∂μ =
    (∫⁻ (ω : Ω), X j ω ∂μ) * ∫⁻ (ω : Ω), (∏ c ∈ s, X c) ω ∂μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ Finset.cons j s hj, X i ω ∂μ = ∏ i ∈ Finset.cons j s hj, ∫⁻ (ω : Ω), X i ω ∂μ

Tactic:
simp only [← Finset.prod_apply, Finset.prod_cons, ← ihs]

Premises used: Finset.prod_apply, Finset.prod_cons
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
cons : AEMeasurable (X j) μ
cons₁ : AEMeasurable (β := ℝ≥0∞) (∏ c ∈ s, X c) μ
cons₂ : X j ⟂ᵢ[μ] ∏ c ∈ s, X c
⊢ ∫⁻ (ω : Ω), HMul.hMul (β := (a : Ω) → ℝ≥0∞) (X j) (∏ c ∈ s, X c) ω ∂μ =
    (∫⁻ (ω : Ω), X j ω ∂μ) * ∫⁻ (ω : Ω), (∏ c ∈ s, X c) ω ∂μ

Tactic:
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'

Premises used: ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (X j) μ

Tactic:
(x_mea j).aemeasurable

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (X j) μ

Tactic:
exact (x_mea j).aemeasurable

Premises used: Measurable.aemeasurable
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (β := ℝ≥0∞) (∏ c ∈ s, X c) μ

Tactic:
s.aemeasurable_prod (fun i _ ↦ (x_mea i).aemeasurable)

Premises used: Measurable.aemeasurable, Finset.aemeasurable_prod
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (β := ℝ≥0∞) (∏ c ∈ s, X c) μ

Tactic:
exact s.aemeasurable_prod (fun i _ ↦ (x_mea i).aemeasurable)

Premises used: Measurable.aemeasurable, Finset.aemeasurable_prod
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ X j ⟂ᵢ[μ] ∏ c ∈ s, X c

Tactic:
(iIndepFun.indepFun_finsetProd_of_notMem hX x_mea hj).symm

Premises used: ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem, ProbabilityTheory.IndepFun.symm
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun (β := fun (x : ι) ↦ ℝ≥0∞) X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ X j ⟂ᵢ[μ] ∏ c ∈ s, X c

Tactic:
exact (iIndepFun.indepFun_finsetProd_of_notMem hX x_mea hj).symm

Premises used: ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem, ProbabilityTheory.IndepFun.symm
-- Module: Mathlib.Probability.Independence.Integration
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)
this : IsProbabilityMeasure μ
empty : ∫⁻ (ω : Ω), ∏ i ∈ ∅, X i ω ∂μ = ∏ i ∈ ∅, ∫⁻ (ω : Ω), X i ω ∂μ
cons :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s) (ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ),
    ∫⁻ (ω : Ω), ∏ i ∈ Finset.cons j s hj, X i ω ∂μ = ∏ i ∈ Finset.cons j s hj, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ

Tactic:
induction s using Finset.cons_induction with
  | empty => simp only [Finset.prod_empty, lintegral_const, measure_univ, mul_one]
  | cons j s hj ihs =>
    simp only [← Finset.prod_apply, Finset.prod_cons, ← ihs]
    apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'
    · exact (x_mea j).aemeasurable
    · exact s.aemeasurable_prod (fun i _ ↦ (x_mea i).aemeasurable)
    · exact (iIndepFun.indepFun_finsetProd_of_notMem hX x_mea hj).symm

Premises used: MeasureTheory.lintegral_const, Finset.prod_empty, ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun', Measurable.aemeasurable, Finset.prod_apply, MeasureTheory.IsProbabilityMeasure.measure_univ, Finset.aemeasurable_prod, Finset.prod_cons, mul_one
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : ContinuousENorm F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
inst_8 : TopologicalSpace G
inst_9 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ (↑C : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ
⊢ Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ

Tactic:
⟨cB.comp_aestronglyMeasurable₂ hX.1 hY.1, ?_⟩

Premises used: MeasureTheory.Integrable, And.left, And.intro, Continuous.comp_aestronglyMeasurable₂
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : ContinuousENorm F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
inst_8 : TopologicalSpace G
inst_9 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ (↑C : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ
refine : HasFiniteIntegral.{u_1, u_7} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
⊢ Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ

Tactic:
refine ⟨cB.comp_aestronglyMeasurable₂ hX.1 hY.1, ?_⟩
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : ContinuousENorm F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
inst_8 : TopologicalSpace G
inst_9 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ (↑C : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (ω : Ω) ↦ ‖X ω‖ₑ * ‖Y ω‖ₑ) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : ContinuousENorm F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
inst_8 : TopologicalSpace G
inst_9 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ (↑C : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ
rw :
  ∫⁻ (a : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) a) ∂μ ≤ ∫⁻ (a : Ω), (↑C : ℝ≥0∞) * (‖X a‖ₑ * ‖Y a‖ₑ) ∂μ
⊢ ∫⁻ (a : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) a) ∂μ ≤ (↑C : ℝ≥0∞) * ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ

Tactic:
rw [← lintegral_const_mul'' _ (by fun_prop)]

Premises used: MeasureTheory.lintegral_const_mul''
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : ContinuousENorm F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
inst_8 : TopologicalSpace G
inst_9 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ (↑C : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ
hfg : ∀ (ω : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) ω) ≤ (↑C : ℝ≥0∞) * (‖X ω‖ₑ * ‖Y ω‖ₑ)
⊢ ∫⁻ (a : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) a) ∂μ ≤ ∫⁻ (a : Ω), (↑C : ℝ≥0∞) * (‖X a‖ₑ * ‖Y a‖ₑ) ∂μ

Tactic:
gcongr with ω
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : ContinuousENorm F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
inst_8 : TopologicalSpace G
inst_9 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ (↑C : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ
ω : Ω
⊢ enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) ω) ≤ (↑C : ℝ≥0∞) * (‖X ω‖ₑ * ‖Y ω‖ₑ)

Tactic:
simp [← mul_assoc, hB]

Premises used: mul_assoc
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : TopologicalSpace F
inst_5 : ContinuousENorm F
inst_6 : MeasurableSpace F
inst_7 : OpensMeasurableSpace F
inst_8 : TopologicalSpace G
inst_9 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E → F → G
cB : Continuous (Function.uncurry B)
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖B x y‖ₑ ≤ (↑C : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ
rw rw₁ :
  (↑C : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ) =
    (↑C : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)
⊢ (↑C : ℝ≥0∞) * ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ = (↑C : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)

Tactic:
rw [lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.1.enorm hY.1.enorm
        (hXY.comp measurable_enorm measurable_enorm)]

Premises used: ProbabilityTheory.IndepFun.comp, ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'', And.left, measurable_enorm, MeasureTheory.AEStronglyMeasurable.enorm