case pos
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

case neg
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : ¬b₀ ∈ Icc b₁ b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
by_cases h₀ : b₀ ∈ Icc b₁ b₂
case pos
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
case pos
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have h₁₂ : b₁ ≤ b₂ := h₀.1.trans h₀.2
case pos
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
case pos
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have min₁₂ : min b₁ b₂ = b₁ := min_eq_left h₁₂
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  ∀ (b : ℝ), b ∈ Icc b₁ b₂ → (∫ (x : ℝ) in a..b, f x ∂μ) = (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..b, f x ∂μ
⊢ ContinuousWithinAt (fun y => (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
case pos
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  ∀ (b : ℝ), b ∈ Icc b₁ b₂ → (∫ (x : ℝ) in a..b, f x ∂μ) = (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..b, f x ∂μ
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
apply ContinuousWithinAt.congr _ this (this _ h₀)
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ ContinuousWithinAt (fun y => (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  ∀ (b : ℝ), b ∈ Icc b₁ b₂ → (∫ (x : ℝ) in a..b, f x ∂μ) = (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..b, f x ∂μ
⊢ ContinuousWithinAt (fun y => (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
clear this
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ ContinuousWithinAt (fun y => ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ ContinuousWithinAt (fun y => (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
refine' continuousWithinAt_const.add _
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ContinuousWithinAt (fun y => ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ ContinuousWithinAt (fun y => ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
have :
  (fun b => ∫ x in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b =>
    ∫ x in b₁..b₂, indicator {x | x ≤ b} f x ∂μ := by
  apply eventuallyEq_of_mem self_mem_nhdsWithin
  exact fun b b_in => (integral_indicator b_in).symm
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ) (Icc b₁ b₂) b₀
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ContinuousWithinAt (fun y => ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
apply ContinuousWithinAt.congr_of_eventuallyEq _ this (integral_indicator h₀).symm
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : IntervalIntegrable (fun x => ‖f x‖) μ b₁ b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ) (Icc b₁ b₂) b₀
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ) (Icc b₁ b₂) b₀
have : IntervalIntegrable (fun x => ‖f x‖) μ b₁ b₂ :=
  IntervalIntegrable.norm (h_int' <| right_mem_Icc.mpr h₁₂)
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀,
    AEStronglyMeasurable (fun x_1 => indicator {x_2 | x_2 ≤ x} f x_1) (Measure.restrict μ (Ι b₁ b₂))

case refine'_2
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 | x_1 ≤ x} f t‖ ≤ ‖f t‖

case refine'_3
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f t) (Icc b₁ b₂) b₀
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : IntervalIntegrable (fun x => ‖f x‖) μ b₁ b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ) (Icc b₁ b₂) b₀
refine' continuousWithinAt_of_dominated_interval _ _ this _ <;> clear this
case intro
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ IntervalIntegrable f μ b₁ x
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
⊢ ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
rintro x ⟨h₁, h₂⟩
case intro
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ [[b₁, x]] ⊆ [[min a b₁, max a b₂]]
case intro
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ IntervalIntegrable f μ b₁ x
apply h_int.mono_set
case intro.h₁
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ b₁ ∈ [[min a b₁, max a b₂]]

case intro.h₂
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ x ∈ [[min a b₁, max a b₂]]
case intro
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ [[b₁, x]] ⊆ [[min a b₁, max a b₂]]
apply uIcc_subset_uIcc
no goals
case intro.h₁
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ b₁ ∈ [[min a b₁, max a b₂]]
exact ⟨min_le_of_left_le (min_le_right a b₁),
  h₁.trans (h₂.trans <| le_max_of_le_right <| le_max_right _ _)⟩
no goals
case intro.h₂
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ x ∈ [[min a b₁, max a b₂]]
exact ⟨min_le_of_left_le <| (min_le_right _ _).trans h₁,
  le_max_of_le_right <| h₂.trans <| le_max_right _ _⟩
case intro
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..b, f x ∂μ
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ ∀ (b : ℝ), b ∈ Icc b₁ b₂ → (∫ (x : ℝ) in a..b, f x ∂μ) = (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..b, f x ∂μ
rintro b ⟨h₁, h₂⟩
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ IntervalIntegrable f μ a b₁
case intro
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = (∫ (x : ℝ) in a..b₁, f x ∂μ) + ∫ (x : ℝ) in b₁..b, f x ∂μ
rw [← integral_add_adjacent_intervals _ (h_int' ⟨h₁, h₂⟩)]
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ [[a, b₁]] ⊆ [[min a b₁, max a b₂]]
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ IntervalIntegrable f μ a b₁
apply h_int.mono_set
case h₁
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ a ∈ [[min a b₁, max a b₂]]

case h₂
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ b₁ ∈ [[min a b₁, max a b₂]]
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ [[a, b₁]] ⊆ [[min a b₁, max a b₂]]
apply uIcc_subset_uIcc
no goals
case h₁
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ a ∈ [[min a b₁, max a b₂]]
exact ⟨min_le_of_left_le (min_le_left a b₁), le_max_of_le_right (le_max_left _ _)⟩
no goals
case h₂
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b✝ b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ b₁ ∈ [[min a b₁, max a b₂]]
exact ⟨min_le_of_left_le (min_le_right _ _),
  le_max_of_le_right (h₁.trans <| h₂.trans (le_max_right a b₂))⟩
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ EqOn (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) (fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ) (Icc b₁ b₂)
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
apply eventuallyEq_of_mem self_mem_nhdsWithin
no goals
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ EqOn (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) (fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ) (Icc b₁ b₂)
exact fun b b_in => (integral_indicator b_in).symm
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ (x : ℝ),
    b₁ ≤ x ∧ x ≤ b₂ → AEStronglyMeasurable (fun x_1 => indicator {x_2 | x_2 ≤ x} f x_1) (Measure.restrict μ (Ι b₁ b₂))
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀,
    AEStronglyMeasurable (fun x_1 => indicator {x_2 | x_2 ≤ x} f x_1) (Measure.restrict μ (Ι b₁ b₂))
apply Eventually.mono self_mem_nhdsWithin
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ AEStronglyMeasurable (fun x_1 => indicator {x_2 | x_2 ≤ x} f x_1) (Measure.restrict μ (Ι b₁ b₂))
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ (x : ℝ),
    b₁ ≤ x ∧ x ≤ b₂ → AEStronglyMeasurable (fun x_1 => indicator {x_2 | x_2 ≤ x} f x_1) (Measure.restrict μ (Ι b₁ b₂))
intro x hx
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ AEStronglyMeasurable f (Measure.restrict μ (Ioc (min b₁ b₂) x))

case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ x ≤ max b₁ b₂

case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ MeasurableSet {x_1 | x_1 ≤ x}

case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ MeasurableSet {x_1 | x_1 ≤ x}
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ AEStronglyMeasurable (fun x_1 => indicator {x_2 | x_2 ≤ x} f x_1) (Measure.restrict μ (Ι b₁ b₂))
erw [aestronglyMeasurable_indicator_iff, Measure.restrict_restrict, Iic_inter_Ioc_of_le]
no goals
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ MeasurableSet {x_1 | x_1 ≤ x}

case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ MeasurableSet {x_1 | x_1 ≤ x}
exacts [measurableSet_Iic, measurableSet_Iic]
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ AEStronglyMeasurable f (Measure.restrict μ (Ioc b₁ x))
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ AEStronglyMeasurable f (Measure.restrict μ (Ioc (min b₁ b₂) x))
rw [min₁₂]
no goals
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ AEStronglyMeasurable f (Measure.restrict μ (Ioc b₁ x))
exact (h_int' hx).1.aestronglyMeasurable
no goals
case refine'_1
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : b₁ ≤ x ∧ x ≤ b₂
⊢ x ≤ max b₁ b₂
exact le_max_of_le_right hx.2
case refine'_2
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x t : ℝ
⊢ t ∈ Ι b₁ b₂ → ‖indicator {x_1 | x_1 ≤ x} f t‖ ≤ ‖f t‖
case refine'_2
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 | x_1 ≤ x} f t‖ ≤ ‖f t‖
refine' eventually_of_forall fun x => eventually_of_forall fun t => _
case refine'_2
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x t : ℝ
⊢ t ∈ Ι b₁ b₂ → ‖if t ≤ x then f t else 0‖ ≤ ‖f t‖
case refine'_2
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x t : ℝ
⊢ t ∈ Ι b₁ b₂ → ‖indicator {x_1 | x_1 ≤ x} f t‖ ≤ ‖f t‖
dsimp [indicator]
no goals
case refine'_2
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x t : ℝ
⊢ t ∈ Ι b₁ b₂ → ‖if t ≤ x then f t else 0‖ ≤ ‖f t‖
split_ifs <;> simp
case refine'_3
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
⊢ ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f t) (Icc b₁ b₂) b₀
case refine'_3
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f t) (Icc b₁ b₂) b₀
have : ∀ᵐ t ∂μ, t < b₀ ∨ b₀ < t := by
  apply Eventually.mono (compl_mem_ae_iff.mpr hb₀)
  intro x hx
  exact Ne.lt_or_lt hx
case refine'_3
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
⊢ ∀ (x : ℝ), x < b₀ ∨ b₀ < x → x ∈ Ι b₁ b₂ → ContinuousWithinAt (fun x_1 => indicator {x | x ≤ x_1} f x) (Icc b₁ b₂) b₀
case refine'_3
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
⊢ ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f t) (Icc b₁ b₂) b₀
apply this.mono
case refine'_3.inl
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀

case refine'_3.inr
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
⊢ ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
case refine'_3
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
⊢ ∀ (x : ℝ), x < b₀ ∨ b₀ < x → x ∈ Ι b₁ b₂ → ContinuousWithinAt (fun x_1 => indicator {x | x ≤ x_1} f x) (Icc b₁ b₂) b₀
rintro x₀ (hx₀ | hx₀) -
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ (x : ℝ), ¬x ∈ {b₀} → x < b₀ ∨ b₀ < x
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
apply Eventually.mono (compl_mem_ae_iff.mpr hb₀)
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : ¬x ∈ {b₀}
⊢ x < b₀ ∨ b₀ < x
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
⊢ ∀ (x : ℝ), ¬x ∈ {b₀} → x < b₀ ∨ b₀ < x
intro x hx
no goals
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
x : ℝ
hx : ¬x ∈ {b₀}
⊢ x < b₀ ∨ b₀ < x
exact Ne.lt_or_lt hx
case refine'_3.inl
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝¹ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this✝ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = f x₀
⊢ ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
case refine'_3.inl
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
have : ∀ᶠ x in 𝓝[Icc b₁ b₂] b₀, {t : ℝ | t ≤ x}.indicator f x₀ = f x₀ := by
  apply mem_nhdsWithin_of_mem_nhds
  apply Eventually.mono (Ioi_mem_nhds hx₀)
  intro x hx
  simp [hx.le]
case refine'_3.inl
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝¹ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this✝ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = f x₀
⊢ indicator {t | t ≤ b₀} f x₀ = f x₀
case refine'_3.inl
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝¹ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this✝ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = f x₀
⊢ ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
apply continuousWithinAt_const.congr_of_eventuallyEq this
no goals
case refine'_3.inl
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝¹ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this✝ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = f x₀
⊢ indicator {t | t ≤ b₀} f x₀ = f x₀
simp [hx₀.le]
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ {x | (fun x => indicator {t | t ≤ x} f x₀ = f x₀) x} ∈ 𝓝 b₀
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = f x₀
apply mem_nhdsWithin_of_mem_nhds
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ ∀ (x : ℝ), x₀ < x → indicator {t | t ≤ x} f x₀ = f x₀
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ {x | (fun x => indicator {t | t ≤ x} f x₀ = f x₀) x} ∈ 𝓝 b₀
apply Eventually.mono (Ioi_mem_nhds hx₀)
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
x : ℝ
hx : x₀ < x
⊢ indicator {t | t ≤ x} f x₀ = f x₀
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ ∀ (x : ℝ), x₀ < x → indicator {t | t ≤ x} f x₀ = f x₀
intro x hx
no goals
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
x : ℝ
hx : x₀ < x
⊢ indicator {t | t ≤ x} f x₀ = f x₀
simp [hx.le]
case refine'_3.inr
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝¹ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this✝ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = 0
⊢ ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
case refine'_3.inr
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
⊢ ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
have : ∀ᶠ x in 𝓝[Icc b₁ b₂] b₀, {t : ℝ | t ≤ x}.indicator f x₀ = 0 := by
  apply mem_nhdsWithin_of_mem_nhds
  apply Eventually.mono (Iio_mem_nhds hx₀)
  intro x hx
  simp [hx]
case refine'_3.inr
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝¹ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this✝ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = 0
⊢ indicator {t | t ≤ b₀} f x₀ = 0
case refine'_3.inr
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝¹ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this✝ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = 0
⊢ ContinuousWithinAt (fun x => indicator {x_1 | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
apply continuousWithinAt_const.congr_of_eventuallyEq this
no goals
case refine'_3.inr
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝¹ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this✝ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = 0
⊢ indicator {t | t ≤ b₀} f x₀ = 0
simp [hx₀]
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
⊢ {x | (fun x => indicator {t | t ≤ x} f x₀ = 0) x} ∈ 𝓝 b₀
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t | t ≤ x} f x₀ = 0
apply mem_nhdsWithin_of_mem_nhds
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
⊢ ∀ (x : ℝ), x < x₀ → indicator {t | t ≤ x} f x₀ = 0
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
⊢ {x | (fun x => indicator {t | t ≤ x} f x₀ = 0) x} ∈ 𝓝 b₀
apply Eventually.mono (Iio_mem_nhds hx₀)
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
x : ℝ
hx : x < x₀
⊢ indicator {t | t ≤ x} f x₀ = 0
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
⊢ ∀ (x : ℝ), x < x₀ → indicator {t | t ≤ x} f x₀ = 0
intro x hx
no goals
case h
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b => ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b => ∫ (x : ℝ) in b₁..b₂, indicator {x | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
x : ℝ
hx : x < x₀
⊢ indicator {t | t ≤ x} f x₀ = 0
simp [hx]
case neg.a
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : ¬b₀ ∈ Icc b₁ b₂
⊢ ¬b₀ ∈ closure (Icc b₁ b₂)
case neg
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : ¬b₀ ∈ Icc b₁ b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
apply continuousWithinAt_of_not_mem_closure
no goals
case neg.a
ι : Type ?u.18098281
𝕜 : Type ?u.18098284
E : Type u_1
F : Type ?u.18098290
A : Type ?u.18098293
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
hb₀ : ↑↑μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : ¬b₀ ∈ Icc b₁ b₂
⊢ ¬b₀ ∈ closure (Icc b₁ b₂)
rwa [closure_Icc]