awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
⊢ 0 y ≤
    ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
hgi : Integrable (ε := ℝ) (fun (a : Y) ↦ ‖L‖ * ‖g a‖ * δ) (μ.restrict k)
h :
  (ae (μ.restrict k)).EventuallyLE (β := ℝ)
    (fun (a : Y) ↦
      ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f p a) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f q a) : E)‖)
    fun (a : Y) ↦ ‖L‖ * ‖g a‖ * δ
⊢ LE.le (α := ℝ)
    (∫ (x : Y) in k,
      ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) : E)‖ ∂μ)
    (∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ)

Tactic:
apply integral_mono_of_nonneg (Eventually.of_forall (fun y ↦ by positivity))

Premises used: Filter.Eventually.of_forall, MeasureTheory.integral_mono_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ Integrable (ε := ℝ) (fun (a : Y) ↦ ‖L‖ * ‖g a‖ * δ) (μ.restrict k)

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

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ Integrable (ε := ℝ) (fun (a : Y) ↦ ‖L‖ * ‖g a‖ * δ) (μ.restrict k)

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

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
h :
  ∀ (y : Y),
    ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
      ‖L‖ * ‖g y‖ * δ
⊢ (ae (μ.restrict k)).EventuallyLE (β := ℝ)
    (fun (a : Y) ↦
      ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f p a) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f q a) : E)‖)
    fun (a : Y) ↦ ‖L‖ * ‖g a‖ * δ

Tactic:
filter_upwards with y
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
pos :
  ∀ (hy : y ∈ k),
    ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
      ‖L‖ * ‖g y‖ * δ
neg :
  ∀ (hy : y ∉ k),
    ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
      ‖L‖ * ‖g y‖ * δ
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ

Tactic:
by_cases hy : y ∈ k
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∈ k
⊢ ‖f p y - f q y‖ < δ

Tactic:
specialize hv p hp y hy
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∈ k
hv : ‖f p y - f q y‖ < δ
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ =
    norm.{u_3} (E := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y - f q y) : E)

Tactic:
simp only [map_sub]

Premises used: map_sub
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∈ k
hv : ‖f p y - f q y‖ < δ
⊢ norm.{u_3} (E := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y - f q y) : E) ≤
    ‖L‖ * ‖g y‖ * ‖f p y - f q y‖

Tactic:
le_opNorm₂ _ _ _

Premises used: ContinuousLinearMap.le_opNorm₂
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∈ k
hv : ‖f p y - f q y‖ < δ
ha : 0 ≤ ‖L‖ * ‖g y‖
⊢ ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ ≤ ‖L‖ * ‖g y‖ * δ

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∈ k
hv : ‖f p y - f q y‖ < δ
p₁ :
  ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ =
    norm.{u_3} (E := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y - f q y) : E)
p₂ : ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ ≤ ‖L‖ * ‖g y‖ * δ
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ

Tactic:
calc
          ‖L (g y) (f p y) - L (g y) (f q y)‖
            = ‖L (g y) (f p y - f q y)‖ := by simp only [map_sub]
          _ ≤ ‖L‖ * ‖g y‖ * ‖f p y - f q y‖ := le_opNorm₂ _ _ _
          _ ≤ ‖L‖ * ‖g y‖ * δ := by gcongr

Premises used: HSub.hSub, ContinuousLinearMap.le_opNorm₂, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∉ k
neg : 0 ≤ ‖L‖ * ‖g y‖ * δ
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ

Tactic:
simp only [hfs p y h'p hy, hfs q y hq hy, sub_self, norm_zero]

Premises used: sub_self, norm_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
hy : y ∉ k
⊢ 0 ≤ ‖L‖ * ‖g y‖ * δ

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
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_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : 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) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (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.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε

Tactic:
hδ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
f : X → Y → E
s : Set X
k : Set Y
inst_6 : IsFiniteMeasureOnCompacts μ
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
⊢ ContinuousOn.{u_5, u_3} (Y := E) (fun (x : X) ↦ ∫ (y : Y), f x y ∂μ) s

Tactic:
simpa using continuousOn_integral_bilinear_of_locally_integrable_of_compact_support (lsmul ℝ ℝ)
    hk hf hfs (integrableOn_const hk.measure_ne_top) (g := fun _ ↦ 1)

Premises used: Real, MeasureTheory.integrableOn_const, continuousOn_integral_bilinear_of_locally_integrable_of_compact_support, ContinuousLinearMap.lsmul, IsCompact.measure_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ Integrable f (Measure.sum μ)

Tactic:
⟨aestronglyMeasurable_sum_measure_iff.mpr fun i ↦ (hf i).aestronglyMeasurable, ?_⟩

Premises used: Iff.mpr, MeasureTheory.Integrable.aestronglyMeasurable, aestronglyMeasurable_sum_measure_iff, MeasureTheory.Integrable, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
refine : HasFiniteIntegral f (Measure.sum μ)
⊢ Integrable f (Measure.sum μ)

Tactic:
refine ⟨aestronglyMeasurable_sum_measure_iff.mpr fun i ↦ (hf i).aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
rw : LT.lt (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) ∞
⊢ HasFiniteIntegral f (Measure.sum μ)

Tactic:
rw [HasFiniteIntegral, lintegral_sum_measure]

Premises used: MeasureTheory.HasFiniteIntegral, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : Countable ι
mX : MeasurableSpace X
inst_1 : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable (α := ℝ) fun (i : ι) ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ LT.lt (α := ℝ≥0∞) (∑' (i : ι), ENNReal.ofReal (∫ (x : X), ‖f x‖ ∂μ i)) ∞

Tactic:
h.tsum_ofReal_lt_top

Premises used: Summable.tsum_ofReal_lt_top