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

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

case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
apply @Measurable.ennreal_induction _ Mf
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
intro c' s' h_meas_s'
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
simp_rw [← inter_indicator_mul]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ∂μ
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
rw [lintegral_indicator _ (MeasurableSet.inter (hMf _ h_meas_s') h_meas_T),
  lintegral_indicator _ (hMf _ h_meas_s'), lintegral_indicator _ h_meas_T]
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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)
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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 ∂μ
simp only [measurable_const, lintegral_const, univ_inter, lintegral_const_mul,
  MeasurableSet.univ, Measure.restrict_apply]
no goals
case h_ind
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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)
rw [mul_mul_mul_comm, h_ind s' T h_meas_s' (Set.mem_singleton _)]
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
intro f' g _ h_meas_f' _ h_ind_f' h_ind_g
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
have h_measM_f' : Measurable f' := h_meas_f'.mono hMf le_rfl
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
simp_rw [Pi.add_apply, right_distrib]
no goals
case h_add
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
rw [lintegral_add_left (h_mul_indicator _ h_measM_f'), lintegral_add_left h_measM_f',
  right_distrib, h_ind_f', h_ind_g]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
intro f h_meas_f h_mono_f h_ind_f
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
have h_measM_f : ∀ n, Measurable (f n) := fun n => (h_meas_f n).mono hMf le_rfl
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ
simp_rw [ENNReal.iSup_mul]
case h_iSup
Ω : Type u_1
mΩ✝ : MeasurableSpace Ω
μ✝ : MeasureTheory.Measure Ω
g : Ω → ℝ≥0∞
X Y : Ω → ℝ
Mf mΩ : MeasurableSpace Ω
μ : MeasureTheory.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) ω ∂μ

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

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