[GOAL]
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_meas_f : Measurable f
⊢ ∫⁻ (ω : Ω), f ω * indicator T (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
revert f
[GOAL]
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
⊢ ∀ {f : Ω → ℝ≥0∞},
    Measurable f →
      ∫⁻ (ω : Ω), f ω * indicator T (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
have h_mul_indicator : ∀ g, Measurable g → Measurable fun a => g a * T.indicator (fun _ => c) a := fun g h_mg =>
  h_mg.mul (measurable_const.indicator h_meas_T)
[GOAL]
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
⊢ ∀ {f : Ω → ℝ≥0∞},
    Measurable f →
      ∫⁻ (ω : Ω), f ω * indicator T (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
apply @Measurable.ennreal_induction _ Mf
[GOAL]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
⊢ ∀ (c_1 : ℝ≥0∞) ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), indicator s (fun x => c_1) ω * indicator T (fun x => c) ω ∂μ =
        (∫⁻ (ω : Ω), indicator s (fun x => c_1) ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
intro c' s' h_meas_s'
[GOAL]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (ω : Ω), indicator s' (fun x => c') ω * indicator T (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), indicator s' (fun x => c') ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
simp_rw [← inter_indicator_mul]
[GOAL]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (ω : Ω), indicator (s' ∩ T) (fun x => c' * c) ω ∂μ =
    (∫⁻ (ω : Ω), indicator s' (fun x => c') ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
rw [lintegral_indicator _ (MeasurableSet.inter (hMf _ h_meas_s') h_meas_T), lintegral_indicator _ (hMf _ h_meas_s'),
  lintegral_indicator _ h_meas_T]
[GOAL]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (a : Ω) in T, c ∂μ
[PROOFSTEP]
simp only [measurable_const, lintegral_const, univ_inter, lintegral_const_mul, MeasurableSet.univ,
  Measure.restrict_apply]
[GOAL]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ c' * c * ↑↑μ (s' ∩ T) = c' * ↑↑μ s' * (c * ↑↑μ T)
[PROOFSTEP]
rw [IndepSets_iff] at h_ind
[GOAL]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : ∀ (t1 t2 : Set Ω), t1 ∈ {s | MeasurableSet s} → t2 ∈ {T} → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ c' * c * ↑↑μ (s' ∩ T) = c' * ↑↑μ s' * (c * ↑↑μ T)
[PROOFSTEP]
rw [mul_mul_mul_comm, h_ind s' T h_meas_s' (Set.mem_singleton _)]
[GOAL]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
⊢ ∀ ⦃f g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * indicator T (fun x => c) ω ∂μ =
              (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ →
            ∫⁻ (ω : Ω), g ω * indicator T (fun x => c) ω ∂μ =
                (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ →
              ∫⁻ (ω : Ω), (f + g) ω * indicator T (fun x => c) ω ∂μ =
                (∫⁻ (ω : Ω), (f + g) ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
intro f' g _ h_meas_f' _ h_ind_f' h_ind_g
[GOAL]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * indicator T (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * indicator T (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
⊢ ∫⁻ (ω : Ω), (f' + g) ω * indicator T (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
have h_measM_f' : Measurable f' := h_meas_f'.mono hMf le_rfl
[GOAL]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * indicator T (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * indicator T (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), (f' + g) ω * indicator T (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), (f' + g) ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
simp_rw [Pi.add_apply, right_distrib]
[GOAL]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_meas_f' : Measurable f'
a✝ : Measurable g
h_ind_f' :
  ∫⁻ (ω : Ω), f' ω * indicator T (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f' ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_ind_g :
  ∫⁻ (ω : Ω), g ω * indicator T (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f' ω * indicator T (fun x => c) ω + g ω * indicator T (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), f' ω + g ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
rw [lintegral_add_left (h_mul_indicator _ h_measM_f'), lintegral_add_left h_measM_f', right_distrib, h_ind_f', h_ind_g]
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
⊢ ∀ ⦃f : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ),
            ∫⁻ (ω : Ω), f n ω * indicator T (fun x => c) ω ∂μ =
              (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ) →
          ∫⁻ (ω : Ω), (fun x => ⨆ (n : ℕ), f n x) ω * indicator T (fun x => c) ω ∂μ =
            (∫⁻ (ω : Ω), (fun x => ⨆ (n : ℕ), f n x) ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
intro f h_meas_f h_mono_f h_ind_f
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * indicator T (fun x => c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
⊢ ∫⁻ (ω : Ω), (fun x => ⨆ (n : ℕ), f n x) ω * indicator T (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), (fun x => ⨆ (n : ℕ), f n x) ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
have h_measM_f : ∀ n, Measurable (f n) := fun n => (h_meas_f n).mono hMf le_rfl
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * indicator T (fun x => c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ∫⁻ (ω : Ω), (fun x => ⨆ (n : ℕ), f n x) ω * indicator T (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), (fun x => ⨆ (n : ℕ), f n x) ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
simp_rw [ENNReal.iSup_mul]
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * indicator T (fun x => c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ∫⁻ (ω : Ω), ⨆ (i : ℕ), f i ω * indicator T (fun x => c) ω ∂μ =
    (∫⁻ (ω : Ω), ⨆ (n : ℕ), f n ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
rw [lintegral_iSup h_measM_f h_mono_f, lintegral_iSup, ENNReal.iSup_mul]
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * indicator T (fun x => c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ⨆ (n : ℕ), ∫⁻ (a : Ω), f n a * indicator T (fun x => c) a ∂μ =
    ⨆ (i : ℕ), (∫⁻ (a : Ω), f i a ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
[PROOFSTEP]
simp_rw [← h_ind_f]
[GOAL]
case h_iSup.hf
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * indicator T (fun x => c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ∀ (n : ℕ), Measurable fun ω => f n ω * indicator T (fun x => c) ω
[PROOFSTEP]
exact fun n => h_mul_indicator _ (h_measM_f n)
[GOAL]
case h_iSup.h_mono
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T}
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * indicator T (fun x => c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * indicator T (fun x => c) ω ∂μ =
      (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), indicator T (fun x => c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ Monotone fun i ω => f i ω * indicator T (fun x => c) ω
[PROOFSTEP]
exact fun m n h_le a => mul_le_mul_right' (h_mono_f h_le a) _
[GOAL]
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_meas_g : Measurable g
⊢ ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
[PROOFSTEP]
revert g
[GOAL]
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
⊢ ∀ {g : Ω → ℝ≥0∞}, Measurable g → ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
[PROOFSTEP]
have h_measM_f : Measurable f := h_meas_f.mono hMf le_rfl
[GOAL]
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
⊢ ∀ {g : Ω → ℝ≥0∞}, Measurable g → ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
[PROOFSTEP]
apply @Measurable.ennreal_induction _ Mg
[GOAL]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), f ω * indicator s (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), indicator s (fun x => c) ω ∂μ
[PROOFSTEP]
intro c s h_s
[GOAL]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ ∫⁻ (ω : Ω), f ω * indicator s (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), indicator s (fun x => c) ω ∂μ
[PROOFSTEP]
apply lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator hMf _ (hMg _ h_s) _ h_meas_f
[GOAL]
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ IndepSets {s | MeasurableSet s} {s}
[PROOFSTEP]
apply indepSets_of_indepSets_of_le_right h_ind
[GOAL]
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
c : ℝ≥0∞
s : Set Ω
h_s : MeasurableSet s
⊢ {s} ⊆ {s | MeasurableSet s}
[PROOFSTEP]
rwa [singleton_subset_iff]
[GOAL]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
⊢ ∀ ⦃f_1 g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * f_1 ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 ω ∂μ →
            ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ →
              ∫⁻ (ω : Ω), f ω * (f_1 + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f_1 + g) ω ∂μ
[PROOFSTEP]
intro f' g _ h_measMg_f' _ h_ind_f' h_ind_g'
[GOAL]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
a✝ : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
⊢ ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ
[PROOFSTEP]
have h_measM_f' : Measurable f' := h_measMg_f'.mono hMg le_rfl
[GOAL]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
a✝ : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ
[PROOFSTEP]
simp_rw [Pi.add_apply, left_distrib]
[GOAL]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
a✝ : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
[PROOFSTEP]
rw [lintegral_add_left h_measM_f', lintegral_add_left (h_measM_f.mul h_measM_f'), left_distrib, h_ind_f', h_ind_g']
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
⊢ ∀ ⦃f_1 : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f_1 n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f_1 n ω ∂μ) →
          ∫⁻ (ω : Ω), f ω * (fun x => ⨆ (n : ℕ), f_1 n x) ω ∂μ =
            (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun x => ⨆ (n : ℕ), f_1 n x) ω ∂μ
[PROOFSTEP]
intro f' h_meas_f' h_mono_f' h_ind_f'
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
⊢ ∫⁻ (ω : Ω), f ω * (fun x => ⨆ (n : ℕ), f' n x) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun x => ⨆ (n : ℕ), f' n x) ω ∂μ
[PROOFSTEP]
have h_measM_f' : ∀ n, Measurable (f' n) := fun n => (h_meas_f' n).mono hMg le_rfl
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ∫⁻ (ω : Ω), f ω * (fun x => ⨆ (n : ℕ), f' n x) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (fun x => ⨆ (n : ℕ), f' n x) ω ∂μ
[PROOFSTEP]
simp_rw [ENNReal.mul_iSup]
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ∫⁻ (ω : Ω), ⨆ (i : ℕ), f ω * f' i ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), ⨆ (n : ℕ), f' n ω ∂μ
[PROOFSTEP]
rw [lintegral_iSup, lintegral_iSup h_measM_f' h_mono_f', ENNReal.mul_iSup]
[GOAL]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ⨆ (n : ℕ), ∫⁻ (a : Ω), f a * f' n a ∂μ = ⨆ (i : ℕ), (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' i a ∂μ
[PROOFSTEP]
simp_rw [← h_ind_f']
[GOAL]
case h_iSup.hf
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ∀ (n : ℕ), Measurable fun ω => f ω * f' n ω
[PROOFSTEP]
exact fun n => h_measM_f.mul (h_measM_f' n)
[GOAL]
case h_iSup.h_mono
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ Monotone fun i ω => f ω * f' i ω
[PROOFSTEP]
exact fun n m (h_le : n ≤ m) a => mul_le_mul_left' (h_mono_f' h_le a) _
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
h_meas_f : AEMeasurable f
h_meas_g : AEMeasurable g
h_indep_fun : IndepFun f g
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
[PROOFSTEP]
have fg_ae : f * g =ᵐ[μ] h_meas_f.mk _ * h_meas_g.mk _ := h_meas_f.ae_eq_mk.mul h_meas_g.ae_eq_mk
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
h_meas_f : AEMeasurable f
h_meas_g : AEMeasurable g
h_indep_fun : IndepFun f g
fg_ae : f * g =ᵐ[μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
[PROOFSTEP]
rw [lintegral_congr_ae h_meas_f.ae_eq_mk, lintegral_congr_ae h_meas_g.ae_eq_mk, lintegral_congr_ae fg_ae]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
h_meas_f : AEMeasurable f
h_meas_g : AEMeasurable g
h_indep_fun : IndepFun f g
fg_ae : f * g =ᵐ[μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (a : Ω), (AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g) a ∂μ =
    (∫⁻ (a : Ω), AEMeasurable.mk f h_meas_f a ∂μ) * ∫⁻ (a : Ω), AEMeasurable.mk g h_meas_g a ∂μ
[PROOFSTEP]
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun h_meas_f.measurable_mk h_meas_g.measurable_mk
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
h_meas_f : AEMeasurable f
h_meas_g : AEMeasurable g
h_indep_fun : IndepFun f g
fg_ae : f * g =ᵐ[μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ IndepFun (AEMeasurable.mk f h_meas_f) (AEMeasurable.mk g h_meas_g)
[PROOFSTEP]
exact h_indep_fun.ae_eq h_meas_f.ae_eq_mk h_meas_g.ae_eq_mk
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
⊢ Integrable (X * Y)
[PROOFSTEP]
let nX : Ω → ENNReal := fun a => ‖X a‖₊
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊
⊢ Integrable (X * Y)
[PROOFSTEP]
let nY : Ω → ENNReal := fun a => ‖Y a‖₊
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊
nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊
⊢ Integrable (X * Y)
[PROOFSTEP]
have hXY' : IndepFun (fun a => ‖X a‖₊) (fun a => ‖Y a‖₊) μ := hXY.comp measurable_nnnorm measurable_nnnorm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊
nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊
hXY' : IndepFun (fun a => ‖X a‖₊) fun a => ‖Y a‖₊
⊢ Integrable (X * Y)
[PROOFSTEP]
have hXY'' : IndepFun nX nY μ := hXY'.comp measurable_coe_nnreal_ennreal measurable_coe_nnreal_ennreal
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊
nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊
hXY' : IndepFun (fun a => ‖X a‖₊) fun a => ‖Y a‖₊
hXY'' : IndepFun nX nY
⊢ Integrable (X * Y)
[PROOFSTEP]
have hnX : AEMeasurable nX μ := hX.1.aemeasurable.nnnorm.coe_nnreal_ennreal
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊
nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊
hXY' : IndepFun (fun a => ‖X a‖₊) fun a => ‖Y a‖₊
hXY'' : IndepFun nX nY
hnX : AEMeasurable nX
⊢ Integrable (X * Y)
[PROOFSTEP]
have hnY : AEMeasurable nY μ := hY.1.aemeasurable.nnnorm.coe_nnreal_ennreal
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊
nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊
hXY' : IndepFun (fun a => ‖X a‖₊) fun a => ‖Y a‖₊
hXY'' : IndepFun nX nY
hnX : AEMeasurable nX
hnY : AEMeasurable nY
⊢ Integrable (X * Y)
[PROOFSTEP]
have hmul : ∫⁻ a, nX a * nY a ∂μ = (∫⁻ a, nX a ∂μ) * ∫⁻ a, nY a ∂μ :=
  lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' hnX hnY hXY''
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊
nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊
hXY' : IndepFun (fun a => ‖X a‖₊) fun a => ‖Y a‖₊
hXY'' : IndepFun nX nY
hnX : AEMeasurable nX
hnY : AEMeasurable nY
hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ
⊢ Integrable (X * Y)
[PROOFSTEP]
refine' ⟨hX.1.mul hY.1, _⟩
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊
nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊
hXY' : IndepFun (fun a => ‖X a‖₊) fun a => ‖Y a‖₊
hXY'' : IndepFun nX nY
hnX : AEMeasurable nX
hnY : AEMeasurable nY
hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ
⊢ HasFiniteIntegral (X * Y)
[PROOFSTEP]
simp_rw [HasFiniteIntegral, Pi.mul_apply, nnnorm_mul, ENNReal.coe_mul, hmul]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊
nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊
hXY' : IndepFun (fun a => ‖X a‖₊) fun a => ‖Y a‖₊
hXY'' : IndepFun nX nY
hnX : AEMeasurable nX
hnY : AEMeasurable nY
hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ
⊢ (∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ) * ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ < ⊤
[PROOFSTEP]
exact ENNReal.mul_lt_top hX.2.ne hY.2.ne
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
⊢ Integrable X
[PROOFSTEP]
refine' ⟨hX, _⟩
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
⊢ HasFiniteIntegral X
[PROOFSTEP]
have I : (∫⁻ ω, ‖Y ω‖₊ ∂μ) ≠ 0 := fun H ↦
  by
  have I : (fun ω => ‖Y ω‖₊ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hY.ennnorm).1 H
  apply h'Y
  filter_upwards [I] with ω hω
  simpa using hω
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ = 0
⊢ False
[PROOFSTEP]
have I : (fun ω => ‖Y ω‖₊ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hY.ennnorm).1 H
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ = 0
I : (fun ω => ↑‖Y ω‖₊) =ᵐ[μ] 0
⊢ False
[PROOFSTEP]
apply h'Y
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ = 0
I : (fun ω => ↑‖Y ω‖₊) =ᵐ[μ] 0
⊢ Y =ᵐ[μ] 0
[PROOFSTEP]
filter_upwards [I] with ω hω
[GOAL]
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ = 0
I : (fun ω => ↑‖Y ω‖₊) =ᵐ[μ] 0
ω : Ω
hω : ↑‖Y ω‖₊ = OfNat.ofNat 0 ω
⊢ Y ω = OfNat.ofNat 0 ω
[PROOFSTEP]
simpa using hω
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0
⊢ HasFiniteIntegral X
[PROOFSTEP]
refine lt_top_iff_ne_top.2 fun H => ?_
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤
⊢ False
[PROOFSTEP]
have J : IndepFun (fun ω => ‖X ω‖₊ : Ω → ℝ≥0∞) (fun ω => ‖Y ω‖₊ : Ω → ℝ≥0∞) μ :=
  by
  have M : Measurable fun x : β => (‖x‖₊ : ℝ≥0∞) := measurable_nnnorm.coe_nnreal_ennreal
  apply IndepFun.comp hXY M M
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤
⊢ IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
[PROOFSTEP]
have M : Measurable fun x : β => (‖x‖₊ : ℝ≥0∞) := measurable_nnnorm.coe_nnreal_ennreal
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤
M : Measurable fun x => ↑‖x‖₊
⊢ IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
[PROOFSTEP]
apply IndepFun.comp hXY M M
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
⊢ False
[PROOFSTEP]
have A : (∫⁻ ω, ‖X ω * Y ω‖₊ ∂μ) < ∞ := h'XY.2
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : ∫⁻ (ω : Ω), ↑‖X ω * Y ω‖₊ ∂μ < ⊤
⊢ False
[PROOFSTEP]
simp only [nnnorm_mul, ENNReal.coe_mul] at A
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : ∫⁻ (ω : Ω), ↑‖X ω‖₊ * ↑‖Y ω‖₊ ∂μ < ⊤
⊢ False
[PROOFSTEP]
rw [lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.ennnorm hY.ennnorm J, H] at A
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : ⊤ * ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ < ⊤
⊢ False
[PROOFSTEP]
simp only [ENNReal.top_mul I] at A
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
⊢ Integrable Y
[PROOFSTEP]
refine' ⟨hY, _⟩
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
⊢ HasFiniteIntegral Y
[PROOFSTEP]
have I : (∫⁻ ω, ‖X ω‖₊ ∂μ) ≠ 0 := fun H ↦
  by
  have I : (fun ω => ‖X ω‖₊ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hX.ennnorm).1 H
  apply h'X
  filter_upwards [I] with ω hω
  simpa using hω
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ = 0
⊢ False
[PROOFSTEP]
have I : (fun ω => ‖X ω‖₊ : Ω → ℝ≥0∞) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' hX.ennnorm).1 H
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ = 0
I : (fun ω => ↑‖X ω‖₊) =ᵐ[μ] 0
⊢ False
[PROOFSTEP]
apply h'X
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ = 0
I : (fun ω => ↑‖X ω‖₊) =ᵐ[μ] 0
⊢ X =ᵐ[μ] 0
[PROOFSTEP]
filter_upwards [I] with ω hω
[GOAL]
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ = 0
I : (fun ω => ↑‖X ω‖₊) =ᵐ[μ] 0
ω : Ω
hω : ↑‖X ω‖₊ = OfNat.ofNat 0 ω
⊢ X ω = OfNat.ofNat 0 ω
[PROOFSTEP]
simpa using hω
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0
⊢ HasFiniteIntegral Y
[PROOFSTEP]
refine lt_top_iff_ne_top.2 fun H => ?_
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤
⊢ False
[PROOFSTEP]
have J : IndepFun (fun ω => ‖X ω‖₊ : Ω → ℝ≥0∞) (fun ω => ‖Y ω‖₊ : Ω → ℝ≥0∞) μ :=
  by
  have M : Measurable fun x : β => (‖x‖₊ : ℝ≥0∞) := measurable_nnnorm.coe_nnreal_ennreal
  apply IndepFun.comp hXY M M
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤
⊢ IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
[PROOFSTEP]
have M : Measurable fun x : β => (‖x‖₊ : ℝ≥0∞) := measurable_nnnorm.coe_nnreal_ennreal
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤
M : Measurable fun x => ↑‖x‖₊
⊢ IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
[PROOFSTEP]
apply IndepFun.comp hXY M M
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
⊢ False
[PROOFSTEP]
have A : (∫⁻ ω, ‖X ω * Y ω‖₊ ∂μ) < ∞ := h'XY.2
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : ∫⁻ (ω : Ω), ↑‖X ω * Y ω‖₊ ∂μ < ⊤
⊢ False
[PROOFSTEP]
simp only [nnnorm_mul, ENNReal.coe_mul] at A
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : ∫⁻ (ω : Ω), ↑‖X ω‖₊ * ↑‖Y ω‖₊ ∂μ < ⊤
⊢ False
[PROOFSTEP]
rw [lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' hX.ennnorm hY.ennnorm J, H] at A
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X✝ Y✝ : Ω → ℝ
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y
h'XY : Integrable (X * Y)
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ↑‖Y a‖₊ ∂μ = ⊤
J : IndepFun (fun ω => ↑‖X ω‖₊) fun ω => ↑‖Y ω‖₊
A : (∫⁻ (ω : Ω), ↑‖X ω‖₊ ∂μ) * ⊤ < ⊤
⊢ False
[PROOFSTEP]
simp only [ENNReal.mul_top I] at A
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ := ENNReal.measurable_ofReal.comp_aemeasurable hXm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ := ENNReal.measurable_ofReal.comp_aemeasurable hYm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have h3 : AEMeasurable (X * Y) μ := hXm.mul hYm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have h4 : 0 ≤ᵐ[μ] X * Y := ae_of_all _ fun ω => mul_nonneg (hXp ω) (hYp ω)
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ hXp) hXm.aestronglyMeasurable,
  integral_eq_lintegral_of_nonneg_ae (ae_of_all _ hYp) hYm.aestronglyMeasurable,
  integral_eq_lintegral_of_nonneg_ae h4 h3.aestronglyMeasurable]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal ((X * Y) a) ∂μ) =
    ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ)
[PROOFSTEP]
simp_rw [← ENNReal.toReal_mul, Pi.mul_apply, ENNReal.ofReal_mul (hXp _)]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ ENNReal.toReal (∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ) =
    ENNReal.toReal ((∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ)
[PROOFSTEP]
congr
[GOAL]
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ ∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ =
    (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ
[PROOFSTEP]
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' h1 h2
[GOAL]
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hXp : 0 ≤ X
hYp : 0 ≤ Y
hXm : AEMeasurable X
hYm : AEMeasurable Y
h1 : AEMeasurable fun a => ENNReal.ofReal (X a)
h2 : AEMeasurable fun a => ENNReal.ofReal (Y a)
h3 : AEMeasurable (X * Y)
h4 : 0 ≤ᵐ[μ] X * Y
⊢ IndepFun (fun a => ENNReal.ofReal (X a)) fun a => ENNReal.ofReal (Y a)
[PROOFSTEP]
exact hXY.comp ENNReal.measurable_ofReal ENNReal.measurable_ofReal
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
let pos : ℝ → ℝ := fun x => max x 0
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
let neg : ℝ → ℝ := fun x => max (-x) 0
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have posm : Measurable pos := measurable_id'.max measurable_const
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have negm : Measurable neg := measurable_id'.neg.max measurable_const
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
let Xp := pos ∘ X
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
let Xm := neg ∘ X
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
let Yp := pos ∘ Y
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
let Ym := neg ∘ Y
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hXpm : X = Xp - Xm := funext fun ω => (max_zero_sub_max_neg_zero_eq_self (X ω)).symm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hYpm : Y = Yp - Ym := funext fun ω => (max_zero_sub_max_neg_zero_eq_self (Y ω)).symm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hp1 : 0 ≤ Xm := fun ω => le_max_right _ _
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hp2 : 0 ≤ Xp := fun ω => le_max_right _ _
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hp3 : 0 ≤ Ym := fun ω => le_max_right _ _
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hp4 : 0 ≤ Yp := fun ω => le_max_right _ _
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hm1 : AEMeasurable Xm μ := hX.1.aemeasurable.neg.max aemeasurable_const
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hm2 : AEMeasurable Xp μ := hX.1.aemeasurable.max aemeasurable_const
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hm3 : AEMeasurable Ym μ := hY.1.aemeasurable.neg.max aemeasurable_const
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hm4 : AEMeasurable Yp μ := hY.1.aemeasurable.max aemeasurable_const
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hv1 : Integrable Xm μ := hX.neg_part
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hv2 : Integrable Xp μ := hX.pos_part
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hv3 : Integrable Ym μ := hY.neg_part
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hv4 : Integrable Yp μ := hY.pos_part
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hi1 : IndepFun Xm Ym μ := hXY.comp negm negm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hi2 : IndepFun Xp Ym μ := hXY.comp posm negm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hi3 : IndepFun Xm Yp μ := hXY.comp negm posm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hi4 : IndepFun Xp Yp μ := hXY.comp posm posm
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
hi4 : IndepFun Xp Yp
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hl1 : Integrable (Xm * Ym) μ := hi1.integrable_mul hv1 hv3
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
hi4 : IndepFun Xp Yp
hl1 : Integrable (Xm * Ym)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hl2 : Integrable (Xp * Ym) μ := hi2.integrable_mul hv2 hv3
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
hi4 : IndepFun Xp Yp
hl1 : Integrable (Xm * Ym)
hl2 : Integrable (Xp * Ym)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hl3 : Integrable (Xm * Yp) μ := hi3.integrable_mul hv1 hv4
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
hi4 : IndepFun Xp Yp
hl1 : Integrable (Xm * Ym)
hl2 : Integrable (Xp * Ym)
hl3 : Integrable (Xm * Yp)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hl4 : Integrable (Xp * Yp) μ := hi4.integrable_mul hv2 hv4
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
hi4 : IndepFun Xp Yp
hl1 : Integrable (Xm * Ym)
hl2 : Integrable (Xp * Ym)
hl3 : Integrable (Xm * Yp)
hl4 : Integrable (Xp * Yp)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hl5 : Integrable (Xp * Yp - Xm * Yp) μ := hl4.sub hl3
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
hi4 : IndepFun Xp Yp
hl1 : Integrable (Xm * Ym)
hl2 : Integrable (Xp * Ym)
hl3 : Integrable (Xm * Yp)
hl4 : Integrable (Xp * Yp)
hl5 : Integrable (Xp * Yp - Xm * Yp)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have hl6 : Integrable (Xp * Ym - Xm * Ym) μ := hl2.sub hl1
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
hi4 : IndepFun Xp Yp
hl1 : Integrable (Xm * Ym)
hl2 : Integrable (Xp * Ym)
hl3 : Integrable (Xm * Yp)
hl4 : Integrable (Xp * Yp)
hl5 : Integrable (Xp * Yp - Xm * Yp)
hl6 : Integrable (Xp * Ym - Xm * Ym)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
rw [hXpm, hYpm, mul_sub, sub_mul, sub_mul]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
hi4 : IndepFun Xp Yp
hl1 : Integrable (Xm * Ym)
hl2 : Integrable (Xp * Ym)
hl3 : Integrable (Xm * Yp)
hl4 : Integrable (Xp * Yp)
hl5 : Integrable (Xp * Yp - Xm * Yp)
hl6 : Integrable (Xp * Ym - Xm * Ym)
⊢ integral μ (Xp * Yp - Xm * Yp - (Xp * Ym - Xm * Ym)) = integral μ (Xp - Xm) * integral μ (Yp - Ym)
[PROOFSTEP]
rw [integral_sub' hl5 hl6, integral_sub' hl4 hl3, integral_sub' hl2 hl1, integral_sub' hv2 hv1, integral_sub' hv4 hv3,
  hi1.integral_mul_of_nonneg hp1 hp3 hm1 hm3, hi2.integral_mul_of_nonneg hp2 hp3 hm2 hm3,
  hi3.integral_mul_of_nonneg hp1 hp4 hm1 hm4, hi4.integral_mul_of_nonneg hp2 hp4 hm2 hm4]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : Integrable X
hY : Integrable Y
pos : ℝ → ℝ := fun x => max x 0
neg : ℝ → ℝ := fun x => max (-x) 0
posm : Measurable pos
negm : Measurable neg
Xp : Ω → ℝ := pos ∘ X
Xm : Ω → ℝ := neg ∘ X
Yp : Ω → ℝ := pos ∘ Y
Ym : Ω → ℝ := neg ∘ Y
hXpm : X = Xp - Xm
hYpm : Y = Yp - Ym
hp1 : 0 ≤ Xm
hp2 : 0 ≤ Xp
hp3 : 0 ≤ Ym
hp4 : 0 ≤ Yp
hm1 : AEMeasurable Xm
hm2 : AEMeasurable Xp
hm3 : AEMeasurable Ym
hm4 : AEMeasurable Yp
hv1 : Integrable Xm
hv2 : Integrable Xp
hv3 : Integrable Ym
hv4 : Integrable Yp
hi1 : IndepFun Xm Ym
hi2 : IndepFun Xp Ym
hi3 : IndepFun Xm Yp
hi4 : IndepFun Xp Yp
hl1 : Integrable (Xm * Ym)
hl2 : Integrable (Xp * Ym)
hl3 : Integrable (Xm * Yp)
hl4 : Integrable (Xp * Yp)
hl5 : Integrable (Xp * Yp - Xm * Yp)
hl6 : Integrable (Xp * Ym - Xm * Ym)
⊢ integral μ Xp * integral μ Yp - integral μ Xm * integral μ Yp -
      (integral μ Xp * integral μ Ym - integral μ Xm * integral μ Ym) =
    (∫ (a : Ω), Xp a ∂μ - ∫ (a : Ω), Xm a ∂μ) * (∫ (a : Ω), Yp a ∂μ - ∫ (a : Ω), Ym a ∂μ)
[PROOFSTEP]
ring
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
by_cases h'X : X =ᵐ[μ] 0
[GOAL]
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have h' : X * Y =ᵐ[μ] 0 := by
  filter_upwards [h'X] with ω hω
  simp [hω]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
⊢ X * Y =ᵐ[μ] 0
[PROOFSTEP]
filter_upwards [h'X] with ω hω
[GOAL]
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
ω : Ω
hω : X ω = OfNat.ofNat 0 ω
⊢ (X * Y) ω = OfNat.ofNat 0 ω
[PROOFSTEP]
simp [hω]
[GOAL]
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : X =ᵐ[μ] 0
h' : X * Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
simp only [integral_congr_ae h'X, integral_congr_ae h', Pi.zero_apply, integral_const, Algebra.id.smul_eq_mul, mul_zero,
  zero_mul]
[GOAL]
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
by_cases h'Y : Y =ᵐ[μ] 0
[GOAL]
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have h' : X * Y =ᵐ[μ] 0 := by
  filter_upwards [h'Y] with ω hω
  simp [hω]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
⊢ X * Y =ᵐ[μ] 0
[PROOFSTEP]
filter_upwards [h'Y] with ω hω
[GOAL]
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
ω : Ω
hω : Y ω = OfNat.ofNat 0 ω
⊢ (X * Y) ω = OfNat.ofNat 0 ω
[PROOFSTEP]
simp [hω]
[GOAL]
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : Y =ᵐ[μ] 0
h' : X * Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
simp only [integral_congr_ae h'Y, integral_congr_ae h', Pi.zero_apply, integral_const, Algebra.id.smul_eq_mul, mul_zero,
  zero_mul]
[GOAL]
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
by_cases h : Integrable (X * Y) μ
[GOAL]
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : Integrable (X * Y)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have HX : Integrable X μ := hXY.integrable_left_of_integrable_mul h hX hY h'Y
[GOAL]
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : Integrable (X * Y)
HX : Integrable X
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
have HY : Integrable Y μ := hXY.integrable_right_of_integrable_mul h hX hY h'X
[GOAL]
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : Integrable (X * Y)
HX : Integrable X
HY : Integrable Y
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
exact hXY.integral_mul_of_integrable HX HY
[GOAL]
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
⊢ integral μ (X * Y) = integral μ X * integral μ Y
[PROOFSTEP]
rw [integral_undef h]
[GOAL]
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
⊢ 0 = integral μ X * integral μ Y
[PROOFSTEP]
have I : ¬(Integrable X μ ∧ Integrable Y μ) := by
  rintro ⟨HX, HY⟩
  exact h (hXY.integrable_mul HX HY)
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
⊢ ¬(Integrable X ∧ Integrable Y)
[PROOFSTEP]
rintro ⟨HX, HY⟩
[GOAL]
case intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
HX : Integrable X
HY : Integrable Y
⊢ False
[PROOFSTEP]
exact h (hXY.integrable_mul HX HY)
[GOAL]
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
I : ¬(Integrable X ∧ Integrable Y)
⊢ 0 = integral μ X * integral μ Y
[PROOFSTEP]
rw [not_and_or] at I
[GOAL]
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
I : ¬Integrable X ∨ ¬Integrable Y
⊢ 0 = integral μ X * integral μ Y
[PROOFSTEP]
cases' I with I I
[GOAL]
case neg.inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
I : ¬Integrable X
⊢ 0 = integral μ X * integral μ Y
[PROOFSTEP]
simp [integral_undef I]
[GOAL]
case neg.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
hXY : IndepFun X Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᵐ[μ] 0
h'Y : ¬Y =ᵐ[μ] 0
h : ¬Integrable (X * Y)
I : ¬Integrable Y
⊢ 0 = integral μ X * integral μ Y
[PROOFSTEP]
simp [integral_undef I]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ IndepFun f g ↔
    ∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) → Integrable (ψ ∘ g) → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
[PROOFSTEP]
refine' ⟨fun hfg _ _ hφ hψ => IndepFun.integral_mul_of_integrable (hfg.comp hφ hψ), _⟩
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) →
            Integrable (ψ ∘ g) → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    IndepFun f g
[PROOFSTEP]
rw [IndepFun_iff]
[GOAL]
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) →
            Integrable (ψ ∘ g) → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
[PROOFSTEP]
rintro h _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩
[GOAL]
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
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
⊢ ↑↑μ (f ⁻¹' A ∩ g ⁻¹' B) = ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B)
[PROOFSTEP]
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))
[GOAL]
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (indicator A 1 ∘ f * indicator B 1 ∘ g) = integral μ (indicator A 1 ∘ f) * integral μ (indicator B 1 ∘ g)
⊢ ↑↑μ (f ⁻¹' A ∩ g ⁻¹' B) = ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B)
[PROOFSTEP]
rwa [← ENNReal.toReal_eq_toReal (measure_ne_top μ _), ENNReal.toReal_mul, ←
  integral_indicator_one ((hfm hA).inter (hgm hB)), ← integral_indicator_one (hfm hA), ←
  integral_indicator_one (hgm hB), Set.inter_indicator_one]
[GOAL]
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (indicator A 1 ∘ f * indicator B 1 ∘ g) = integral μ (indicator A 1 ∘ f) * integral μ (indicator B 1 ∘ g)
⊢ ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B) ≠ ⊤
[PROOFSTEP]
exact ENNReal.mul_ne_top (measure_ne_top μ _) (measure_ne_top μ _)