case h_ind
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      (∫⁻ (a : α), indicator s (fun x => c) a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * indicator s fun x => c) a ∂μ

case h_add
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (support f_1) (support g) →
      Measurable f_1 →
        Measurable g →
          ((∫⁻ (a : α), f_1 a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * f_1) a ∂μ) →
            ((∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ) →
              (∫⁻ (a : α), (f_1 + g) a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ

case h_iSup
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), (∫⁻ (a : α), f_1 n a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), f_1 n x) a ∂Measure.withDensity μ f) =
            ∫⁻ (a : α), (f * fun x => ⨆ (n : ℕ), f_1 n x) a ∂μ
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ {g : α → ℝ≥0∞}, Measurable g → (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
apply Measurable.ennreal_induction
case h_ind
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
c : ℝ≥0∞
s : Set α
h_ms : MeasurableSet s
⊢ (∫⁻ (a : α), indicator s (fun x => c) a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * indicator s fun x => c) a ∂μ
case h_ind
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      (∫⁻ (a : α), indicator s (fun x => c) a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * indicator s fun x => c) a ∂μ
intro c s h_ms
no goals
case h_ind
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
c : ℝ≥0∞
s : Set α
h_ms : MeasurableSet s
⊢ (∫⁻ (a : α), indicator s (fun x => c) a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * indicator s fun x => c) a ∂μ
simp [*, mul_comm _ c, ← indicator_mul_right]
case h_add
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝¹ : Disjoint (support g) (support h)
h_mea_g : Measurable g
a✝ : Measurable h
h_ind_g : (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
h_ind_h : (∫⁻ (a : α), h a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * h) a ∂μ
⊢ (∫⁻ (a : α), (g + h) a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * (g + h)) a ∂μ
case h_add
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (support f_1) (support g) →
      Measurable f_1 →
        Measurable g →
          ((∫⁻ (a : α), f_1 a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * f_1) a ∂μ) →
            ((∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ) →
              (∫⁻ (a : α), (f_1 + g) a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ
intro g h _ h_mea_g _ h_ind_g h_ind_h
no goals
case h_add
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝¹ : Disjoint (support g) (support h)
h_mea_g : Measurable g
a✝ : Measurable h
h_ind_g : (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
h_ind_h : (∫⁻ (a : α), h a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * h) a ∂μ
⊢ (∫⁻ (a : α), (g + h) a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * (g + h)) a ∂μ
simp [mul_add, *, Measurable.mul]
case h_iSup
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), (∫⁻ (a : α), g n a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g n) a ∂μ
⊢ (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), g n x) a ∂Measure.withDensity μ f) =
    ∫⁻ (a : α), (f * fun x => ⨆ (n : ℕ), g n x) a ∂μ
case h_iSup
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), (∫⁻ (a : α), f_1 n a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), f_1 n x) a ∂Measure.withDensity μ f) =
            ∫⁻ (a : α), (f * fun x => ⨆ (n : ℕ), f_1 n x) a ∂μ
intro g h_mea_g h_mono_g h_ind
case h_iSup
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), (∫⁻ (a : α), g n a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g n) a ∂μ
this : Monotone fun n a => f a * g n a
⊢ (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), g n x) a ∂Measure.withDensity μ f) =
    ∫⁻ (a : α), (f * fun x => ⨆ (n : ℕ), g n x) a ∂μ
case h_iSup
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), (∫⁻ (a : α), g n a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g n) a ∂μ
⊢ (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), g n x) a ∂Measure.withDensity μ f) =
    ∫⁻ (a : α), (f * fun x => ⨆ (n : ℕ), g n x) a ∂μ
have : Monotone fun n a => f a * g n a := fun m n hmn x => mul_le_mul_left' (h_mono_g hmn x) _
no goals
case h_iSup
α : Type u_1
β : Type ?u.1781918
γ : Type ?u.1781921
δ : Type ?u.1781924
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), (∫⁻ (a : α), g n a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g n) a ∂μ
this : Monotone fun n a => f a * g n a
⊢ (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), g n x) a ∂Measure.withDensity μ f) =
    ∫⁻ (a : α), (f * fun x => ⨆ (n : ℕ), g n x) a ∂μ
simp [lintegral_iSup, ENNReal.mul_iSup, h_mf.mul (h_mea_g _), *]