-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem continuous_parametric_integral_of_continuous
    [FirstCountableTopology X] [LocallyCompactSpace X]
    [SecondCountableTopologyEither Y E] [IsLocallyFiniteMeasure μ]
    {f : X → Y → E} (hf : Continuous f.uncurry) {s : Set Y} (hs : IsCompact s) :
    Continuous (∫ y in s, f · y ∂μ)

Proof state:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
⊢ ∀ (x : X), ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x

Tactic:
intro x₀

Result:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
⊢ ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x₀

Proof state:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)
x : X
⊢ Continuous (f x)

Tactic:
fun_prop

Result:
no goals

Proof state:
case intro.intro.intro.bound_integrable
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)
⊢ Integrable (fun t => M) (μ.restrict s)

Tactic:
exact integrableOn_const.mpr (Or.inr hs.measure_lt_top)

Result:
no goals

Proof state:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
⊢ ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x₀

Tactic:
rcases exists_compact_mem_nhds x₀ with ⟨U, U_cpct, U_nhds⟩

Result:
case intro.intro
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
⊢ ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x₀

Proof state:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)
⊢ ∀ (a : Y), ContinuousAt (fun x => f x a) x₀

Tactic:
fun_prop

Result:
no goals

Proof state:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)
x : X
x_in : x ∈ U
⊢ Continuous fun x => M

Tactic:
fun_prop

Result:
no goals

Proof state:
case intro.intro
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
⊢ ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x₀

Tactic:
rcases (U_cpct.prod hs).bddAbove_image hf.norm.continuousOn with ⟨M, hM⟩

Result:
case intro.intro.intro
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)
⊢ ContinuousAt (fun x => ∫ (y : Y) in s, f x y ∂μ) x₀

Proof state:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x => ‖uncurry f x‖) '' U ×ˢ s)
x : X
x_in : x ∈ U
⊢ Continuous fun x_1 => ‖f x x_1‖

Tactic:
fun_prop

Result:
no goals