awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : CompleteSpace E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace ℝ G
inst_15 : NormedSpace 𝕜 G
inst_16 : CompleteSpace G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
B : E →L[ℝ] F →L[ℝ] G
c : ℝ≥0
hc : c ≠ 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ) * ‖x‖ * ‖y‖ ≤ norm.{u_7} (E := G) ((((B : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) y : G)
⊢ Eq.{u_7 + 1} (α := G) (∫ (ω : Ω), (((B : (a : E) → F →L[ℝ] G) (X ω) : F →L[ℝ] G) : (a : F) → G) (Y ω) ∂μ : G)
    (((B : (a : E) → F →L[ℝ] G) (∫ (x : Ω), X x ∂μ) : (a : F) → G) (∫ (x : Ω), Y x ∂μ) : G)

Tactic:
hXY.integral_bilin_comp_comp' hX.aemeasurable hY.aemeasurable
    hX.aestronglyMeasurable_id_map hY.aestronglyMeasurable_id_map B c hc hB

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.IndepFun.integral_bilin_comp_comp', MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_id_map
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
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 : SMul E F
inst_9 : ContinuousSMul E F
inst_10 : ENormSMulClass E F
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
⊢ Continuous (X := E × F) (Y := F) (Function.uncurry fun (x1 : E) (x2 : F) ↦ x1 • x2)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
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 : SMul E F
inst_9 : ContinuousSMul E F
inst_10 : ENormSMulClass E F
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
⊢ ∀ (x : E) (y : F), enorm.{u_6} (E := F) ((fun (x1 : E) (x2 : F) ↦ x1 • x2) x y) ≤ (↑1 : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ

Tactic:
simp [enorm_smul]

Premises used: enorm_smul
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
inst_2 : Mul E
inst_3 : ContinuousMul E
inst_4 : ENormSMulClass E E
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
X Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
⊢ Integrable (X * Y) μ

Tactic:
hXY.integrable_smul hX hY

Premises used: ProbabilityTheory.IndepFun.integrable_smul
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
pos :
  ∀ (hE : CompleteSpace E),
    ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
      HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)
neg :
  ∀ (hE : ¬CompleteSpace E),
    ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
      HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)
⊢ ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
hE : CompleteSpace E
⊢ Ne (α := ℝ≥0) 1 0

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
hE : CompleteSpace E
⊢ ∀ (x : 𝕜) (y : E),
    (↑1 : ℝ) * ‖x‖ * ‖y‖ ≤
      norm (E := E)
        (((((ContinuousLinearMap.lsmul ℝ 𝕜 : ContinuousLinearMap.{0, 0, u_2, u_5} (RingHom.id ℝ) 𝕜 (E →L[ℝ] E)) :
                    (a : 𝕜) → E →L[ℝ] E)
                  x :
                E →L[ℝ] E) :
              (a : E) → E)
            y :
          E)

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
hE : CompleteSpace E
⊢ ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
exact hXY.integral_bilin_comp_comp' hX hY hf hg (.lsmul ℝ 𝕜) 1 (by simp) (by simp [norm_smul])

Premises used: Real, ProbabilityTheory.IndepFun.integral_bilin_comp_comp', ContinuousLinearMap.lsmul, OfNat.ofNat
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
hE : ¬CompleteSpace E
⊢ ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
simp [integral, hE]

Premises used: MeasureTheory.integral
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → 𝕜
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
⊢ ∫ (ω : Ω), f (X ω) * g (Y ω) ∂μ = HMul.hMul (α := 𝕜) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
hXY.integral_fun_comp_smul_comp hX hY hf hg

Premises used: ProbabilityTheory.IndepFun.integral_fun_comp_smul_comp
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
⊢ ∫ (x : Ω), (f ∘ X • g ∘ Y) x ∂μ =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), (f ∘ X) x ∂μ) (∫ (x : Ω), (g ∘ Y) x ∂μ)

Tactic:
hXY.integral_fun_comp_smul_comp hX hY hf hg

Premises used: ProbabilityTheory.IndepFun.integral_fun_comp_smul_comp
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → 𝕜
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
⊢ ∫ (x : Ω), (f ∘ X * g ∘ Y) x ∂μ = HMul.hMul (α := 𝕜) (∫ (x : Ω), (f ∘ X) x ∂μ) (∫ (x : Ω), (g ∘ Y) x ∂μ)

Tactic:
hXY.integral_fun_comp_mul_comp hX hY hf hg

Premises used: ProbabilityTheory.IndepFun.integral_fun_comp_mul_comp
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
pos :
  ∀ (hE : CompleteSpace E),
    ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
neg :
  ∀ (hE : ¬CompleteSpace E),
    ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
⊢ ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
hE : CompleteSpace E
⊢ Ne (α := ℝ≥0) 1 0

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
hE : CompleteSpace E
⊢ ∀ (x : 𝕜) (y : E),
    (↑1 : ℝ) * ‖x‖ * ‖y‖ ≤
      norm (E := E)
        (((((ContinuousLinearMap.lsmul ℝ 𝕜 : ContinuousLinearMap.{0, 0, u_2, u_5} (RingHom.id ℝ) 𝕜 (E →L[ℝ] E)) :
                    (a : 𝕜) → E →L[ℝ] E)
                  x :
                E →L[ℝ] E) :
              (a : E) → E)
            y :
          E)

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
hE : CompleteSpace E
⊢ ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
exact hXY.integral_bilin' (𝕜 := 𝕜) hX hY (.lsmul ℝ 𝕜) 1 (by simp) (by simp [norm_smul])

Premises used: Real, ProbabilityTheory.IndepFun.integral_bilin', ContinuousLinearMap.lsmul, OfNat.ofNat
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
hE : ¬CompleteSpace E
⊢ ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
simp [integral, hE]

Premises used: MeasureTheory.integral
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → 𝕜
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ ∫ (x : Ω), (X * Y) x ∂μ = HMul.hMul (α := 𝕜) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
hXY.integral_smul_eq_smul_integral hX hY

Premises used: ProbabilityTheory.IndepFun.integral_smul_eq_smul_integral
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ ∫ (ω : Ω), X ω • Y ω ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), X ω ∂μ) (∫ (ω : Ω), Y ω ∂μ)

Tactic:
hXY.integral_smul_eq_smul_integral hX hY

Premises used: ProbabilityTheory.IndepFun.integral_smul_eq_smul_integral
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → 𝕜
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ ∫ (ω : Ω), X ω * Y ω ∂μ = HMul.hMul (α := 𝕜) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
hXY.integral_fun_smul_eq_smul_integral hX hY

Premises used: ProbabilityTheory.IndepFun.integral_fun_smul_eq_smul_integral
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ f ⟂ᵢ[μ] g ↔
    ∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)

Tactic:
⟨fun hfg _ _ hφ hψ _ _ => hfg.integral_comp_mul_comp
      hfm.aemeasurable hgm.aemeasurable hφ.aestronglyMeasurable hψ.aestronglyMeasurable, ?_⟩

Premises used: Measurable.aemeasurable, ProbabilityTheory.IndepFun.integral_comp_mul_comp, Measurable.aestronglyMeasurable, Iff.intro
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
refine :
  (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    f ⟂ᵢ[μ] g
⊢ f ⟂ᵢ[μ] g ↔
    ∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)

Tactic:
refine ⟨fun hfg _ _ hφ hψ _ _ => hfg.integral_comp_mul_comp
      hfm.aemeasurable hgm.aemeasurable hφ.aestronglyMeasurable hψ.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
rw :
  (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    f ⟂ᵢ[μ] g

Tactic:
rw [IndepFun_iff]

Premises used: ProbabilityTheory.IndepFun_iff
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
h :
  ∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) μ →
          Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ integral μ (HMul.hMul (α := Ω → ℝ) (A.indicator 1 ∘ f) (B.indicator 1 ∘ g)) =
    HMul.hMul (α := ℝ) (integral μ (A.indicator 1 ∘ f)) (integral μ (B.indicator 1 ∘ g))

Tactic:
specialize
    h (measurable_one.indicator hA) (measurable_one.indicator hB)
      ((integrable_const 1).indicator (hfm.comp measurable_id hA))
      ((integrable_const 1).indicator (hgm.comp measurable_id hB))

Premises used: Measurable.comp, measurable_id, Measurable.indicator, measurable_one, MeasureTheory.Integrable.indicator
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h :
  integral μ (HMul.hMul (α := Ω → ℝ) (A.indicator 1 ∘ f) (B.indicator 1 ∘ g)) =
    HMul.hMul (α := ℝ) (integral μ (A.indicator 1 ∘ f)) (integral μ (B.indicator 1 ∘ g))
rwa :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' B) : ℝ≥0∞) ≠
    ∞
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A ∩ g ⁻¹' B) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' B) : ℝ≥0∞)

Tactic:
rwa [← toReal_eq_toReal_iff' (measure_ne_top μ _), toReal_mul, ← measureReal_def,
    ← measureReal_def, ← measureReal_def, ← integral_indicator_one ((hfm hA).inter (hgm hB)),
    ← integral_indicator_one (hfm hA), ← integral_indicator_one (hgm hB), Set.inter_indicator_one]

Premises used: ENNReal.toReal_eq_toReal_iff', MeasureTheory.measure_ne_top, MeasureTheory.integral_indicator_one, ENNReal.toReal_mul, MeasureTheory.measureReal_def, Set.inter_indicator_one, MeasurableSet.inter
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h :
  integral μ (HMul.hMul (α := Ω → ℝ) (A.indicator 1 ∘ f) (B.indicator 1 ∘ g)) =
    HMul.hMul (α := ℝ) (integral μ (A.indicator 1 ∘ f)) (integral μ (B.indicator 1 ∘ g))
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' B) : ℝ≥0∞) ≠
    ∞

Tactic:
mul_ne_top (measure_ne_top μ _) (measure_ne_top μ _)

Premises used: MeasureTheory.measure_ne_top, ENNReal.mul_ne_top
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h :
  integral μ (HMul.hMul (α := Ω → ℝ) (A.indicator 1 ∘ f) (B.indicator 1 ∘ g)) =
    HMul.hMul (α := ℝ) (integral μ (A.indicator 1 ∘ f)) (integral μ (B.indicator 1 ∘ g))
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' B) : ℝ≥0∞) ≠
    ∞

Tactic:
exact mul_ne_top (measure_ne_top μ _) (measure_ne_top μ _)

Premises used: MeasureTheory.measure_ne_top, ENNReal.mul_ne_top
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst_1 : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun (β := 𝓧) X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (m₀ := m𝓧 i) (f i) (Measure.map (X i) μ)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (ω : Ω), ∏ i : ι, f i (X i ω) ∂μ) (∏ i : ι, ∫ (ω : Ω), f i (X i ω) ∂μ)

Tactic:
hX.integral_fun_prod_comp mX hf

Premises used: ProbabilityTheory.iIndepFun.integral_fun_prod_comp
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst_1 : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun (β := 𝓧) X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (m₀ := m𝓧 i) (f i) (Measure.map (X i) μ)
h : ∀ (x : Ω), Eq.{u_2 + 1} (α := 𝕜) ((∏ i : ι, f i ∘ X i) x) (∏ i : ι, f i (X i x))
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (x : Ω), (∏ i : ι, f i ∘ X i) x ∂μ) (∏ i : ι, ∫ (x : Ω), (f i ∘ X i) x ∂μ)

Tactic:
convert! hX.integral_fun_prod_comp mX hf

Premises used: ProbabilityTheory.iIndepFun.integral_fun_prod_comp
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst_1 : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun (β := 𝓧) X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (m₀ := m𝓧 i) (f i) (Measure.map (X i) μ)
x : Ω
⊢ Eq.{u_2 + 1} (α := 𝕜) ((∏ i : ι, f i ∘ X i) x) (∏ i : ι, f i (X i x))

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst_1 : Fintype ι
X : (i : ι) → Ω → 𝕜
hX : iIndepFun (β := fun (x : ι) ↦ 𝕜) X μ
mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (x : Ω), (∏ i : ι, X i) x ∂μ) (∏ i : ι, ∫ (x : Ω), X i x ∂μ)

Tactic:
hX.integral_prod_comp (fun i ↦ (mX i).aemeasurable) (fun _ ↦ aestronglyMeasurable_id)

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, aestronglyMeasurable_id, ProbabilityTheory.iIndepFun.integral_prod_comp
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst_1 : Fintype ι
X : (i : ι) → Ω → 𝕜
hX : iIndepFun (β := fun (x : ι) ↦ 𝕜) X μ
mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (ω : Ω), ∏ i : ι, X i ω ∂μ) (∏ i : ι, ∫ (x : Ω), X i x ∂μ)

Tactic:
hX.integral_fun_prod_comp (fun i ↦ (mX i).aemeasurable) (fun _ ↦ aestronglyMeasurable_id)

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, aestronglyMeasurable_id, ProbabilityTheory.iIndepFun.integral_fun_prod_comp