Theorem: ContinuousOn.intervalIntegral
Proof state before:
case intro.intro
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..b, f x t) s x
Tactic:
apply intervalIntegral.continuousWithinAt_of_dominated_interval (bound := fun _ ↦ c)
Proof state after:
case intro.intro.hF_meas
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fun t => f x t) (volume.restrict (Ι a b))

case intro.intro.h_bound
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (t : ℝ) ∂volume, t ∈ Ι a b → ‖f x t‖ ≤ c

case intro.intro.bound_integrable
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ IntervalIntegrable (fun x => c) volume a b

case intro.intro.h_cont
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
inst✝¹⁰ : SecondCountableTopology E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
X : Type
inst✝⁶ : MeasureSpace X
inst✝⁵ : MetricSpace X
inst✝⁴ : BorelSpace X
Y : Type
inst✝³ : MeasureSpace Y
inst✝² : MetricSpace Y
inst✝¹ : BorelSpace Y
A : Type
inst✝ : TopologicalSpace A
f : X → ℝ → E
s : Set X
a b : ℝ
fc : ContinuousOn (uncurry f) (s ×ˢ Icc a b)
sc : IsCompact s
ab : a ≤ b
c : ℝ
left✝ : 0 ≤ c
fb : ∀ x ∈ s, ∀ y ∈ Icc a b, ‖f x y‖ ≤ c
e : ∀ (x : X) (t : ℝ), f x t = uncurry f (x, t)
x : X
xs : x ∈ s
⊢ ∀ᵐ (t : ℝ) ∂volume, t ∈ Ι a b → ContinuousWithinAt (fun x => f x t) s x