-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
/-- Consider a parameterized integral `x ↦ ∫ y, L (g y) (f x y)` where `L` is bilinear,
`g` is locally integrable and `f` is continuous and uniformly compactly supported. Then the
integral depends continuously on `x`. -/
lemma continuousOn_integral_bilinear_of_locally_integrable_of_compact_support
    [NormedSpace 𝕜 E] (L : F →L[𝕜] G →L[𝕜] E)
    {f : X → Y → G} {s : Set X} {k : Set Y} {g : Y → F}
    (hk : IsCompact k) (hf : ContinuousOn f.uncurry (s ×ˢ univ))
    (hfs : ∀ p, ∀ x, p ∈ s → x ∉ k → f p x = 0) (hg : IntegrableOn g k μ) :
    ContinuousOn (fun x ↦ ∫ y, L (g y) (f x y) ∂μ) s

Proof state:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (x : X) in 𝓝[s] q, dist (∫ (y : Y), (L (g y)) (f x y) ∂μ) (∫ (y : Y), (L (g y)) (f q y) ∂μ) < ε

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ (δ : ℝ), 0 < δ ∧ ∫ x in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε := by
  simpa [integral_mul_right] using exists_pos_mul_lt εpos _

Result:
case intro.intro
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
⊢ ∀ᶠ (x : X) in 𝓝[s] q, dist (∫ (y : Y), (L (g y)) (f x y) ∂μ) (∫ (y : Y), (L (g y)) (f q y) ∂μ) < ε

Proof state:
case intro
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
p : X
hp : p ∈ s
this : ContinuousOn (f p) k
C : ℝ
hC : ∀ x ∈ k, ‖f p x‖ ≤ C
⊢ ∃ C, ∀ (y : Y), ‖f p y‖ ≤ C

Tactic:
refine ⟨max C 0, fun y ↦ ?_⟩

Result:
case intro
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
p : X
hp : p ∈ s
this : ContinuousOn (f p) k
C : ℝ
hC : ∀ x ∈ k, ‖f p x‖ ≤ C
y : Y
⊢ ‖f p y‖ ≤ C ⊔ 0

Proof state:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
p : X
hp : p ∈ s
C : ℝ
hC : ∀ (y : Y), ‖f p y‖ ≤ C
this : IntegrableOn (fun y => ‖L‖ * ‖g y‖ * C) k μ
y : Y
⊢ ‖L‖ * ‖g y‖ * ‖f p y‖ ≤ ‖L‖ * ‖g y‖ * C

Tactic:
gcongr

Result:
case h
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
p : X
hp : p ∈ s
C : ℝ
hC : ∀ (y : Y), ‖f p y‖ ≤ C
this : IntegrableOn (fun y => ‖L‖ * ‖g y‖ * C) k μ
y : Y
⊢ ‖f p y‖ ≤ C

Proof state:
case hgi
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ
I : ∀ p ∈ s, IntegrableOn (fun y => (L (g y)) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ Integrable (fun a => ‖L‖ * ‖g a‖ * δ) (μ.restrict k)

Tactic:
exact (hg.norm.const_mul _).mul_const _

Result:
no goals