awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
⊢ ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)

Tactic:
have hB x y : c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ := by
    rw [← toReal_le_toReal]
    · simpa using hB x y
    all_goals finiteness
-- 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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
pos :
  ∀
    (h :
      Integrable.{u_7, u_1} (ε := G)
        (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ),
    Eq.{u_7 + 1} (α := G)
      (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
      (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
neg :
  ∀
    (h :
      ¬Integrable.{u_7, u_1} (ε := G)
          (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ),
    Eq.{u_7 + 1} (α := G)
      (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
      (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
⊢ Eq.{u_7 + 1} (α := G) (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
by_cases h : Integrable (fun ω ↦ B (f (X ω)) (g (Y ω))) μ

Premises used: MeasureTheory.Integrable, DFunLike.coe
-- 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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  Integrable.{u_7, u_1} (ε := G)
    (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
⊢ @Integrable _ _ _ _ inst_1 f (Measure.map X μ)

Tactic:
have h1 : Integrable f (μ.map X) := (integrable_map_measure hf hX).2 <|
      hfXgY.integrable_left_of_integrable_op (B · ·) c hc hB h hfX hgY h'Y
-- 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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  Integrable.{u_7, u_1} (ε := G)
    (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
h1 : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
⊢ @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)

Tactic:
have h2 : Integrable g (μ.map Y) := (integrable_map_measure hg hY).2 <|
      hfXgY.integrable_right_of_integrable_op (B · ·) c hc hB h hfX hgY h'X
-- 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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  Integrable.{u_7, u_1} (ε := G)
    (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
h1 : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
h2 : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
⊢ Eq.{u_7 + 1} (α := G) (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
hXY.integral_bilin_comp_comp hX hY h1 h2 B

Premises used: ProbabilityTheory.IndepFun.integral_bilin_comp_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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  Integrable.{u_7, u_1} (ε := G)
    (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
h1 : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
h2 : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
⊢ Eq.{u_7 + 1} (α := G) (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
exact hXY.integral_bilin_comp_comp hX hY h1 h2 B

Premises used: ProbabilityTheory.IndepFun.integral_bilin_comp_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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  ¬Integrable.{u_7, u_1} (ε := G)
      (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
neg :
  Eq.{u_7 + 1} (α := G) (0 : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
⊢ Eq.{u_7 + 1} (α := G) (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
rw [integral_undef h]

Premises used: MeasureTheory.integral_undef
-- 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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  ¬Integrable.{u_7, u_1} (ε := G)
      (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
⊢ ¬Integrable.{u_5, u_1} (ε := E) (fun (ω : Ω) ↦ f (X ω)) μ ∨ ¬Integrable.{u_6, u_1} (ε := F) (fun (ω : Ω) ↦ g (Y ω)) μ

Tactic:
not_and_or.1 fun ⟨HX, HY⟩ ↦ h (hfXgY.integrable_bilin HX HY B)

Premises used: False, ProbabilityTheory.IndepFun.integrable_bilin, _private.0.ProbabilityTheory.IndepFun.integral_bilin_comp_comp'.match_3, not_and_or, Iff.mp
-- 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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  ¬Integrable.{u_7, u_1} (ε := G)
      (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
neg :
  ∀ (h : ¬Integrable.{u_5, u_1} (ε := E) (fun (ω : Ω) ↦ f (X ω)) μ),
    Eq.{u_7 + 1} (α := G) (0 : G)
      (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
neg₁ :
  ∀ (h : ¬Integrable.{u_6, u_1} (ε := F) (fun (ω : Ω) ↦ g (Y ω)) μ),
    Eq.{u_7 + 1} (α := G) (0 : G)
      (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
⊢ Eq.{u_7 + 1} (α := G) (0 : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
obtain h | h : ¬(Integrable (fun ω ↦ f (X ω)) μ) ∨ ¬(Integrable (fun ω ↦ g (Y ω)) μ) :=
      not_and_or.1 fun ⟨HX, HY⟩ ↦ h (hfXgY.integrable_bilin HX HY B)

Premises used: False, MeasureTheory.Integrable, ProbabilityTheory.IndepFun.integrable_bilin, _private.0.match_1, not_and_or, Iff.mp
-- 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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h_1 :
  ¬Integrable.{u_7, u_1} (ε := G)
      (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
h : ¬Integrable.{u_5, u_1} (ε := E) (fun (ω : Ω) ↦ f (X ω)) μ
⊢ Eq.{u_7 + 1} (α := G) (0 : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
simp [integral_undef h]

Premises used: MeasureTheory.integral_undef
-- 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
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
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 μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB_1 :
  ∀ (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)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h_1 :
  ¬Integrable.{u_7, u_1} (ε := G)
      (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
h : ¬Integrable.{u_6, u_1} (ε := F) (fun (ω : Ω) ↦ g (Y ω)) μ
⊢ Eq.{u_7 + 1} (α := G) (0 : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
simp [integral_undef h]

Premises used: MeasureTheory.integral_undef
-- 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 : Integrable X μ
hY : Integrable Y μ
B : E →L[ℝ] F →L[ℝ] 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
    ((integrable_map_measure hX.aestronglyMeasurable.aestronglyMeasurable_id_map hX.aemeasurable).2
      hX)
    ((integrable_map_measure hY.aestronglyMeasurable.aestronglyMeasurable_id_map hY.aemeasurable).2
      hY) B

Premises used: Iff.mpr, MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.Integrable.aemeasurable, MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_id_map, MeasureTheory.integrable_map_measure, ProbabilityTheory.IndepFun.integral_bilin_comp_comp