-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem continuousWithinAt_primitive (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₀

Proof state:
case refine_2.h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
x t : ℝ
⊢ t ∈ Ι b₁ b₂ → ‖if t ≤ x then f t else 0‖ ≤ ‖f t‖

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₀

Tactic:
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

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
⊢ ContinuousWithinAt (fun y => ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀

Proof state:
case intro.h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : b₁ ⊓ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ b₁ ∈ [[a ⊓ b₁, a ⊔ b₂]]

Tactic:
exact ⟨min_le_of_left_le (min_le_right a b₁),
  h₁.trans (h₂.trans <| le_max_of_le_right <| le_max_right _ _)⟩

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
⊢ ∀ a ∈ Icc b₁ b₂, AEStronglyMeasurable ({x | x ≤ a}.indicator f) (μ.restrict (Ι b₁ b₂))

Tactic:
intro x hx

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ AEStronglyMeasurable ({x_1 | x_1 ≤ x}.indicator f) (μ.restrict (Ι b₁ b₂))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
⊢ ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t

Tactic:
filter_upwards [compl_mem_ae_iff.mpr hb₀] with x hx using Ne.lt_or_lt hx

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ AEStronglyMeasurable f (μ.restrict (Ioc b₁ x))

Tactic:
exact (h_int' hx).1.aestronglyMeasurable

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ {x | (fun x => {t | t ≤ x}.indicator f x₀ = f x₀) x} ∈ 𝓝 b₀

Tactic:
apply Eventually.mono (Ioi_mem_nhds hx₀)

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ ∀ (x : ℝ), x₀ < x → {t | t ≤ x}.indicator f x₀ = f x₀

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ MeasurableSet {x_1 | x_1 ≤ x}

case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ MeasurableSet {x_1 | x_1 ≤ x}

Tactic:
exacts [measurableSet_Iic, measurableSet_Iic]

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
x : ℝ
hx : x₀ < x
⊢ {t | t ≤ x}.indicator f x₀ = f x₀

Tactic:
simp [hx.le]

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (a ⊓ b₁) (a ⊔ b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
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₂, {x | x ≤ b}.indicator f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
x : ℝ
hx : x < x₀
⊢ {t | t ≤ x}.indicator f x₀ = 0

Tactic:
simp [hx]

Result:
no goals