[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
s : Set α
φ : ι → Set α
hs : MeasurableSet s
ae_eventually_mem : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (n : ι) in l, x ∈ φ n
measurable : ∀ (n : ι), MeasurableSet (φ n)
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, ∀ᶠ (i : ι) in l, x ∈ φ i
[PROOFSTEP]
rwa [ae_restrict_iff' hs]
[GOAL]
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
⊢ AEMeasurable f
[PROOFSTEP]
obtain ⟨u, hu⟩ := l.exists_seq_tendsto
[GOAL]
case intro
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
u : ℕ → ι
hu : Tendsto u atTop l
⊢ AEMeasurable f
[PROOFSTEP]
have := aemeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)
[GOAL]
case intro
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f
⊢ AEMeasurable f
[PROOFSTEP]
rwa [Measure.restrict_eq_self_of_ae_mem] at this 
[GOAL]
case intro.hs
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEMeasurable f
u : ℕ → ι
hu : Tendsto u atTop l
this : AEMeasurable f
⊢ ∀ᵐ (x : α) ∂μ, x ∈ ⋃ (i : ℕ), φ (u i)
[PROOFSTEP]
filter_upwards [hφ.ae_eventually_mem] with x hx using mem_iUnion.mpr (hu.eventually hx).exists
[GOAL]
α : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (Measure.restrict μ (φ i))
⊢ AEStronglyMeasurable f μ
[PROOFSTEP]
obtain ⟨u, hu⟩ := l.exists_seq_tendsto
[GOAL]
case intro
α : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (Measure.restrict μ (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
⊢ AEStronglyMeasurable f μ
[PROOFSTEP]
have := aestronglyMeasurable_iUnion_iff.mpr fun n : ℕ => hfm (u n)
[GOAL]
case intro
α : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (Measure.restrict μ (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEStronglyMeasurable f (Measure.restrict μ (⋃ (i : ℕ), φ (u i)))
⊢ AEStronglyMeasurable f μ
[PROOFSTEP]
rwa [Measure.restrict_eq_self_of_ae_mem] at this 
[GOAL]
case intro.hs
α : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
f : α → β
φ : ι → Set α
hφ : AECover μ l φ
hfm : ∀ (i : ι), AEStronglyMeasurable f (Measure.restrict μ (φ i))
u : ℕ → ι
hu : Tendsto u atTop l
this : AEStronglyMeasurable f (Measure.restrict μ (⋃ (i : ℕ), φ (u i)))
⊢ ∀ᵐ (x : α) ∂μ, x ∈ ⋃ (i : ℕ), φ (u i)
[PROOFSTEP]
filter_upwards [hφ.ae_eventually_mem] with x hx using mem_iUnion.mpr (hu.eventually hx).exists
[GOAL]
α : Type u_1
ι : Type u_2
inst✝² : Countable ι
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : Preorder ι
φ : ι → Set α
hφ : AECover μ atTop φ
x : α
h : ∀ᶠ (i : ι) in atTop, x ∈ φ i
⊢ ∀ᶠ (i : ι) in atTop, x ∈ ⋂ (k : ι) (_ : k ∈ Ici i), φ k
[PROOFSTEP]
simpa only [mem_iInter, mem_Ici, eventually_forall_ge_atTop]
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
⊢ Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
[PROOFSTEP]
have lim₁ :=
  lintegral_tendsto_of_monotone_of_nat hφ.biInter_Ici_aecover
    (fun i j hij => biInter_subset_biInter_left (Ici_subset_Ici.mpr hij)) hfm
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
[PROOFSTEP]
have lim₂ :=
  lintegral_tendsto_of_monotone_of_nat hφ.biUnion_Iic_aecover
    (fun i j hij => biUnion_subset_biUnion_left (Iic_subset_Iic.mpr hij)) hfm
[GOAL]
α : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
[PROOFSTEP]
refine tendsto_of_tendsto_of_tendsto_of_le_of_le lim₁ lim₂ (fun n ↦ ?_) fun n ↦ ?_
[GOAL]
case refine_1
α : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
n : ℕ
⊢ ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici n), φ k, f x ∂μ ≤ ∫⁻ (x : α) in φ n, f x ∂μ
case refine_2
α : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
n : ℕ
⊢ ∫⁻ (x : α) in φ n, f x ∂μ ≤ ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic n), φ k, f x ∂μ
[PROOFSTEP]
exacts [lintegral_mono_set (biInter_subset_of_mem left_mem_Ici),
  lintegral_mono_set (subset_biUnion_of_mem right_mem_Iic)]
[GOAL]
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
⊢ ⨆ (i : ι), ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ
[PROOFSTEP]
have := hφ.lintegral_tendsto_of_countably_generated hfm
[GOAL]
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ ⨆ (i : ι), ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ
[PROOFSTEP]
refine'
  ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun i => lintegral_mono' Measure.restrict_le_self le_rfl) fun w hw => _
[GOAL]
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
[PROOFSTEP]
rcases exists_between hw with ⟨m, hm₁, hm₂⟩
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
m : ℝ≥0∞
hm₁ : w < m
hm₂ : m < ∫⁻ (x : α), f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
[PROOFSTEP]
rcases(eventually_ge_of_tendsto_gt hm₂ this).exists with ⟨i, hi⟩
[GOAL]
case intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
m : ℝ≥0∞
hm₁ : w < m
hm₂ : m < ∫⁻ (x : α), f x ∂μ
i : ι
hi : m ≤ ∫⁻ (x : α) in φ i, f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
[PROOFSTEP]
exact ⟨i, lt_of_lt_of_le hm₁ hi⟩
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
⊢ Integrable f
[PROOFSTEP]
refine' ⟨hfm, (le_of_tendsto _ hbounded).trans_lt ENNReal.ofReal_lt_top⟩
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
⊢ Tendsto (fun c => ∫⁻ (x : α) in φ c, ↑‖f x‖₊ ∂μ) l (𝓝 (∫⁻ (a : α), ↑‖f a‖₊ ∂μ))
[PROOFSTEP]
exact hφ.lintegral_tendsto_of_countably_generated hfm.ennnorm
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ Integrable f
[PROOFSTEP]
refine' hφ.integrable_of_lintegral_nnnorm_bounded (max 1 (I + 1)) hfm _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal (max 1 (I + 1))
[PROOFSTEP]
refine' htendsto.eventually (ge_mem_nhds _)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ ENNReal.ofReal I < ENNReal.ofReal (max 1 (I + 1))
[PROOFSTEP]
refine' (ENNReal.ofReal_lt_ofReal_iff (lt_max_of_lt_left zero_lt_one)).2 _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ I < max 1 (I + 1)
[PROOFSTEP]
exact lt_max_of_lt_right (lt_add_one I)
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ≥0
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ↑I
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal ↑I
[PROOFSTEP]
simpa only [ENNReal.ofReal_coe_nnreal] using hbounded
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ≥0
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 ↑I)
⊢ Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal ↑I))
[PROOFSTEP]
simpa only [ENNReal.ofReal_coe_nnreal] using htendsto
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
⊢ Integrable f
[PROOFSTEP]
have hfm : AEStronglyMeasurable f μ := hφ.aestronglyMeasurable fun i => (hfi i).aestronglyMeasurable
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
⊢ Integrable f
[PROOFSTEP]
refine' hφ.integrable_of_lintegral_nnnorm_bounded I hfm _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
[PROOFSTEP]
conv at hbounded in integral _ _ =>
  rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x)) hfm.norm.restrict]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
| ∫ (x : α) in φ i, ‖f x‖ ∂μ
[PROOFSTEP]
rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x)) hfm.norm.restrict]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
| ∫ (x : α) in φ i, ‖f x‖ ∂μ
[PROOFSTEP]
rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x)) hfm.norm.restrict]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
| ∫ (x : α) in φ i, ‖f x‖ ∂μ
[PROOFSTEP]
rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x)) hfm.norm.restrict]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ENNReal.toReal (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ) ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
[PROOFSTEP]
conv at hbounded in ENNReal.ofReal _ =>
  dsimp
  rw [← coe_nnnorm]
  rw [ENNReal.ofReal_coe_nnreal]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ENNReal.toReal (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ) ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
a : α
| ENNReal.ofReal ‖f a‖
[PROOFSTEP]
  dsimp
  rw [← coe_nnnorm]
  rw [ENNReal.ofReal_coe_nnreal]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ENNReal.toReal (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ) ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
a : α
| ENNReal.ofReal ‖f a‖
[PROOFSTEP]
  dsimp
  rw [← coe_nnnorm]
  rw [ENNReal.ofReal_coe_nnreal]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ENNReal.toReal (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ) ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
a : α
| ENNReal.ofReal ‖f a‖
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ENNReal.toReal (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ) ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
a : α
| ENNReal.ofReal ‖f a‖
[PROOFSTEP]
rw [← coe_nnnorm]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ENNReal.toReal (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ) ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
a : α
| ENNReal.ofReal ↑‖f a‖₊
[PROOFSTEP]
rw [ENNReal.ofReal_coe_nnreal]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ENNReal.toReal (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ) ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
[PROOFSTEP]
refine' hbounded.mono fun i hi => _
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ENNReal.toReal (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ) ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
hi : ENNReal.toReal (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ) ≤ I
⊢ ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
[PROOFSTEP]
rw [← ENNReal.ofReal_toReal (ne_top_of_lt (hfi i).2)]
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i)
hbounded : ∀ᶠ (i : ι) in l, ENNReal.toReal (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ) ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
hi : ENNReal.toReal (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ) ≤ I
⊢ ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ)) ≤ ENNReal.ofReal I
[PROOFSTEP]
apply ENNReal.ofReal_le_ofReal hi
[GOAL]
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f
h : Tendsto (fun i => ∫ (x : α), indicator (φ i) f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
⊢ Tendsto (fun i => ∫ (x : α) in φ i, f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
[PROOFSTEP]
convert h using 2
[GOAL]
case h.e'_3.h
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f
h : Tendsto (fun i => ∫ (x : α), indicator (φ i) f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
x✝ : ι
⊢ ∫ (x : α) in φ x✝, f x ∂μ = ∫ (x : α), indicator (φ x✝) f x ∂μ
[PROOFSTEP]
rw [integral_indicator (hφ.measurableSet _)]
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
⊢ Integrable f
[PROOFSTEP]
have hφ : AECover μ l _ := aecover_Ioc ha hb
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun i => Ioc (a i) (b i)
⊢ Integrable f
[PROOFSTEP]
refine' hφ.integrable_of_integral_norm_bounded I hfi (h.mp _)
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun i => Ioc (a i) (b i)
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioc (a x) (b x), ‖f x‖ ∂μ ≤ I
[PROOFSTEP]
filter_upwards [ha.eventually (eventually_le_atBot 0), hb.eventually (eventually_ge_atTop 0)] with i hai hbi ht
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun i => Ioc (a i) (b i)
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
ht : ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ ≤ I
[PROOFSTEP]
rwa [← intervalIntegral.integral_of_le (hai.trans hbi)]
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b✝ : ι → ℝ
f : ℝ → E
I b : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b)
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
⊢ IntegrableOn f (Iic b)
[PROOFSTEP]
have hφ : AECover (μ.restrict <| Iic b) l _ := aecover_Ioi ha
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b✝ : ι → ℝ
f : ℝ → E
I b : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b)
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Iic b)) l fun i => Ioi (a i)
⊢ IntegrableOn f (Iic b)
[PROOFSTEP]
have hfi : ∀ i, IntegrableOn f (Ioi (a i)) (μ.restrict <| Iic b) :=
  by
  intro i
  rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i)]
  exact hfi i
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b✝ : ι → ℝ
f : ℝ → E
I b : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b)
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Iic b)) l fun i => Ioi (a i)
⊢ ∀ (i : ι), IntegrableOn f (Ioi (a i))
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b✝ : ι → ℝ
f : ℝ → E
I b : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b)
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Iic b)) l fun i => Ioi (a i)
i : ι
⊢ IntegrableOn f (Ioi (a i))
[PROOFSTEP]
rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i)]
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b✝ : ι → ℝ
f : ℝ → E
I b : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b)
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Iic b)) l fun i => Ioi (a i)
i : ι
⊢ Integrable f
[PROOFSTEP]
exact hfi i
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b✝ : ι → ℝ
f : ℝ → E
I b : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b)
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Iic b)) l fun i => Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i))
⊢ IntegrableOn f (Iic b)
[PROOFSTEP]
refine' hφ.integrable_of_integral_norm_bounded I hfi (h.mp _)
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b✝ : ι → ℝ
f : ℝ → E
I b : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b)
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Iic b)) l fun i => Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i))
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a x), ‖f x‖ ∂Measure.restrict μ (Iic b) ≤ I
[PROOFSTEP]
filter_upwards [ha.eventually (eventually_le_atBot b)] with i hai
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b✝ : ι → ℝ
f : ℝ → E
I b : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b)
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Iic b)) l fun i => Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i))
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i), ‖f x‖ ∂Measure.restrict μ (Iic b) ≤ I
[PROOFSTEP]
rw [intervalIntegral.integral_of_le hai, Measure.restrict_restrict (hφ.measurableSet i)]
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b✝ : ι → ℝ
f : ℝ → E
I b : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc (a i) b)
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Iic b)) l fun i => Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i))
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in Ioc (a i) b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i) ∩ Iic b, ‖f x‖ ∂μ ≤ I
[PROOFSTEP]
exact id
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
have hφ : AECover (μ.restrict <| Ioi a) l _ := aecover_Iic hb
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
have hfi : ∀ i, IntegrableOn f (Iic (b i)) (μ.restrict <| Ioi a) :=
  by
  intro i
  rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
  exact hfi i
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
⊢ ∀ (i : ι), IntegrableOn f (Iic (b i))
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
i : ι
⊢ IntegrableOn f (Iic (b i))
[PROOFSTEP]
rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
i : ι
⊢ Integrable f
[PROOFSTEP]
exact hfi i
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
⊢ IntegrableOn f (Ioi a)
[PROOFSTEP]
refine' hφ.integrable_of_integral_norm_bounded I hfi (h.mp _)
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b x), ‖f x‖ ∂Measure.restrict μ (Ioi a) ≤ I
[PROOFSTEP]
filter_upwards [hb.eventually (eventually_ge_atTop a)] with i hbi
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
i : ι
hbi : a ≤ b i
⊢ ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b i), ‖f x‖ ∂Measure.restrict μ (Ioi a) ≤ I
[PROOFSTEP]
rw [intervalIntegral.integral_of_le hbi, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a✝ b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi✝ : ∀ (i : ι), IntegrableOn f (Ioc a (b i))
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (Measure.restrict μ (Ioi a)) l fun i => Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i))
i : ι
hbi : a ≤ b i
⊢ ∫ (x : ℝ) in Ioc a (b i), ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi a ∩ Iic (b i), ‖f x‖ ∂μ ≤ I
[PROOFSTEP]
exact id
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ IntegrableOn f (Ioc a₀ b₀)
[PROOFSTEP]
refine
  (aecover_Ioc_of_Ioc ha hb).integrable_of_integral_norm_bounded I (fun i => (hfi i).restrict measurableSet_Ioc)
    (h.mono fun i hi ↦ ?_)
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂Measure.restrict volume (Ioc a₀ b₀) ≤ I
[PROOFSTEP]
rw [Measure.restrict_restrict measurableSet_Ioc]
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i) ∩ Ioc a₀ b₀, ‖f x‖ ≤ I
[PROOFSTEP]
refine' le_trans (set_integral_mono_set (hfi i).norm _ _) hi
[GOAL]
case refine'_1
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ 0 ≤ᵐ[Measure.restrict volume (Ioc (a i) (b i))] fun x => ‖f x‖
[PROOFSTEP]
apply ae_of_all
[GOAL]
case refine'_2
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ Ioc (a i) (b i) ∩ Ioc a₀ b₀ ≤ᵐ[volume] Ioc (a i) (b i)
[PROOFSTEP]
apply ae_of_all
[GOAL]
case refine'_1.a
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∀ (a : ℝ), OfNat.ofNat 0 a ≤ (fun x => ‖f x‖) a
[PROOFSTEP]
simp only [Pi.zero_apply, norm_nonneg, forall_const]
[GOAL]
case refine'_2.a
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∀ (a_1 : ℝ), (Ioc (a i) (b i) ∩ Ioc a₀ b₀) a_1 ≤ Ioc (a i) (b i) a_1
[PROOFSTEP]
intro c hc
[GOAL]
case refine'_2.a
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : NeBot l
inst✝¹ : IsCountablyGenerated l
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i))
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
c : ℝ
hc : (Ioc (a i) (b i) ∩ Ioc a₀ b₀) c
⊢ Ioc (a i) (b i) c
[PROOFSTEP]
exact hc.1
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
[PROOFSTEP]
let φ i := Ioc (a i) (b i)
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
[PROOFSTEP]
have hφ : AECover μ l φ := aecover_Ioc ha hb
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
hφ : AECover μ l φ
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
[PROOFSTEP]
refine' (hφ.integral_tendsto_of_countably_generated hfi).congr' _
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
hφ : AECover μ l φ
⊢ (fun i => ∫ (x : ℝ) in φ i, f x ∂μ) =ᶠ[l] fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ
[PROOFSTEP]
filter_upwards [ha.eventually (eventually_le_atBot 0), hb.eventually (eventually_ge_atTop 0)] with i hai hbi
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Ioc (a i) (b i)
hφ : AECover μ l φ
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
⊢ ∫ (x : ℝ) in Ioc (a i) (b i), f x ∂μ = ∫ (x : ℝ) in a i..b i, f x ∂μ
[PROOFSTEP]
exact (intervalIntegral.integral_of_le (hai.trans hbi)).symm
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b✝ : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b)
ha : Tendsto a l atBot
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))
[PROOFSTEP]
let φ i := Ioi (a i)
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b✝ : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b)
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))
[PROOFSTEP]
have hφ : AECover (μ.restrict <| Iic b) l φ := aecover_Ioi ha
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b✝ : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b)
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (Measure.restrict μ (Iic b)) l φ
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))
[PROOFSTEP]
refine' (hφ.integral_tendsto_of_countably_generated hfi).congr' _
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b✝ : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b)
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (Measure.restrict μ (Iic b)) l φ
⊢ (fun i => ∫ (x : ℝ) in φ i, f x ∂Measure.restrict μ (Iic b)) =ᶠ[l] fun i => ∫ (x : ℝ) in a i..b, f x ∂μ
[PROOFSTEP]
filter_upwards [ha.eventually (eventually_le_atBot <| b)] with i hai
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b✝ : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b)
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (Measure.restrict μ (Iic b)) l φ
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in Ioi (a i), f x ∂Measure.restrict μ (Iic b) = ∫ (x : ℝ) in a i..b, f x ∂μ
[PROOFSTEP]
rw [intervalIntegral.integral_of_le hai, Measure.restrict_restrict (hφ.measurableSet i)]
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b✝ : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b)
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (Measure.restrict μ (Iic b)) l φ
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in φ i ∩ Iic b, f x ∂μ = ∫ (x : ℝ) in Ioc (a i) b, f x ∂μ
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a✝ b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a)
hb : Tendsto b l atTop
⊢ Tendsto (fun i => ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))
[PROOFSTEP]
let φ i := Iic (b i)
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a✝ b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a)
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Iic (b i)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))
[PROOFSTEP]
have hφ : AECover (μ.restrict <| Ioi a) l φ := aecover_Iic hb
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a✝ b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a)
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Iic (b i)
hφ : AECover (Measure.restrict μ (Ioi a)) l φ
⊢ Tendsto (fun i => ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))
[PROOFSTEP]
refine' (hφ.integral_tendsto_of_countably_generated hfi).congr' _
[GOAL]
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a✝ b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a)
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Iic (b i)
hφ : AECover (Measure.restrict μ (Ioi a)) l φ
⊢ (fun i => ∫ (x : ℝ) in φ i, f x ∂Measure.restrict μ (Ioi a)) =ᶠ[l] fun i => ∫ (x : ℝ) in a..b i, f x ∂μ
[PROOFSTEP]
filter_upwards [hb.eventually (eventually_ge_atTop <| a)] with i hbi
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a✝ b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a)
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Iic (b i)
hφ : AECover (Measure.restrict μ (Ioi a)) l φ
i : ι
hbi : a ≤ b i
⊢ ∫ (x : ℝ) in Iic (b i), f x ∂Measure.restrict μ (Ioi a) = ∫ (x : ℝ) in a..b i, f x ∂μ
[PROOFSTEP]
rw [intervalIntegral.integral_of_le hbi, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
[GOAL]
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝³ : IsCountablyGenerated l
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a✝ b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a)
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i => Iic (b i)
hφ : AECover (Measure.restrict μ (Ioi a)) l φ
i : ι
hbi : a ≤ b i
⊢ ∫ (x : ℝ) in Ioi a ∩ φ i, f x ∂μ = ∫ (x : ℝ) in Ioc a (b i), f x ∂μ
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ ∫ (x : ℝ) in Ioi a, f' x = m - f a
[PROOFSTEP]
refine' tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi a f'int tendsto_id) _
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x) atTop (𝓝 (m - f a))
[PROOFSTEP]
apply Tendsto.congr' _ (hf.sub_const _)
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ (fun k => f k - f a) =ᶠ[atTop] fun i => ∫ (x : ℝ) in a..id i, f' x
[PROOFSTEP]
filter_upwards [Ioi_mem_atTop a] with x hx
[GOAL]
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x
[PROOFSTEP]
have h'x : a ≤ id x := le_of_lt hx
[GOAL]
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x
[PROOFSTEP]
symm
[GOAL]
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ ∫ (x : ℝ) in a..id x, f' x = f x - f a
[PROOFSTEP]
apply
  intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self) fun y hy => hderiv y hy.1
[GOAL]
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable (fun y => f' y) volume a (id x)
[PROOFSTEP]
rw [intervalIntegrable_iff_integrable_Ioc_of_le h'x]
[GOAL]
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn (fun y => f' y) (Ioc a (id x))
[PROOFSTEP]
exact f'int.mono (fun y hy => hy.1) le_rfl
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ ∫ (x : ℝ) in Ioi a, f' x = m - f a
[PROOFSTEP]
refine integral_Ioi_of_hasDerivAt_of_tendsto (fun x hx ↦ ?_) (fun x hx => hderiv x hx.out.le) f'int hf
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) x
[PROOFSTEP]
exact (hderiv x hx).continuousAt.continuousWithinAt
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a)
[PROOFSTEP]
refine integrableOn_Ioi_of_intervalIntegral_norm_tendsto (l - g a) a (fun x => ?_) tendsto_id ?_
[GOAL]
case refine_1
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
⊢ IntegrableOn g' (Ioc a (id x))
[PROOFSTEP]
exact
  intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self) (fun y hy => hderiv y hy.1) fun y hy =>
    g'pos y hy.1
[GOAL]
case refine_2
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a..id i, ‖g' x‖) atTop (𝓝 (l - g a))
[PROOFSTEP]
apply Tendsto.congr' _ (hg.sub_const _)
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ (fun k => g k - g a) =ᶠ[atTop] fun i => ∫ (x : ℝ) in a..id i, ‖g' x‖
[PROOFSTEP]
filter_upwards [Ioi_mem_atTop a] with x hx
[GOAL]
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
[PROOFSTEP]
have h'x : a ≤ id x := le_of_lt hx
[GOAL]
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
[PROOFSTEP]
calc
  g x - g a = ∫ y in a..id x, g' y := by
    symm
    apply
      intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self) fun y hy =>
        hderiv y hy.1
    rw [intervalIntegrable_iff_integrable_Ioc_of_le h'x]
    exact
      intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self) (fun y hy => hderiv y hy.1)
        fun y hy => g'pos y hy.1
  _ = ∫ y in a..id x, ‖g' y‖ := by
    simp_rw [intervalIntegral.integral_of_le h'x]
    refine' set_integral_congr measurableSet_Ioc fun y hy => _
    dsimp
    rw [abs_of_nonneg]
    exact g'pos _ hy.1
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ g x - g a = ∫ (y : ℝ) in a..id x, g' y
[PROOFSTEP]
symm
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ ∫ (y : ℝ) in a..id x, g' y = g x - g a
[PROOFSTEP]
apply
  intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self) fun y hy => hderiv y hy.1
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable (fun y => g' y) volume a (id x)
[PROOFSTEP]
rw [intervalIntegrable_iff_integrable_Ioc_of_le h'x]
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn (fun y => g' y) (Ioc a (id x))
[PROOFSTEP]
exact
  intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self) (fun y hy => hderiv y hy.1) fun y hy =>
    g'pos y hy.1
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ ∫ (y : ℝ) in a..id x, g' y = ∫ (y : ℝ) in a..id x, ‖g' y‖
[PROOFSTEP]
simp_rw [intervalIntegral.integral_of_le h'x]
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ ∫ (y : ℝ) in Ioc a (id x), g' y = ∫ (y : ℝ) in Ioc a (id x), ‖g' y‖
[PROOFSTEP]
refine' set_integral_congr measurableSet_Ioc fun y hy => _
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ g' y = ‖g' y‖
[PROOFSTEP]
dsimp
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ g' y = |g' y|
[PROOFSTEP]
rw [abs_of_nonneg]
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ 0 ≤ g' y
[PROOFSTEP]
exact g'pos _ hy.1
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a)
[PROOFSTEP]
refine integrableOn_Ioi_deriv_of_nonneg (fun x hx ↦ ?_) (fun x hx => hderiv x hx.out.le) g'pos hg
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt g (Ici a) x
[PROOFSTEP]
exact (hderiv x hx).continuousAt.continuousWithinAt
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'neg : ∀ (x : ℝ), x ∈ Ioi a → g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a)
[PROOFSTEP]
apply integrable_neg_iff.1
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'neg : ∀ (x : ℝ), x ∈ Ioi a → g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ Integrable (-g')
[PROOFSTEP]
exact
  integrableOn_Ioi_deriv_of_nonneg hcont.neg (fun x hx => (hderiv x hx).neg)
    (fun x hx => neg_nonneg_of_nonpos (g'neg x hx)) hg.neg
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt g (g' x) x
g'neg : ∀ (x : ℝ), x ∈ Ioi a → g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a)
[PROOFSTEP]
refine integrableOn_Ioi_deriv_of_nonpos (fun x hx ↦ ?_) (fun x hx ↦ hderiv x hx.out.le) g'neg hg
[GOAL]
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt g (g' x) x
g'neg : ∀ (x : ℝ), x ∈ Ioi a → g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt g (Ici a) x
[PROOFSTEP]
exact (hderiv x hx).continuousAt.continuousWithinAt
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
⊢ ∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
[PROOFSTEP]
have eq : ∀ b : ℝ, a < b → (∫ x in a..b, f' x • (g ∘ f) x) = ∫ u in f a..f b, g u := fun b hb ↦
  by
  have i1 : Ioo (min a b) (max a b) ⊆ Ioi a := by
    rw [min_eq_left hb.le]
    exact Ioo_subset_Ioi_self
  have i2 : [[a, b]] ⊆ Ici a := by rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
  refine'
    intervalIntegral.integral_comp_smul_deriv''' (hf.mono i2) (fun x hx => hff' x <| mem_of_mem_of_subset hx i1)
      (hg_cont.mono <| image_subset _ _) (hg1.mono_set <| image_subset _ _) (hg2.mono_set i2)
  · rw [min_eq_left hb.le]; exact Ioo_subset_Ioi_self
  · rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
[PROOFSTEP]
have i1 : Ioo (min a b) (max a b) ⊆ Ioi a := by
  rw [min_eq_left hb.le]
  exact Ioo_subset_Ioi_self
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
⊢ Ioo (min a b) (max a b) ⊆ Ioi a
[PROOFSTEP]
rw [min_eq_left hb.le]
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
⊢ Ioo a (max a b) ⊆ Ioi a
[PROOFSTEP]
exact Ioo_subset_Ioi_self
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
[PROOFSTEP]
have i2 : [[a, b]] ⊆ Ici a := by rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ [[a, b]] ⊆ Ici a
[PROOFSTEP]
rw [uIcc_of_le hb.le]
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ Icc a b ⊆ Ici a
[PROOFSTEP]
exact Icc_subset_Ici_self
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
i2 : [[a, b]] ⊆ Ici a
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
[PROOFSTEP]
refine'
  intervalIntegral.integral_comp_smul_deriv''' (hf.mono i2) (fun x hx => hff' x <| mem_of_mem_of_subset hx i1)
    (hg_cont.mono <| image_subset _ _) (hg1.mono_set <| image_subset _ _) (hg2.mono_set i2)
[GOAL]
case refine'_1
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
i2 : [[a, b]] ⊆ Ici a
⊢ Ioo (min a b) (max a b) ⊆ Ioi a
[PROOFSTEP]
rw [min_eq_left hb.le]
[GOAL]
case refine'_1
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
i2 : [[a, b]] ⊆ Ici a
⊢ Ioo a (max a b) ⊆ Ioi a
[PROOFSTEP]
exact Ioo_subset_Ioi_self
[GOAL]
case refine'_2
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
i2 : [[a, b]] ⊆ Ici a
⊢ [[a, b]] ⊆ Ici a
[PROOFSTEP]
rw [uIcc_of_le hb.le]
[GOAL]
case refine'_2
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
i2 : [[a, b]] ⊆ Ici a
⊢ Icc a b ⊆ Ici a
[PROOFSTEP]
exact Icc_subset_Ici_self
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
⊢ ∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
[PROOFSTEP]
rw [integrableOn_Ici_iff_integrableOn_Ioi] at hg2 
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ioi a)
eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
⊢ ∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
[PROOFSTEP]
have t2 := intervalIntegral_tendsto_integral_Ioi _ hg2 tendsto_id
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ioi a)
eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
t2 : Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop (𝓝 (∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x))
⊢ ∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
[PROOFSTEP]
have : Ioi (f a) ⊆ f '' Ici a :=
  Ioi_subset_Ici_self.trans <|
    IsPreconnected.intermediate_value_Ici isPreconnected_Ici left_mem_Ici (le_principal_iff.mpr <| Ici_mem_atTop _) hf
      hft
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ioi a)
eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
t2 : Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop (𝓝 (∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x))
this : Ioi (f a) ⊆ f '' Ici a
⊢ ∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
[PROOFSTEP]
have t1 := (intervalIntegral_tendsto_integral_Ioi _ (hg1.mono_set this) tendsto_id).comp hft
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ioi a)
eq : ∀ (b : ℝ), a < b → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
t2 : Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop (𝓝 (∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x))
this : Ioi (f a) ⊆ f '' Ici a
t1 : Tendsto ((fun i => ∫ (x : ℝ) in f a..id i, g x) ∘ f) atTop (𝓝 (∫ (x : ℝ) in Ioi (f a), g x))
⊢ ∫ (x : ℝ) in Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Ioi (f a), g u
[PROOFSTEP]
exact tendsto_nhds_unique (Tendsto.congr' (eventuallyEq_of_mem (Ioi_mem_atTop a) eq) t2) t1
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a)
⊢ ∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Ioi (f a), g u
[PROOFSTEP]
have hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) := by simpa [mul_comm] using hg2
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a)
⊢ IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
[PROOFSTEP]
simpa [mul_comm] using hg2
[GOAL]
E : Type u_1
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a)
hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
⊢ ∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Ioi (f a), g u
[PROOFSTEP]
simpa [mul_comm] using integral_comp_smul_deriv_Ioi hf hft hff' hg_cont hg1 hg2'
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
[PROOFSTEP]
let S := Ioi (0 : ℝ)
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
[PROOFSTEP]
have a1 : ∀ x : ℝ, x ∈ S → HasDerivWithinAt (fun t : ℝ => t ^ p) (p * x ^ (p - 1)) S x := fun x hx =>
  (hasDerivAt_rpow_const (Or.inl (mem_Ioi.mp hx).ne')).hasDerivWithinAt
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
[PROOFSTEP]
have a2 : InjOn (fun x : ℝ => x ^ p) S :=
  by
  rcases lt_or_gt_of_ne hp with (h | h)
  · apply StrictAntiOn.injOn
    intro x hx y hy hxy
    rw [← inv_lt_inv (rpow_pos_of_pos hx p) (rpow_pos_of_pos hy p), ← rpow_neg (le_of_lt hx), ← rpow_neg (le_of_lt hy)]
    exact rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h)
  exact StrictMonoOn.injOn fun x hx y _ hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
⊢ InjOn (fun x => x ^ p) S
[PROOFSTEP]
rcases lt_or_gt_of_ne hp with (h | h)
[GOAL]
case inl
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ InjOn (fun x => x ^ p) S
[PROOFSTEP]
apply StrictAntiOn.injOn
[GOAL]
case inl.H
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ StrictAntiOn (fun x => x ^ p) S
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
case inl.H
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ (fun x => x ^ p) y < (fun x => x ^ p) x
[PROOFSTEP]
rw [← inv_lt_inv (rpow_pos_of_pos hx p) (rpow_pos_of_pos hy p), ← rpow_neg (le_of_lt hx), ← rpow_neg (le_of_lt hy)]
[GOAL]
case inl.H
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ x ^ (-p) < y ^ (-p)
[PROOFSTEP]
exact rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h)
[GOAL]
case inr
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p > 0
⊢ InjOn (fun x => x ^ p) S
[PROOFSTEP]
exact StrictMonoOn.injOn fun x hx y _ hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
[PROOFSTEP]
have a3 : (fun t : ℝ => t ^ p) '' S = S := by
  ext1 x; rw [mem_image]; constructor
  · rintro ⟨y, hy, rfl⟩; exact rpow_pos_of_pos hy p
  · intro hx; refine' ⟨x ^ (1 / p), rpow_pos_of_pos hx _, _⟩
    rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
⊢ (fun t => t ^ p) '' S = S
[PROOFSTEP]
ext1 x
[GOAL]
case h
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ (fun t => t ^ p) '' S ↔ x ∈ S
[PROOFSTEP]
rw [mem_image]
[GOAL]
case h
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x) ↔ x ∈ S
[PROOFSTEP]
constructor
[GOAL]
case h.mp
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x) → x ∈ S
[PROOFSTEP]
rintro ⟨y, hy, rfl⟩
[GOAL]
case h.mp.intro.intro
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
y : ℝ
hy : y ∈ S
⊢ y ^ p ∈ S
[PROOFSTEP]
exact rpow_pos_of_pos hy p
[GOAL]
case h.mpr
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ S → ∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x
[PROOFSTEP]
intro hx
[GOAL]
case h.mpr
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ ∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x
[PROOFSTEP]
refine' ⟨x ^ (1 / p), rpow_pos_of_pos hx _, _⟩
[GOAL]
case h.mpr
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ (x ^ (1 / p)) ^ p = x
[PROOFSTEP]
rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
[PROOFSTEP]
have := integral_image_eq_integral_abs_deriv_smul measurableSet_Ioi a1 a2 g
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : ∫ (x : ℝ) in (fun t => t ^ p) '' Ioi 0, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
[PROOFSTEP]
rw [a3] at this 
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : ∫ (x : ℝ) in S, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
[PROOFSTEP]
rw [this]
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : ∫ (x : ℝ) in S, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
[PROOFSTEP]
refine' set_integral_congr measurableSet_Ioi _
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : ∫ (x : ℝ) in S, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
⊢ EqOn (fun x => (|p| * x ^ (p - 1)) • g (x ^ p)) (fun x => |p * x ^ (p - 1)| • g (x ^ p)) (Ioi 0)
[PROOFSTEP]
intro x hx
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : ∫ (x : ℝ) in S, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => (|p| * x ^ (p - 1)) • g (x ^ p)) x = (fun x => |p * x ^ (p - 1)| • g (x ^ p)) x
[PROOFSTEP]
dsimp only
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : ∫ (x : ℝ) in S, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
x : ℝ
hx : x ∈ Ioi 0
⊢ (|p| * x ^ (p - 1)) • g (x ^ p) = |p * x ^ (p - 1)| • g (x ^ p)
[PROOFSTEP]
rw [abs_mul, abs_of_nonneg (rpow_nonneg_of_nonneg (le_of_lt hx) _)]
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : 0 < p
⊢ ∫ (x : ℝ) in Ioi 0, (p * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
[PROOFSTEP]
convert integral_comp_rpow_Ioi g hp.ne'
[GOAL]
case h.e'_2.h.e'_7.h.h.e'_5.h.e'_5
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : 0 < p
x✝ : ℝ
⊢ p = |p|
[PROOFSTEP]
funext
[GOAL]
case h.e'_2.h.e'_7.h.h.e'_5.h.e'_5
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : 0 < p
x✝ : ℝ
⊢ p = |p|
[PROOFSTEP]
congr
[GOAL]
case h.e'_2.h.e'_7.h.h.e'_5.h.e'_5
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
p : ℝ
hp : 0 < p
x✝ : ℝ
⊢ p = |p|
[PROOFSTEP]
rw [abs_of_nonneg hp.le]
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi a, g (b * x) = |b⁻¹| • ∫ (x : ℝ) in Ioi (b * a), g x
[PROOFSTEP]
have : ∀ c : ℝ, MeasurableSet (Ioi c) := fun c => measurableSet_Ioi
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ ∫ (x : ℝ) in Ioi a, g (b * x) = |b⁻¹| • ∫ (x : ℝ) in Ioi (b * a), g x
[PROOFSTEP]
rw [← integral_indicator (this a), ← integral_indicator (this (b * a)), ← Measure.integral_comp_mul_left]
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ ∫ (x : ℝ), indicator (Ioi a) (fun x => g (b * x)) x = ∫ (x : ℝ), indicator (Ioi (b * a)) (fun x => g x) (b * x)
[PROOFSTEP]
congr
[GOAL]
case e_f
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ (fun x => indicator (Ioi a) (fun x => g (b * x)) x) = fun x => indicator (Ioi (b * a)) (fun x => g x) (b * x)
[PROOFSTEP]
ext1 x
[GOAL]
case e_f.h
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
x : ℝ
⊢ indicator (Ioi a) (fun x => g (b * x)) x = indicator (Ioi (b * a)) (fun x => g x) (b * x)
[PROOFSTEP]
rw [← indicator_comp_right, preimage_const_mul_Ioi _ hb, mul_div_cancel_left _ hb.ne']
[GOAL]
case e_f.h
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
x : ℝ
⊢ indicator (Ioi a) (fun x => g (b * x)) x = indicator (Ioi a) ((fun x => g x) ∘ HMul.hMul b) x
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi a, g (x * b) = |b⁻¹| • ∫ (x : ℝ) in Ioi (a * b), g x
[PROOFSTEP]
simpa only [mul_comm] using integral_comp_mul_left_Ioi g a hb
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
[PROOFSTEP]
let S := Ioi (0 : ℝ)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
[PROOFSTEP]
have a1 : ∀ x : ℝ, x ∈ S → HasDerivWithinAt (fun t : ℝ => t ^ p) (p * x ^ (p - 1)) S x := fun x hx =>
  (hasDerivAt_rpow_const (Or.inl (mem_Ioi.mp hx).ne')).hasDerivWithinAt
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
[PROOFSTEP]
have a2 : InjOn (fun x : ℝ => x ^ p) S :=
  by
  rcases lt_or_gt_of_ne hp with (h | h)
  · apply StrictAntiOn.injOn
    intro x hx y hy hxy
    rw [← inv_lt_inv (rpow_pos_of_pos hx p) (rpow_pos_of_pos hy p), ← rpow_neg (le_of_lt hx), ← rpow_neg (le_of_lt hy)]
    exact rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h)
  exact StrictMonoOn.injOn fun x hx y _hy hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
⊢ InjOn (fun x => x ^ p) S
[PROOFSTEP]
rcases lt_or_gt_of_ne hp with (h | h)
[GOAL]
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ InjOn (fun x => x ^ p) S
[PROOFSTEP]
apply StrictAntiOn.injOn
[GOAL]
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ StrictAntiOn (fun x => x ^ p) S
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ (fun x => x ^ p) y < (fun x => x ^ p) x
[PROOFSTEP]
rw [← inv_lt_inv (rpow_pos_of_pos hx p) (rpow_pos_of_pos hy p), ← rpow_neg (le_of_lt hx), ← rpow_neg (le_of_lt hy)]
[GOAL]
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ x ^ (-p) < y ^ (-p)
[PROOFSTEP]
exact rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h)
[GOAL]
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
h : p > 0
⊢ InjOn (fun x => x ^ p) S
[PROOFSTEP]
exact StrictMonoOn.injOn fun x hx y _hy hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
[PROOFSTEP]
have a3 : (fun t : ℝ => t ^ p) '' S = S := by
  ext1 x; rw [mem_image]; constructor
  · rintro ⟨y, hy, rfl⟩; exact rpow_pos_of_pos hy p
  · intro hx; refine' ⟨x ^ (1 / p), rpow_pos_of_pos hx _, _⟩
    rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
⊢ (fun t => t ^ p) '' S = S
[PROOFSTEP]
ext1 x
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ (fun t => t ^ p) '' S ↔ x ∈ S
[PROOFSTEP]
rw [mem_image]
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x) ↔ x ∈ S
[PROOFSTEP]
constructor
[GOAL]
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x) → x ∈ S
[PROOFSTEP]
rintro ⟨y, hy, rfl⟩
[GOAL]
case h.mp.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
y : ℝ
hy : y ∈ S
⊢ y ^ p ∈ S
[PROOFSTEP]
exact rpow_pos_of_pos hy p
[GOAL]
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ S → ∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x
[PROOFSTEP]
intro hx
[GOAL]
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ ∃ x_1, x_1 ∈ S ∧ x_1 ^ p = x
[PROOFSTEP]
refine' ⟨x ^ (1 / p), rpow_pos_of_pos hx _, _⟩
[GOAL]
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ (x ^ (1 / p)) ^ p = x
[PROOFSTEP]
rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
[PROOFSTEP]
have := integrableOn_image_iff_integrableOn_abs_deriv_smul measurableSet_Ioi a1 a2 f
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f ((fun t => t ^ p) '' Ioi 0) ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0)
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
[PROOFSTEP]
rw [a3] at this 
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0)
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
[PROOFSTEP]
rw [this]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0)
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔
    IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0)
[PROOFSTEP]
refine' integrableOn_congr_fun (fun x hx => _) measurableSet_Ioi
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ (x : ℝ), x ∈ S → HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
⊢ (|p| * x ^ (p - 1)) • f (x ^ p) = |p * x ^ (p - 1)| • f (x ^ p)
[PROOFSTEP]
simp_rw [abs_mul, abs_of_nonneg (rpow_nonneg_of_nonneg (le_of_lt hx) _)]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
⊢ IntegrableOn (fun x => x ^ (p - 1) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)
[PROOFSTEP]
simpa only [← integrableOn_Ioi_comp_rpow_iff f hp, mul_smul] using (integrable_smul_iff (abs_pos.mpr hp).ne' _).symm
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => f (a * x)) (Ioi c) ↔ IntegrableOn f (Ioi (a * c))
[PROOFSTEP]
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi c)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable (indicator (Ioi c) fun x => f (a * x)) ↔ IntegrableOn f (Ioi (a * c))
[PROOFSTEP]
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi <| a * c)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable (indicator (Ioi c) fun x => f (a * x)) ↔ Integrable (indicator (Ioi (a * c)) f)
[PROOFSTEP]
convert integrable_comp_mul_left_iff ((Ioi (a * c)).indicator f) ha.ne' using 2
[GOAL]
case h.e'_1.h.e'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ (indicator (Ioi c) fun x => f (a * x)) = fun x => indicator (Ioi (a * c)) f (a * x)
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_1.h.e'_5.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ indicator (Ioi c) (fun x => f (a * x)) x = indicator (Ioi (a * c)) f (a * x)
[PROOFSTEP]
rw [← indicator_comp_right, preimage_const_mul_Ioi _ ha, mul_comm a c, mul_div_cancel _ ha.ne']
[GOAL]
case h.e'_1.h.e'_5.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ indicator (Ioi c) (fun x => f (a * x)) x = indicator (Ioi c) (f ∘ HMul.hMul a) x
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => f (x * a)) (Ioi c) ↔ IntegrableOn f (Ioi (c * a))
[PROOFSTEP]
simpa only [mul_comm, mul_zero] using integrableOn_Ioi_comp_mul_left_iff f c ha
