case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

case neg
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : ¬a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
by_cases h : a ≤ b
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
have : ∀ x ∈ Icc a b, (∫ t in Ioc a x, f t ∂μ) = ∫ t in a..x, f t ∂μ := by
  intro x x_in
  simp_rw [← uIoc_of_le h, integral_of_le x_in.1]
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b)
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
rw [continuousOn_congr this]
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b) x₀
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b)
intro x₀ _
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ IntervalIntegrable (fun t => f t) μ (min a a) (max a b)
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b) x₀
refine' continuousWithinAt_primitive (measure_singleton x₀) _
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ IntegrableOn (fun t => f t) (Ioc a b)
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ IntervalIntegrable (fun t => f t) μ (min a a) (max a b)
simp only [intervalIntegrable_iff_integrable_Ioc_of_le, min_eq_left, max_eq_right, h, min_self]
no goals
case pos
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
this : ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ IntegrableOn (fun t => f t) (Ioc a b)
exact h_int.mono Ioc_subset_Icc_self le_rfl
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
x : ℝ
x_in : x ∈ Icc a b
⊢ (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
⊢ ∀ (x : ℝ), x ∈ Icc a b → (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
intro x x_in
no goals
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : a ≤ b
x : ℝ
x_in : x ∈ Icc a b
⊢ (∫ (t : ℝ) in Ioc a x, f t ∂μ) = ∫ (t : ℝ) in a..x, f t ∂μ
simp_rw [← uIoc_of_le h, integral_of_le x_in.1]
case neg
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : ¬a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) ∅
case neg
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : ¬a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
rw [Icc_eq_empty h]
no goals
case neg
ι : Type ?u.18234336
𝕜 : Type ?u.18234339
E : Type u_1
F : Type ?u.18234345
A : Type ?u.18234348
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
h : ¬a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) ∅
exact continuousOn_empty _