[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
[PROOFSTEP]
have g_intble' : ∀ t : ℝ, 0 ≤ t → IntervalIntegrable g volume 0 t :=
  by
  intro t ht
  cases' eq_or_lt_of_le ht with h h
  · simp [← h]
  · exact g_intble t h
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
⊢ ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
[PROOFSTEP]
intro t ht
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
t : ℝ
ht : 0 ≤ t
⊢ IntervalIntegrable g volume 0 t
[PROOFSTEP]
cases' eq_or_lt_of_le ht with h h
[GOAL]
case inl
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
t : ℝ
ht : 0 ≤ t
h : 0 = t
⊢ IntervalIntegrable g volume 0 t
[PROOFSTEP]
simp [← h]
[GOAL]
case inr
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
t : ℝ
ht : 0 ≤ t
h : 0 < t
⊢ IntervalIntegrable g volume 0 t
[PROOFSTEP]
exact g_intble t h
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → 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)
[PROOFSTEP]
have integrand_eq : ∀ ω, ENNReal.ofReal (∫ t in (0)..f ω, g t) = ∫⁻ t in Ioc 0 (f ω), ENNReal.ofReal (g t) :=
  by
  intro ω
  have g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g := by
    filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))] with x hx using g_nn x hx.1
  rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]
  congr
  exact intervalIntegral.integral_of_le (f_nn ω)
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
⊢ ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
[PROOFSTEP]
intro ω
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
[PROOFSTEP]
have g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g := by
  filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))] with x hx using g_nn x hx.1
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
⊢ 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
[PROOFSTEP]
filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))] with x hx using g_nn x hx.1
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
[PROOFSTEP]
rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ENNReal.ofReal (∫ (x : ℝ) in Ioc 0 (f ω), g x)
[PROOFSTEP]
congr
[GOAL]
case e_r
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[Measure.restrict volume (Ioc 0 (f ω))] g
⊢ ∫ (t : ℝ) in 0 ..f ω, g t = ∫ (x : ℝ) in Ioc 0 (f ω), g x
[PROOFSTEP]
exact intervalIntegral.integral_of_le (f_nn ω)
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
[PROOFSTEP]
simp_rw [integrand_eq, ← lintegral_indicator (fun t => ENNReal.ofReal (g t)) measurableSet_Ioc]
  -- Porting note: was part of `simp_rw` on the previous line, but didn't trigger.
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ∫⁻ (a : ℝ), indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
[PROOFSTEP]
rw [← lintegral_indicator _ measurableSet_Ioi]
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ∫⁻ (a : ℝ), indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a ∂μ =
    ∫⁻ (a : ℝ), indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a
[PROOFSTEP]
rw [lintegral_lintegral_swap]
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (y : ℝ), ∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y ∂μ =
    ∫⁻ (a : ℝ), indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a
[PROOFSTEP]
apply congr_arg
[GOAL]
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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (fun y => ∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y ∂μ) = fun a =>
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a
[PROOFSTEP]
funext s
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
⊢ ∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s ∂μ =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
[PROOFSTEP]
have aux₁ :
  (fun x => (Ioc 0 (f x)).indicator (fun t : ℝ => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * (Ioi (0 : ℝ)).indicator (fun _ => 1) s * (Ici s).indicator (fun _ : ℝ => (1 : ℝ≥0∞)) (f x) :=
  by
  funext a
  by_cases s ∈ Ioc (0 : ℝ) (f a)
  · simp only [h, show s ∈ Ioi (0 : ℝ) from h.1, show f a ∈ Ici s from h.2, indicator_of_mem, mul_one]
  · have h_copy := h
    simp only [mem_Ioc, not_and, not_le] at h
    by_cases h' : 0 < s
    · simp only [h_copy, h h', indicator_of_not_mem, not_false_iff, mem_Ici, not_le, mul_zero]
    · have : s ∉ Ioi (0 : ℝ) := h'
      simp only [this, h', indicator_of_not_mem, not_false_iff, mul_zero, zero_mul, mem_Ioc, false_and_iff]
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
⊢ (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
[PROOFSTEP]
funext a
[GOAL]
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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
[PROOFSTEP]
by_cases s ∈ Ioc (0 : ℝ) (f a)
[GOAL]
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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
[PROOFSTEP]
by_cases s ∈ Ioc (0 : ℝ) (f a)
[GOAL]
case pos
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h : s ∈ Ioc 0 (f a)
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
[PROOFSTEP]
simp only [h, show s ∈ Ioi (0 : ℝ) from h.1, show f a ∈ Ici s from h.2, indicator_of_mem, mul_one]
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h : ¬s ∈ Ioc 0 (f a)
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
[PROOFSTEP]
have h_copy := h
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h h_copy : ¬s ∈ Ioc 0 (f a)
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
[PROOFSTEP]
simp only [mem_Ioc, not_and, not_le] at h
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
[PROOFSTEP]
by_cases h' : 0 < s
[GOAL]
case pos
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
h' : 0 < s
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
[PROOFSTEP]
simp only [h_copy, h h', indicator_of_not_mem, not_false_iff, mem_Ici, not_le, mul_zero]
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
[PROOFSTEP]
have : s ∉ Ioi (0 : ℝ) := h'
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : ¬s ∈ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
this : ¬s ∈ Ioi 0
⊢ indicator (Ioc 0 (f a)) (fun t => ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f a)
[PROOFSTEP]
simp only [this, h', indicator_of_not_mem, not_false_iff, mul_zero, zero_mul, mem_Ioc, false_and_iff]
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ∫⁻ (x : α), indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s ∂μ =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
[PROOFSTEP]
simp_rw [aux₁]
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ∫⁻ (x : α), ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x) ∂μ =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
[PROOFSTEP]
rw [lintegral_const_mul']
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α), indicator (Ici s) (fun x => 1) (f a) ∂μ =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
case h.h.hr
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s ≠ ⊤
[PROOFSTEP]
swap
[GOAL]
case h.h.hr
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s ≠ ⊤
[PROOFSTEP]
apply ENNReal.mul_ne_top ENNReal.ofReal_ne_top
[GOAL]
case h.h.hr
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ indicator (Ioi 0) (fun x => 1) s ≠ ⊤
[PROOFSTEP]
by_cases h : (0 : ℝ) < s
[GOAL]
case pos
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
h : 0 < s
⊢ indicator (Ioi 0) (fun x => 1) s ≠ ⊤
[PROOFSTEP]
simp [indicator_apply, h]
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
h : ¬0 < s
⊢ indicator (Ioi 0) (fun x => 1) s ≠ ⊤
[PROOFSTEP]
simp [indicator_apply, h]
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α), indicator (Ici s) (fun x => 1) (f a) ∂μ =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
[PROOFSTEP]
simp_rw [show
    (fun a => (Ici s).indicator (fun _ : ℝ => (1 : ℝ≥0∞)) (f a)) = fun a => {a : α | s ≤ f a}.indicator (fun _ => 1) a
    by funext a; by_cases s ≤ f a <;> simp [h]]
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ (fun a => indicator (Ici s) (fun x => 1) (f a)) = fun a => indicator {a | s ≤ f a} (fun x => 1) a
[PROOFSTEP]
funext a
[GOAL]
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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
a : α
⊢ indicator (Ici s) (fun x => 1) (f a) = indicator {a | s ≤ f a} (fun x => 1) a
[PROOFSTEP]
by_cases s ≤ f a
[GOAL]
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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
a : α
⊢ indicator (Ici s) (fun x => 1) (f a) = indicator {a | s ≤ f a} (fun x => 1) a
[PROOFSTEP]
by_cases s ≤ f a
[GOAL]
case pos
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
a : α
h : s ≤ f a
⊢ indicator (Ici s) (fun x => 1) (f a) = indicator {a | s ≤ f a} (fun x => 1) a
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
a : α
h : ¬s ≤ f a
⊢ indicator (Ici s) (fun x => 1) (f a) = indicator {a | s ≤ f a} (fun x => 1) a
[PROOFSTEP]
simp [h]
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α), indicator {a | s ≤ f a} (fun x => 1) a ∂μ =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
[PROOFSTEP]
rw [lintegral_indicator]
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α) in {a | s ≤ f a}, 1 ∂μ =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
case h.h.hs
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ MeasurableSet {a | s ≤ f a}
[PROOFSTEP]
swap
[GOAL]
case h.h.hs
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ MeasurableSet {a | s ≤ f a}
[PROOFSTEP]
exact f_mble measurableSet_Ici
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * ∫⁻ (a : α) in {a | s ≤ f a}, 1 ∂μ =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
[PROOFSTEP]
rw [lintegral_one, Measure.restrict_apply MeasurableSet.univ, univ_inter, indicator_mul_left, mul_assoc,
  show
    (Ioi 0).indicator (fun _x : ℝ => (1 : ℝ≥0∞)) s * μ {a : α | s ≤ f a} =
      (Ioi 0).indicator (fun _x : ℝ => 1 * μ {a : α | s ≤ f a}) s
    by by_cases 0 < s <;> simp [h]]
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ indicator (Ioi 0) (fun _x => 1) s * ↑↑μ {a | s ≤ f a} = indicator (Ioi 0) (fun _x => 1 * ↑↑μ {a | s ≤ f a}) s
[PROOFSTEP]
by_cases 0 < s
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ indicator (Ioi 0) (fun _x => 1) s * ↑↑μ {a | s ≤ f a} = indicator (Ioi 0) (fun _x => 1 * ↑↑μ {a | s ≤ f a}) s
[PROOFSTEP]
by_cases 0 < s
[GOAL]
case pos
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
h : 0 < s
⊢ indicator (Ioi 0) (fun _x => 1) s * ↑↑μ {a | s ≤ f a} = indicator (Ioi 0) (fun _x => 1 * ↑↑μ {a | s ≤ f a}) s
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
h : ¬0 < s
⊢ indicator (Ioi 0) (fun _x => 1) s * ↑↑μ {a | s ≤ f a} = indicator (Ioi 0) (fun _x => 1 * ↑↑μ {a | s ≤ f a}) s
[PROOFSTEP]
simp [h]
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun _x => 1 * ↑↑μ {a | s ≤ f a}) s =
    indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a}) s * ENNReal.ofReal (g s)
[PROOFSTEP]
simp_rw [mul_comm _ (ENNReal.ofReal _), one_mul]
[GOAL]
case h.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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) s) = fun x =>
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun x => 1) s * indicator (Ici s) (fun x => 1) (f x)
⊢ ENNReal.ofReal (g s) * indicator (Ioi 0) (fun _x => ↑↑μ {a | s ≤ f a}) s =
    ENNReal.ofReal (g s) * indicator (Ioi 0) (fun t => ↑↑μ {a | t ≤ f a}) s
[PROOFSTEP]
rfl
[GOAL]
case hf
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ AEMeasurable (Function.uncurry fun ω a => indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a)
[PROOFSTEP]
have aux₂ :
  (Function.uncurry fun (x : α) (y : ℝ) => (Ioc 0 (f x)).indicator (fun t : ℝ => ENNReal.ofReal (g t)) y) =
    {p : α × ℝ | p.2 ∈ Ioc 0 (f p.1)}.indicator fun p => ENNReal.ofReal (g p.2) :=
  by
  funext p
  cases p with
  | mk p_fst p_snd => ?_
  rw [Function.uncurry_apply_pair]
  by_cases p_snd ∈ Ioc 0 (f p_fst)
  · have h' : (p_fst, p_snd) ∈ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h
    rw [Set.indicator_of_mem h', Set.indicator_of_mem h]
  · have h' : (p_fst, p_snd) ∉ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h
    rw [Set.indicator_of_not_mem h', Set.indicator_of_not_mem h]
[GOAL]
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
[PROOFSTEP]
funext p
[GOAL]
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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p : α × ℝ
⊢ Function.uncurry (fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) p =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) p
[PROOFSTEP]
cases p with
| mk p_fst p_snd => ?_
[GOAL]
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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p : α × ℝ
⊢ Function.uncurry (fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) p =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) p
[PROOFSTEP]
cases p with
| mk p_fst p_snd => ?_
[GOAL]
case h.mk
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
⊢ Function.uncurry (fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) (p_fst, p_snd) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
[PROOFSTEP]
rw [Function.uncurry_apply_pair]
[GOAL]
case h.mk
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
[PROOFSTEP]
by_cases p_snd ∈ Ioc 0 (f p_fst)
[GOAL]
case h.mk
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
[PROOFSTEP]
by_cases p_snd ∈ Ioc 0 (f p_fst)
[GOAL]
case pos
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
[PROOFSTEP]
have h' : (p_fst, p_snd) ∈ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h
[GOAL]
case pos
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : p_snd ∈ Ioc 0 (f p_fst)
h' : (p_fst, p_snd) ∈ {p | p.snd ∈ Ioc 0 (f p.fst)}
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
[PROOFSTEP]
rw [Set.indicator_of_mem h', Set.indicator_of_mem h]
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : ¬p_snd ∈ Ioc 0 (f p_fst)
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
[PROOFSTEP]
have h' : (p_fst, p_snd) ∉ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h
[GOAL]
case neg
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : ¬p_snd ∈ Ioc 0 (f p_fst)
h' : ¬(p_fst, p_snd) ∈ {p | p.snd ∈ Ioc 0 (f p.fst)}
⊢ indicator (Ioc 0 (f p_fst)) (fun t => ENNReal.ofReal (g t)) p_snd =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} (fun p => ENNReal.ofReal (g p.snd)) (p_fst, p_snd)
[PROOFSTEP]
rw [Set.indicator_of_not_mem h', Set.indicator_of_not_mem h]
[GOAL]
case hf
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
⊢ AEMeasurable (Function.uncurry fun ω a => indicator (Ioc 0 (f ω)) (fun t => ENNReal.ofReal (g t)) a)
[PROOFSTEP]
rw [aux₂]
[GOAL]
case hf
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
⊢ AEMeasurable (indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd))
[PROOFSTEP]
have mble := measurableSet_region_between_oc measurable_zero f_mble MeasurableSet.univ
[GOAL]
case hf
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
mble : MeasurableSet {p | p.fst ∈ univ ∧ p.snd ∈ Ioc (OfNat.ofNat 0 p.fst) (f p.fst)}
⊢ AEMeasurable (indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd))
[PROOFSTEP]
simp_rw [mem_univ, Pi.zero_apply, true_and_iff] at mble
[GOAL]
case hf
α : 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_mble : Measurable g
g_nn : ∀ (t : ℝ), t > 0 → 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
aux₂ :
  (Function.uncurry fun x y => indicator (Ioc 0 (f x)) (fun t => ENNReal.ofReal (g t)) y) =
    indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd)
mble : MeasurableSet {p | p.snd ∈ Ioc 0 (f p.fst)}
⊢ AEMeasurable (indicator {p | p.snd ∈ Ioc 0 (f p.fst)} fun p => ENNReal.ofReal (g p.snd))
[PROOFSTEP]
exact (ENNReal.measurable_ofReal.comp (g_mble.comp measurable_snd)).aemeasurable.indicator mble
[GOAL]
α : 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)
[PROOFSTEP]
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
[GOAL]
α : 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
[PROOFSTEP]
refine' AEMeasurable.exists_measurable_nonneg _ g_nn
[GOAL]
α : 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
[PROOFSTEP]
exact aemeasurable_Ioi_of_forall_Ioc fun t ht => (g_intble t ht).1.1.aemeasurable
[GOAL]
α : 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)
[PROOFSTEP]
rcases ex_G with ⟨G, G_mble, G_nn, g_eq_G⟩
[GOAL]
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)
[PROOFSTEP]
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
[GOAL]
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)
[PROOFSTEP]
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
[GOAL]
α : 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
[PROOFSTEP]
refine' fun t t_pos => ⟨(g_intble t t_pos).1.congr_fun_ae (g_eq_G_on t), _⟩
[GOAL]
α : 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)
[PROOFSTEP]
rw [Ioc_eq_empty_of_le t_pos.lt.le]
[GOAL]
α : 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 ∅
[PROOFSTEP]
exact integrableOn_empty
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
α : 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)
[PROOFSTEP]
apply lintegral_congr_ae
[GOAL]
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)
[PROOFSTEP]
filter_upwards [g_eq_G] with a ha
[GOAL]
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)
[PROOFSTEP]
rw [ha]
[GOAL]
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)
[PROOFSTEP]
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 ω)
[GOAL]
α : 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
[PROOFSTEP]
refine' fun ω => intervalIntegral.integral_congr_ae _
[GOAL]
α : 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
[PROOFSTEP]
have fω_nn : 0 ≤ f ω := f_nn ω
[GOAL]
α : 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
[PROOFSTEP]
rw [uIoc_of_le fω_nn, ← ae_restrict_iff' (measurableSet_Ioc : MeasurableSet (Ioc (0 : ℝ) (f ω)))]
[GOAL]
α : 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
[PROOFSTEP]
exact g_eq_G_on (f ω)
[GOAL]
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)
[PROOFSTEP]
simp_rw [eq₁, eq₂]
[GOAL]
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)
[PROOFSTEP]
exact lintegral_comp_eq_lintegral_meas_le_mul_of_measurable μ f_nn f_mble G_intble G_mble fun t _ => G_nn t
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
[PROOFSTEP]
set cst := fun _ : ℝ => (1 : ℝ)
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun x => 1
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
[PROOFSTEP]
have cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t := fun _ _ => intervalIntegrable_const
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun x => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
[PROOFSTEP]
have key := lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble cst_intble (eventually_of_forall fun _ => zero_le_one)
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun x => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, cst t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (cst t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
[PROOFSTEP]
simp_rw [ENNReal.ofReal_one, mul_one] at key
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun x => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
[PROOFSTEP]
rw [← key]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun x => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ
[PROOFSTEP]
congr with ω
[GOAL]
case e_f.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
cst : ℝ → ℝ := fun x => 1
cst_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable cst volume 0 t
key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a}
ω : α
⊢ ENNReal.ofReal (f ω) = ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1)
[PROOFSTEP]
simp only [intervalIntegral.integral_const, sub_zero, Algebra.id.smul_eq_mul, mul_one]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
have one_lt_p : -1 < p - 1 := by linarith
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
⊢ -1 < p - 1
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
have obs : ∀ x : ℝ, (∫ t : ℝ in (0)..x, t ^ (p - 1)) = x ^ p / p :=
  by
  intro x
  rw [integral_rpow (Or.inl one_lt_p)]
  simp [Real.zero_rpow p_pos.ne.symm]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
⊢ ∀ (x : ℝ), ∫ (t : ℝ) in 0 ..x, t ^ (p - 1) = x ^ p / p
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
x : ℝ
⊢ ∫ (t : ℝ) in 0 ..x, t ^ (p - 1) = x ^ p / p
[PROOFSTEP]
rw [integral_rpow (Or.inl one_lt_p)]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
x : ℝ
⊢ (x ^ (p - 1 + 1) - 0 ^ (p - 1 + 1)) / (p - 1 + 1) = x ^ p / p
[PROOFSTEP]
simp [Real.zero_rpow p_pos.ne.symm]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
obs : ∀ (x : ℝ), ∫ (t : ℝ) in 0 ..x, t ^ (p - 1) = x ^ p / p
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
set g := fun t : ℝ => t ^ (p - 1)
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
have g_nn : ∀ᵐ t ∂volume.restrict (Ioi (0 : ℝ)), 0 ≤ g t :=
  by
  filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]
  intro t t_pos
  exact Real.rpow_nonneg_of_nonneg (mem_Ioi.mp t_pos).le (p - 1)
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
[PROOFSTEP]
filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]
[GOAL]
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ (a : ℝ), a ∈ Ioi 0 → 0 ≤ a ^ (p - 1)
[PROOFSTEP]
intro t t_pos
[GOAL]
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
t : ℝ
t_pos : t ∈ Ioi 0
⊢ 0 ≤ t ^ (p - 1)
[PROOFSTEP]
exact Real.rpow_nonneg_of_nonneg (mem_Ioi.mp t_pos).le (p - 1)
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
have g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t := fun _ _ =>
  intervalIntegral.intervalIntegrable_rpow' one_lt_p
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
have key := lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
rw [← key, ← lintegral_const_mul (ENNReal.ofReal p)]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (∫ (t : ℝ) in 0 ..f a, g t) ∂μ
[PROOFSTEP]
simp_rw [obs]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ Measurable fun ω => ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t)
[PROOFSTEP]
simp_rw [obs]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ
[PROOFSTEP]
congr with ω
[GOAL]
case e_f.h
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
ω : α
⊢ ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal p * ENNReal.ofReal (f ω ^ p / p)
[PROOFSTEP]
rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel' (f ω ^ p) p_pos.ne.symm]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g✝ : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t => t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), t > 0 → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ Measurable fun ω => ENNReal.ofReal (f ω ^ p / p)
[PROOFSTEP]
exact ((f_mble.pow measurable_const).div_const p).ennreal_ofReal
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
⊢ 0 < ↑↑μ {a | g a = t}
[PROOFSTEP]
have uni : {a : α | t ≤ g a} = {a : α | t < g a} ∪ {a : α | t = g a} :=
  by
  ext a
  simp only [mem_setOf, mem_union]
  apply le_iff_lt_or_eq
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
⊢ {a | t ≤ g a} = {a | t < g a} ∪ {a | t = g a}
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
a : α
⊢ a ∈ {a | t ≤ g a} ↔ a ∈ {a | t < g a} ∪ {a | t = g a}
[PROOFSTEP]
simp only [mem_setOf, mem_union]
[GOAL]
case h
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
a : α
⊢ t ≤ g a ↔ t < g a ∨ t = g a
[PROOFSTEP]
apply le_iff_lt_or_eq
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | t = g a}
⊢ 0 < ↑↑μ {a | g a = t}
[PROOFSTEP]
rw [show {a : α | t = g a} = {a : α | g a = t} by simp_rw [eq_comm]] at uni
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | t = g a}
⊢ {a | t = g a} = {a | g a = t}
[PROOFSTEP]
simp_rw [eq_comm]
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
⊢ 0 < ↑↑μ {a | g a = t}
[PROOFSTEP]
have disj : {a : α | t < g a} ∩ {a : α | g a = t} = ∅ := by
  ext a
  simp only [mem_inter_iff, mem_setOf, mem_empty_iff_false, iff_false_iff, not_and]
  exact ne_of_gt
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
⊢ {a | t < g a} ∩ {a | g a = t} = ∅
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
a : α
⊢ a ∈ {a | t < g a} ∩ {a | g a = t} ↔ a ∈ ∅
[PROOFSTEP]
simp only [mem_inter_iff, mem_setOf, mem_empty_iff_false, iff_false_iff, not_and]
[GOAL]
case h
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
a : α
⊢ t < g a → ¬g a = t
[PROOFSTEP]
exact ne_of_gt
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
⊢ 0 < ↑↑μ {a | g a = t}
[PROOFSTEP]
have μ_add : μ {a : α | t ≤ g a} = μ {a : α | t < g a} + μ {a : α | g a = t} := by
  rw [uni, measure_union (disjoint_iff_inter_eq_empty.mpr disj) (g_mble (Finite.measurableSet (finite_singleton t)))]
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
⊢ ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
[PROOFSTEP]
rw [uni, measure_union (disjoint_iff_inter_eq_empty.mpr disj) (g_mble (Finite.measurableSet (finite_singleton t)))]
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
⊢ 0 < ↑↑μ {a | g a = t}
[PROOFSTEP]
by_contra con
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
con : ¬0 < ↑↑μ {a | g a = t}
⊢ False
[PROOFSTEP]
rw [not_lt, nonpos_iff_eq_zero] at con
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
con : ↑↑μ {a | g a = t} = 0
⊢ False
[PROOFSTEP]
rw [con, add_zero] at μ_add
[GOAL]
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_3
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a}
con : ↑↑μ {a | g a = t} = 0
⊢ False
[PROOFSTEP]
exact ht μ_add
[GOAL]
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
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)
[PROOFSTEP]
rw [lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn]
[GOAL]
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
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
⊢ ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t < f a} * ENNReal.ofReal (g t)
[PROOFSTEP]
apply lintegral_congr_ae
[GOAL]
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
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
⊢ (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)
[PROOFSTEP]
filter_upwards [Measure.meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f_mble] with t ht
[GOAL]
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
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
t : ℝ
ht : ↑↑μ {a | t ≤ f a} = ↑↑μ {a | t < f a}
⊢ ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ↑↑μ {a | t < f a} * ENNReal.ofReal (g t)
[PROOFSTEP]
rw [ht]
[GOAL]
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t < f a}
[PROOFSTEP]
rw [lintegral_eq_lintegral_meas_le μ f_nn f_mble]
[GOAL]
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
⊢ ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} = ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t < f a}
[PROOFSTEP]
apply lintegral_congr_ae
[GOAL]
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
⊢ (fun a => ↑↑μ {a_1 | a ≤ f a_1}) =ᵐ[Measure.restrict volume (Ioi 0)] fun a => ↑↑μ {a_1 | a < f a_1}
[PROOFSTEP]
filter_upwards [Measure.meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f_mble] with t ht
[GOAL]
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
t : ℝ
ht : ↑↑μ {a | t ≤ f a} = ↑↑μ {a | t < f a}
⊢ ↑↑μ {a | t ≤ f a} = ↑↑μ {a | t < f a}
[PROOFSTEP]
rw [ht]
[GOAL]
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
rw [lintegral_rpow_eq_lintegral_meas_le_mul μ f_nn f_mble p_pos]
[GOAL]
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
⊢ ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
apply congr_arg fun z => ENNReal.ofReal p * z
[GOAL]
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
⊢ ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) =
    ∫⁻ (t : ℝ) in Ioi 0, ↑↑μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
apply lintegral_congr_ae
[GOAL]
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
⊢ (fun a => ↑↑μ {a_1 | a ≤ f a_1} * ENNReal.ofReal (a ^ (p - 1))) =ᵐ[Measure.restrict volume (Ioi 0)] fun a =>
    ↑↑μ {a_1 | a < f a_1} * ENNReal.ofReal (a ^ (p - 1))
[PROOFSTEP]
filter_upwards [Measure.meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f_mble] with t ht
[GOAL]
case h
α : Type u_1
inst✝³ : MeasurableSpace α
μ✝ : Measure α
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
f : α → ℝ
g : ℝ → ℝ
s : Set α
μ : Measure α
inst✝ : SigmaFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
p : ℝ
p_pos : 0 < p
t : ℝ
ht : ↑↑μ {a | t ≤ f a} = ↑↑μ {a | t < f a}
⊢ ↑↑μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) = ↑↑μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))
[PROOFSTEP]
rw [ht]


[GOAL]
a b : ℝ
h : 0 < b
⊢ IntegrableOn (fun x => exp (-b * x)) (Ioi a)
[PROOFSTEP]
have : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b)) :=
  by
  refine' Tendsto.div_const (Tendsto.neg _) _
  exact tendsto_exp_atBot.comp (tendsto_id.neg_const_mul_atTop (Right.neg_neg_iff.2 h))
[GOAL]
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
[PROOFSTEP]
refine' Tendsto.div_const (Tendsto.neg _) _
[GOAL]
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => exp (-b * x)) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_exp_atBot.comp (tendsto_id.neg_const_mul_atTop (Right.neg_neg_iff.2 h))
[GOAL]
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
⊢ IntegrableOn (fun x => exp (-b * x)) (Ioi a)
[PROOFSTEP]
refine' integrableOn_Ioi_deriv_of_nonneg' (fun x _ => _) (fun x _ => (exp_pos _).le) this
[GOAL]
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
x : ℝ
x✝ : x ∈ Ici a
⊢ HasDerivAt (fun x => -exp (-b * x) / b) (exp (-b * x)) x
[PROOFSTEP]
simpa [h.ne'] using ((hasDerivAt_id x).const_mul b).neg.exp.neg.div_const b
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
cases' h2.isBigOWith with c h3
[GOAL]
case intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c : ℝ
h3 : Asymptotics.IsBigOWith c atTop f fun x => exp (-b * x)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
rw [Asymptotics.isBigOWith_iff, eventually_atTop] at h3
[GOAL]
case intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c : ℝ
h3 : ∃ a, ∀ (b_1 : ℝ), b_1 ≥ a → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
cases' h3 with r bdr
[GOAL]
case intro.intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
let v := max a r
[GOAL]
case intro.intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
have int_left : IntegrableOn f (Ioc a v) :=
  by
  rw [← intervalIntegrable_iff_integrable_Ioc_of_le (le_max_left a r)]
  have u : Icc a v ⊆ Ici a := Icc_subset_Ici_self
  exact (h1.mono u).intervalIntegrable_of_Icc (le_max_left a r)
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
⊢ IntegrableOn f (Ioc a v)
[PROOFSTEP]
rw [← intervalIntegrable_iff_integrable_Ioc_of_le (le_max_left a r)]
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
⊢ IntervalIntegrable f volume a (max a r)
[PROOFSTEP]
have u : Icc a v ⊆ Ici a := Icc_subset_Ici_self
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
u : Icc a v ⊆ Ici a
⊢ IntervalIntegrable f volume a (max a r)
[PROOFSTEP]
exact (h1.mono u).intervalIntegrable_of_Icc (le_max_left a r)
[GOAL]
case intro.intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
suffices IntegrableOn f (Ioi v) by
  have t := integrableOn_union.mpr ⟨int_left, this⟩
  simpa only [Ioc_union_Ioi_eq_Ioi, le_max_iff, le_refl, true_or_iff] using t
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : IntegrableOn f (Ioi v)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
have t := integrableOn_union.mpr ⟨int_left, this⟩
[GOAL]
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : IntegrableOn f (Ioi v)
t : IntegrableOn f (Ioc a v ∪ Ioi v)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
simpa only [Ioc_union_Ioi_eq_Ioi, le_max_iff, le_refl, true_or_iff] using t
[GOAL]
case intro.intro
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
⊢ IntegrableOn f (Ioi v)
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.left
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
⊢ AEStronglyMeasurable f (Measure.restrict volume (Ioi v))
[PROOFSTEP]
exact (h1.mono <| Ioi_subset_Ici <| le_max_left a r).aestronglyMeasurable measurableSet_Ioi
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
⊢ HasFiniteIntegral f
[PROOFSTEP]
have : HasFiniteIntegral (fun x : ℝ => c * exp (-b * x)) (volume.restrict (Ioi v)) :=
  (exp_neg_integrableOn_Ioi v h0).hasFiniteIntegral.const_mul c
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
⊢ HasFiniteIntegral f
[PROOFSTEP]
apply this.mono
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi v), ‖f a‖ ≤ ‖c * exp (-b * a)‖
[PROOFSTEP]
refine' (ae_restrict_iff' measurableSet_Ioi).mpr _
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi v → ‖f x‖ ≤ ‖c * exp (-b * x)‖
[PROOFSTEP]
refine' ae_of_all _ fun x h1x => _
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
x : ℝ
h1x : x ∈ Ioi v
⊢ ‖f x‖ ≤ ‖c * exp (-b * x)‖
[PROOFSTEP]
rw [norm_mul, norm_eq_abs]
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
x : ℝ
h1x : x ∈ Ioi v
⊢ |f x| ≤ ‖c‖ * ‖exp (-b * x)‖
[PROOFSTEP]
rw [mem_Ioi] at h1x
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
bdr : ∀ (b_1 : ℝ), b_1 ≥ r → ‖f b_1‖ ≤ c * ‖exp (-b * b_1)‖
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
x : ℝ
h1x : v < x
⊢ |f x| ≤ ‖c‖ * ‖exp (-b * x)‖
[PROOFSTEP]
specialize bdr x ((le_max_right a r).trans h1x.le)
[GOAL]
case intro.intro.right
f : ℝ → ℝ
a b : ℝ
h0 : 0 < b
h1 : ContinuousOn f (Ici a)
h2 : f =O[atTop] fun x => exp (-b * x)
c r : ℝ
v : ℝ := max a r
int_left : IntegrableOn f (Ioc a v)
this : HasFiniteIntegral fun x => c * exp (-b * x)
x : ℝ
h1x : v < x
bdr : ‖f x‖ ≤ c * ‖exp (-b * x)‖
⊢ |f x| ≤ ‖c‖ * ‖exp (-b * x)‖
[PROOFSTEP]
exact bdr.trans (mul_le_mul_of_nonneg_right (le_abs_self c) (norm_nonneg _))