α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
ex_G : ∃ G, Measurable G ∧ 0 ≤ G ∧ g =ᵐ[Measure.restrict volume (Ioi 0)] G
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
have ex_G : ∃ G : ℝ → ℝ, Measurable G ∧ 0 ≤ G ∧ g =ᵐ[volume.restrict (Ioi 0)] G := by
  refine' AEMeasurable.exists_measurable_nonneg _ g_nn
  exact aemeasurable_Ioi_of_forall_Ioc fun t ht => (g_intble t ht).1.1.aemeasurable
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
ex_G : ∃ G, Measurable G ∧ 0 ≤ G ∧ g =ᵐ[Measure.restrict volume (Ioi 0)] G
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
rcases ex_G with ⟨G, G_mble, G_nn, g_eq_G⟩
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
have g_eq_G_on : ∀ t, g =ᵐ[volume.restrict (Ioc 0 t)] G := fun t =>
  ae_mono (Measure.restrict_mono Ioc_subset_Ioi_self le_rfl) g_eq_G
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
have G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t := by
  refine' fun t t_pos => ⟨(g_intble t t_pos).1.congr_fun_ae (g_eq_G_on t), _⟩
  rw [Ioc_eq_empty_of_le t_pos.lt.le]
  exact integrableOn_empty
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
have eq₁ :
  (∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (G t) := by
  apply lintegral_congr_ae
  filter_upwards [g_eq_G] with a ha
  rw [ha]
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
eq₂ : ∀ (ω : α), (∫ (t : ℝ) in 0 ..f ω, g t) = ∫ (t : ℝ) in 0 ..f ω, G t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
have eq₂ : ∀ ω, (∫ t in (0)..f ω, g t) = ∫ t in (0)..f ω, G t := by
  refine' fun ω => intervalIntegral.integral_congr_ae _
  have fω_nn : 0 ≤ f ω := f_nn ω
  rw [uIoc_of_le fω_nn, ←
    ae_restrict_iff' (measurableSet_Ioc : MeasurableSet (Ioc (0 : ℝ) (f ω)))]
  exact g_eq_G_on (f ω)
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
eq₂ : ∀ (ω : α), (∫ (t : ℝ) in 0 ..f ω, g t) = ∫ (t : ℝ) in 0 ..f ω, G t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, G t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
eq₂ : ∀ (ω : α), (∫ (t : ℝ) in 0 ..f ω, g t) = ∫ (t : ℝ) in 0 ..f ω, G t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
simp_rw [eq₁, eq₂]
no goals
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
eq₂ : ∀ (ω : α), (∫ (t : ℝ) in 0 ..f ω, g t) = ∫ (t : ℝ) in 0 ..f ω, G t
⊢ (∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, G t) ∂μ) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
exact
  lintegral_comp_eq_lintegral_meas_le_mul_of_measurable μ f_nn f_mble G_intble G_mble
    fun t _ => G_nn t
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ AEMeasurable g
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ ∃ G, Measurable G ∧ 0 ≤ G ∧ g =ᵐ[Measure.restrict volume (Ioi 0)] G
refine' AEMeasurable.exists_measurable_nonneg _ g_nn
no goals
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ AEMeasurable g
exact aemeasurable_Ioi_of_forall_Ioc fun t ht => (g_intble t ht).1.1.aemeasurable
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
t : ℝ
t_pos : t > 0
⊢ IntegrableOn G (Ioc t 0)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
⊢ ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
refine' fun t t_pos => ⟨(g_intble t t_pos).1.congr_fun_ae (g_eq_G_on t), _⟩
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
t : ℝ
t_pos : t > 0
⊢ IntegrableOn G ∅
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
t : ℝ
t_pos : t > 0
⊢ IntegrableOn G (Ioc t 0)
rw [Ioc_eq_empty_of_le t_pos.lt.le]
no goals
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
t : ℝ
t_pos : t > 0
⊢ IntegrableOn G ∅
exact integrableOn_empty
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
⊢ (fun a => ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a)) =ᵐ[Measure.restrict volume (Ioi 0)] fun a =>
    ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (G a)
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
⊢ (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
apply lintegral_congr_ae
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
a : ℝ
ha : g a = G a
⊢ ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a) = ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (G a)
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
⊢ (fun a => ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a)) =ᵐ[Measure.restrict volume (Ioi 0)] fun a =>
    ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (G a)
filter_upwards [g_eq_G] with a ha
no goals
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
a : ℝ
ha : g a = G a
⊢ ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (g a) = ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (G a)
rw [ha]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
ω : α
⊢ ∀ᵐ (x : ℝ), x ∈ Ι 0 (f ω) → g x = G x
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
⊢ ∀ (ω : α), (∫ (t : ℝ) in 0 ..f ω, g t) = ∫ (t : ℝ) in 0 ..f ω, G t
refine' fun ω => intervalIntegral.integral_congr_ae _
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
ω : α
fω_nn : 0 ≤ f ω
⊢ ∀ᵐ (x : ℝ), x ∈ Ι 0 (f ω) → g x = G x
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
ω : α
⊢ ∀ᵐ (x : ℝ), x ∈ Ι 0 (f ω) → g x = G x
have fω_nn : 0 ≤ f ω := f_nn ω
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
ω : α
fω_nn : 0 ≤ f ω
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc 0 (f ω)), g x = G x
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
ω : α
fω_nn : 0 ≤ f ω
⊢ ∀ᵐ (x : ℝ), x ∈ Ι 0 (f ω) → g x = G x
rw [uIoc_of_le fω_nn, ←
  ae_restrict_iff' (measurableSet_Ioc : MeasurableSet (Ioc (0 : ℝ) (f ω)))]
no goals
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[Measure.restrict volume (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[Measure.restrict volume (Ioc 0 t)] G
G_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable G volume 0 t
eq₁ :
  (∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (G t)
ω : α
fω_nn : 0 ≤ f ω
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc 0 (f ω)), g x = G x
exact g_eq_G_on (f ω)