awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖ₑ
⊢ (↑C : ℝ≥0∞) < ∞

Tactic:
finiteness
-- 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‖ₑ
_ : ∫⁻ (a : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) a) ∂μ ≤ (↑C : ℝ≥0∞) * ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ
_₁ : (↑C : ℝ≥0∞) * ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ = (↑C : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)
⊢ ∫⁻ (a : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) a) ∂μ < ∞

Tactic:
calc
  _ ≤ C * ∫⁻ ω, ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ := by
    rw [← lintegral_const_mul'' _ (by fun_prop)]
    gcongr with ω
    simp [← mul_assoc, hB]
  _ = C * ((∫⁻ ω, ‖X ω‖ₑ ∂μ) * (∫⁻ ω, ‖Y ω‖ₑ ∂μ)) := by
    rw [lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.1.enorm hY.1.enorm
        (hXY.comp measurable_enorm measurable_enorm)]
  _ < ∞ := mul_lt_top (by finiteness) (mul_lt_top hX.2 hY.2)

Premises used: HMul.hMul, ENNReal.mul_lt_top, ENorm.enorm, And.right, MeasureTheory.lintegral
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : MeasurableSpace F
inst_8 : OpensMeasurableSpace F
inst_9 : SeminormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E →L[𝕜] F →L[𝕜] G
⊢ Continuous (X := E × F) (Y := G)
    (Function.uncurry fun (x1 : E) (x2 : F) ↦ (((B : (a : E) → F →L[𝕜] G) x1 : F →L[𝕜] G) : (a : F) → G) x2)

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
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : MeasurableSpace F
inst_8 : OpensMeasurableSpace F
inst_9 : SeminormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E →L[𝕜] F →L[𝕜] G
refine :
  ∀ (x : E) (y : F),
    enorm.{u_7} (E := G)
        ((fun (x1 : E) (x2 : F) ↦ ((((B : (a : E) → F →L[𝕜] G) x1 : F →L[𝕜] G) : (a : F) → G) x2 : G)) x y) ≤
      (↑‖B‖₊ : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ
⊢ Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (X ω) : F →L[𝕜] G) : (a : F) → G) (Y ω)) μ

Tactic:
refine hXY.integrable_op hX hY (B · ·) (by fun_prop) ‖B‖₊ (fun x y ↦ ?_)

Premises used: NNNorm.nnnorm, ProbabilityTheory.IndepFun.integrable_op, DFunLike.coe
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : MeasurableSpace F
inst_8 : OpensMeasurableSpace F
inst_9 : SeminormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ enorm.{u_7} (E := G)
      ((fun (x1 : E) (x2 : F) ↦ ((((B : (a : E) → F →L[𝕜] G) x1 : F →L[𝕜] G) : (a : F) → G) x2 : G)) x y) ≠
    ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : MeasurableSpace F
inst_8 : OpensMeasurableSpace F
inst_9 : SeminormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ (↑‖B‖₊ : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : MeasurableSpace F
inst_8 : OpensMeasurableSpace F
inst_9 : SeminormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E →L[𝕜] F →L[𝕜] G
x : E
y : F
rw :
  (enorm.{u_7} (E := G)
        ((fun (x1 : E) (x2 : F) ↦ ((((B : (a : E) → F →L[𝕜] G) x1 : F →L[𝕜] G) : (a : F) → G) x2 : G)) x y)).toReal ≤
    ((↑‖B‖₊ : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ).toReal
⊢ enorm.{u_7} (E := G)
      ((fun (x1 : E) (x2 : F) ↦ ((((B : (a : E) → F →L[𝕜] G) x1 : F →L[𝕜] G) : (a : F) → G) x2 : G)) x y) ≤
    (↑‖B‖₊ : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ

Tactic:
rw [← toReal_le_toReal (by finiteness) (by finiteness)]

Premises used: ENNReal.toReal_le_toReal
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
𝕜 : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SeminormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : MeasurableSpace F
inst_8 : OpensMeasurableSpace F
inst_9 : SeminormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
hX : Integrable X μ
hY : Integrable Y μ
B : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ (enorm.{u_7} (E := G)
        ((fun (x1 : E) (x2 : F) ↦ ((((B : (a : E) → F →L[𝕜] G) x1 : F →L[𝕜] G) : (a : F) → G) x2 : G)) x y)).toReal ≤
    ((↑‖B‖₊ : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ).toReal

Tactic:
simp [B.le_opNorm₂]

Premises used: ContinuousLinearMap.le_opNorm₂
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
⊢ Integrable X μ

Tactic:
⟨hX, ?_⟩

Premises used: MeasureTheory.Integrable, And.intro
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
refine : HasFiniteIntegral X μ
⊢ Integrable X μ

Tactic:
refine ⟨hX, ?_⟩
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
H : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ = 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ ‖Y ω‖ₑ) 0

Tactic:
have I : (fun ω => ‖Y ω‖ₑ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hY.enorm).1 H
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
H : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ = 0
I : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ ‖Y ω‖ₑ) 0
apply : Y =ᶠ[ae μ] 0
⊢ False

Tactic:
apply h'Y
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
H : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ = 0
I : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ ‖Y ω‖ₑ) 0
h : ∀ (ω : Ω) (hω : ‖Y ω‖ₑ = 0 ω), Y ω = 0 ω
⊢ Y =ᶠ[ae μ] 0

Tactic:
filter_upwards [I] with ω hω
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
H : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ = 0
I : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ ‖Y ω‖ₑ) 0
ω : Ω
hω : ‖Y ω‖ₑ = 0 ω
⊢ Y ω = 0 ω

Tactic:
simpa using hω
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
⊢ ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0

Tactic:
have I : (∫⁻ ω, ‖Y ω‖ₑ ∂μ) ≠ 0 := fun H ↦ by
    have I : (fun ω => ‖Y ω‖ₑ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hY.enorm).1 H
    apply h'Y
    filter_upwards [I] with ω hω
    simpa using hω
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
⊢ HasFiniteIntegral X μ

Tactic:
hasFiniteIntegral_iff_enorm.mpr <| lt_top_iff_ne_top.2 fun H => ?_

Premises used: Iff.mpr, lt_top_iff_ne_top, MeasureTheory.hasFiniteIntegral_iff_enorm
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
refine : ∀ (H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞), False
⊢ HasFiniteIntegral X μ

Tactic:
refine hasFiniteIntegral_iff_enorm.mpr <| lt_top_iff_ne_top.2 fun H => ?_

Premises used: Iff.mpr, lt_top_iff_ne_top, MeasureTheory.hasFiniteIntegral_iff_enorm
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
⊢ (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ

Tactic:
have J : (‖X ·‖ₑ) ⟂ᵢ[μ] (‖Y ·‖ₑ) := hXY.comp measurable_enorm measurable_enorm
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
simpa
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ
rw : ∞ = (↑c : ℝ≥0∞) * (∞ * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)
rw₁ : ∞ = (↑c : ℝ≥0∞) * ∞
rw₂ rw₃ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ ∞ = (↑c : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)

Tactic:
rw [H, top_mul I, mul_top (by simpa)]

Premises used: ENNReal.top_mul, ENNReal.mul_top
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ
⊢ 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ
rw : ∫⁻ (a : Ω), (↑c : ℝ≥0∞) * (‖X a‖ₑ * ‖Y a‖ₑ) ∂μ ≤ ∫⁻ (ω : Ω), ‖B (X ω) (Y ω)‖ₑ ∂μ
⊢ (↑c : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ) ≤ ∫⁻ (ω : Ω), ‖B (X ω) (Y ω)‖ₑ ∂μ

Tactic:
rw [← lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.enorm hY.enorm J,
        ← lintegral_const_mul'' _ (by fun_prop)]

Premises used: ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'', MeasureTheory.lintegral_const_mul'', MeasureTheory.AEStronglyMeasurable.enorm
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ
hfg : ∀ (ω : Ω), (↑c : ℝ≥0∞) * (‖X ω‖ₑ * ‖Y ω‖ₑ) ≤ ‖B (X ω) (Y ω)‖ₑ
⊢ ∫⁻ (a : Ω), (↑c : ℝ≥0∞) * (‖X a‖ₑ * ‖Y a‖ₑ) ∂μ ≤ ∫⁻ (ω : Ω), ‖B (X ω) (Y ω)‖ₑ ∂μ

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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ
ω : Ω
⊢ (↑c : ℝ≥0∞) * (‖X ω‖ₑ * ‖Y ω‖ₑ) ≤ ‖B (X ω) (Y ω)‖ₑ

Tactic:
simp [hB, ← mul_assoc]

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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ
⊢ LT.lt (α := ℝ≥0∞) ∞ ∞

Tactic:
have : ∞ < ∞ := calc
    ∞ = c * ((∫⁻ ω, ‖X ω‖ₑ ∂μ) * (∫⁻ ω, ‖Y ω‖ₑ ∂μ)) := by
      rw [H, top_mul I, mul_top (by simpa)]
    _ ≤ ∫⁻ ω, ‖B (X ω) (Y ω)‖ₑ ∂μ := by
      rw [← lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.enorm hY.enorm J,
        ← lintegral_const_mul'' _ (by fun_prop)]
      gcongr with ω
      simp [hB, ← mul_assoc]
    _ < ∞ := h'XY.2
-- 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 : NormedAddGroup F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ
this : LT.lt (α := ℝ≥0∞) ∞ ∞
⊢ False

Tactic:
contradiction