Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω ∂μ
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω ∂μ
revert g
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω ∂μ
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω ∂μ
have h_measM_f : Measurable f := h_meas_f.mono hMf le_rfl
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ

case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ

case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω ∂μ
apply @Measurable.ennreal_induction _ Mg
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
intro c s h_s
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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}
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
apply lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator hMf _ (hMg _ h_s) _ h_meas_f
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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}
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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}
apply indepSets_of_indepSets_of_le_right h_ind
no goals
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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}
rwa [singleton_subset_iff]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
intro f' g _ h_measMg_f' _ h_ind_f' h_ind_g'
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
have h_measM_f' : Measurable f' := h_measMg_f'.mono hMg le_rfl
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω ∂μ
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
simp_rw [Pi.add_apply, left_distrib]
no goals
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω ∂μ
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']
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
intro f' h_meas_f' h_mono_f' h_ind_f'
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
have h_measM_f' : ∀ n, Measurable (f' n) := fun n => (h_meas_f' n).mono hMg le_rfl
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω ∂μ
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
simp_rw [ENNReal.mul_iSup]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ∂μ

case h_iSup.hf
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω

case h_iSup.h_mono
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω ∂μ
rw [lintegral_iSup, lintegral_iSup h_measM_f' h_mono_f', ENNReal.mul_iSup]
no goals
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ∂μ
simp_rw [← h_ind_f']
no goals
case h_iSup.hf
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω
exact fun n => h_measM_f.mul (h_measM_f' n)
no goals
case h_iSup.h_mono
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
f : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf Mg mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ω
exact fun n m (h_le : n ≤ m) a => mul_le_mul_left' (h_mono_f' h_le a) _