-- 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
L₁ :
  ‖HSub.hSub (α := E) (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
        (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖ =
    ‖HSub.hSub (α := E) (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
        (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖
L₂ :
  ‖HSub.hSub (α := E) (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
        (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖ =
    norm.{u_3} (E := E)
      (∫ (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) ∂μ)
L₃ :
  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‖ * δ ∂μ)
⊢ ‖HSub.hSub (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) ∂μ)
        (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ)‖ <
    ε

Tactic:
calc
  ‖∫ x, L (g x) (f p x) ∂μ - ∫ x, L (g x) (f q x) ∂μ‖
    = ‖∫ x in k, L (g x) (f p x) ∂μ - ∫ x in k, L (g x) (f q x) ∂μ‖ := by
      congr 2
      · refine (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
        simp [hfs p y h'p hy]
      · refine (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
        simp [hfs q y hq hy]
  _ = ‖∫ x in k, L (g x) (f p x) - L (g x) (f q x) ∂μ‖ := by rw [integral_sub (I p h'p) (I q hq)]
  _ ≤ ∫ x in k, ‖L (g x) (f p x) - L (g x) (f q x)‖ ∂μ := norm_integral_le_integral_norm _
  _ ≤ ∫ x in k, ‖L‖ * ‖g x‖ * δ ∂μ := by
      apply integral_mono_of_nonneg (Eventually.of_forall (fun y ↦ by positivity))
      · exact (hg.norm.const_mul _).mul_const _
      · filter_upwards with y
        by_cases hy : y ∈ k
        · dsimp only
          specialize hv p hp y hy
          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
        · simp only [hfs p y h'p hy, hfs q y hq hy, sub_self, norm_zero]
          positivity
  _ < ε := hδ

Premises used: MeasureTheory.norm_integral_le_integral_norm