awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 ω ∂μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ Finset.cons j s hj, X i ω ∂μ = ∏ i ∈ Finset.cons j s hj, ∫⁻ (ω : Ω), X i ω ∂μ
have cons : ∫⁻ (ω : Ω), HMul.hMul (β := (a : Ω) → ℝ≥0∞) (X j) (∏ c ∈ s, X c) ω ∂μ =
  (∫⁻ (ω : Ω), X j ω ∂μ) * ∫⁻ (ω : Ω), (∏ c ∈ s, X c) ω ∂μ
Tactic: simp only [← Finset.prod_apply, Finset.prod_cons, ← ihs]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 ω ∂μ
⊢ ∫⁻ (ω : Ω), HMul.hMul (β := (a : Ω) → ℝ≥0∞) (X j) (∏ c ∈ s, X c) ω ∂μ =
    (∫⁻ (ω : Ω), X j ω ∂μ) * ∫⁻ (ω : Ω), (∏ c ∈ s, X c) ω ∂μ
have cons : AEMeasurable (X j) μ
Tactic: apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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) μ
⊢ ∫⁻ (ω : Ω), HMul.hMul (β := (a : Ω) → ℝ≥0∞) (X j) (∏ c ∈ s, X c) ω ∂μ =
    (∫⁻ (ω : Ω), X j ω ∂μ) * ∫⁻ (ω : Ω), (∏ c ∈ s, X c) ω ∂μ
have cons₁ : AEMeasurable (β := ℝ≥0∞) (∏ c ∈ s, X c) μ
Tactic: apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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) μ
⊢ ∫⁻ (ω : Ω), HMul.hMul (β := (a : Ω) → ℝ≥0∞) (X j) (∏ c ∈ s, X c) ω ∂μ =
    (∫⁻ (ω : Ω), X j ω ∂μ) * ∫⁻ (ω : Ω), (∏ c ∈ s, X c) ω ∂μ
have cons₂ : X j ⟂ᵢ[μ] ∏ c ∈ s, X c
Tactic: apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
have empty : ∫⁻ (ω : Ω), ∏ i ∈ ∅, X i ω ∂μ = ∏ i ∈ ∅, ∫⁻ (ω : Ω), 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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 ω ∂μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
have 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 ω ∂μ
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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 ω)) μ
have refine : HasFiniteIntegral.{u_1, u_7} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
Tactic: refine ⟨cB.comp_aestronglyMeasurable₂ hX.1 hY.1, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 ω‖ₑ ∂μ
have rw : ∫⁻ (a : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) a) ∂μ ≤ ∫⁻ (a : Ω), (↑C : ℝ≥0∞) * (‖X a‖ₑ * ‖Y a‖ₑ) ∂μ
Tactic: rw [← lintegral_const_mul'' _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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) ∂μ ≤ ∫⁻ (a : Ω), (↑C : ℝ≥0∞) * (‖X a‖ₑ * ‖Y a‖ₑ) ∂μ
have hfg : ∀ (ω : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) ω) ≤ (↑C : ℝ≥0∞) * (‖X ω‖ₑ * ‖Y ω‖ₑ)
Tactic: gcongr with ω
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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∞) * ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ = (↑C : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)
have rw : (↑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)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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) ∂μ < ∞
have _ : ∫⁻ (a : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) a) ∂μ ≤ (↑C : ℝ≥0∞) * ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ
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)
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 ω‖ₑ ∂μ
⊢ ∫⁻ (a : Ω), enorm.{u_7} (E := G) ((fun (ω : Ω) ↦ B (X ω) (Y ω)) a) ∂μ < ∞
have _₁ : (↑C : ℝ≥0∞) * ∫⁻ (ω : Ω), ‖X ω‖ₑ * ‖Y ω‖ₑ ∂μ = (↑C : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)
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)
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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
⊢ Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (X ω) : F →L[𝕜] G) : (a : F) → G) (Y ω)) μ
have 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‖ₑ
Tactic: refine hXY.integrable_op hX hY (B · ·) (by fun_prop) ‖B‖₊ (fun x y ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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) ≤
    (↑‖B‖₊ : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ
have 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
Tactic: rw [← toReal_le_toReal (by finiteness) (by finiteness)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 μ
have refine : HasFiniteIntegral X μ
Tactic: refine ⟨hX, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
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
⊢ False
have I : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (ω : Ω) ↦ ‖Y ω‖ₑ) 0
Tactic: have I : (fun ω => ‖Y ω‖ₑ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hY.enorm).1 H
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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
⊢ False
have apply : Y =ᶠ[ae μ] 0
Tactic: apply h'Y
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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
⊢ Y =ᶠ[ae μ] 0
have h : ∀ (ω : Ω) (hω : ‖Y ω‖ₑ = 0 ω), Y ω = 0 ω
Tactic: filter_upwards [I] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
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
⊢ HasFiniteIntegral X μ
have I : ∫⁻ (ω : Ω), ‖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ω
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 μ
have refine : ∀ (H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞), False
Tactic: refine hasFiniteIntegral_iff_enorm.mpr <| lt_top_iff_ne_top.2 fun H => ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
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‖ₑ ∂μ = ∞
⊢ False
have J : (fun (x : Ω) ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun (x : Ω) ↦ ‖Y x‖ₑ
Tactic: have J : (‖X ·‖ₑ) ⟂ᵢ[μ] (‖Y ·‖ₑ) := hXY.comp measurable_enorm measurable_enorm
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 ω‖ₑ ∂μ)
have rw : ∞ = (↑c : ℝ≥0∞) * (∞ * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)
Tactic: rw [H, top_mul I, mul_top (by simpa)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 ω‖ₑ ∂μ)
⊢ ∞ = (↑c : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)
have rw₁ : ∞ = (↑c : ℝ≥0∞) * ∞
Tactic: rw [H, top_mul I, mul_top (by simpa)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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∞) * ∞
⊢ ∞ = (↑c : ℝ≥0∞) * ((∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ) * ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ)
have rw₂ : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [H, top_mul I, mul_top (by simpa)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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 ω)‖ₑ ∂μ
have rw : ∫⁻ (a : Ω), (↑c : ℝ≥0∞) * (‖X a‖ₑ * ‖Y a‖ₑ) ∂μ ≤ ∫⁻ (ω : Ω), ‖B (X ω) (Y ω)‖ₑ ∂μ
Tactic: rw [← lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.enorm hY.enorm J,
        ← lintegral_const_mul'' _ (by fun_prop)]