α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 (g x₀))
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
⊢ Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 (g x₀))
let h := g - fun _ => g x₀
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
⊢ Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 (g x₀))
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A : Tendsto (fun i => (∫ (x : α) in s, φ i x • h x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (0 + 1 • g x₀))
⊢ Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 (g x₀))
simp only [one_smul, zero_add] at A
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
⊢ (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) =ᶠ[l] fun i =>
    ∫ (x : α) in s, φ i x • g x ∂μ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
⊢ Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 (g x₀))
refine' Tendsto.congr' _ A
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
i : ι
hi : IntegrableOn (fun x => φ i x • g x) s
h'i : (∫ (x : α) in s, φ i x ∂μ) = OfNat.ofNat 1 i
⊢ (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀ =
    ∫ (x : α) in s, φ i x • g x ∂μ
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
⊢ (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) =ᶠ[l] fun i =>
    ∫ (x : α) in s, φ i x • g x ∂μ
filter_upwards [integrableOn_peak_smul_of_integrableOn_of_continuousWithinAt hs hlφ hiφ hmg hcg,
  hiφ] with i hi h'i
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
i : ι
hi : IntegrableOn (fun x => φ i x • g x) s
h'i : (∫ (x : α) in s, φ i x ∂μ) = OfNat.ofNat 1 i
⊢ (∫ (x : α) in s, φ i x • g x - φ i x • g x₀ ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀ = ∫ (x : α) in s, φ i x • g x ∂μ
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
i : ι
hi : IntegrableOn (fun x => φ i x • g x) s
h'i : (∫ (x : α) in s, φ i x ∂μ) = OfNat.ofNat 1 i
⊢ (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀ =
    ∫ (x : α) in s, φ i x • g x ∂μ
simp only [Pi.sub_apply, smul_sub]
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
i : ι
hi : IntegrableOn (fun x => φ i x • g x) s
h'i : (∫ (x : α) in s, φ i x ∂μ) = OfNat.ofNat 1 i
⊢ Integrable fun x => φ i x • g x₀
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
i : ι
hi : IntegrableOn (fun x => φ i x • g x) s
h'i : (∫ (x : α) in s, φ i x ∂μ) = OfNat.ofNat 1 i
⊢ (∫ (x : α) in s, φ i x • g x - φ i x • g x₀ ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀ = ∫ (x : α) in s, φ i x • g x ∂μ
rw [integral_sub hi, integral_smul_const, sub_add_cancel]
no goals
case h
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
A :
  Tendsto (fun i => (∫ (x : α) in s, φ i x • (g - fun x => g x₀) x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (g x₀))
i : ι
hi : IntegrableOn (fun x => φ i x • g x) s
h'i : (∫ (x : α) in s, φ i x ∂μ) = OfNat.ofNat 1 i
⊢ Integrable fun x => φ i x • g x₀
exact Integrable.smul_const (integrable_of_integral_eq_one h'i) _
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ) l (𝓝 0)
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ Tendsto (fun i => (∫ (x : α) in s, φ i x • h x ∂μ) + (∫ (x : α) in s, φ i x ∂μ) • g x₀) l (𝓝 (0 + 1 • g x₀))
refine' Tendsto.add _ (Tendsto.smul (tendsto_const_nhds.congr' hiφ.symm) tendsto_const_nhds)
case hmg
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ IntegrableOn (fun x => h x) s

case h'g
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ h x₀ = 0

case hcg
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ ContinuousWithinAt (fun x => h x) s x₀
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ Tendsto (fun i => ∫ (x : α) in s, φ i x • h x ∂μ) l (𝓝 0)
apply tendsto_set_integral_peak_smul_of_integrableOn_of_continuousWithinAt_aux hs hnφ hlφ hiφ
case hmg
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ Integrable fun x => g x₀
case hmg
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ IntegrableOn (fun x => h x) s
apply Integrable.sub hmg
case hmg
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ g x₀ = 0 ∨ ↑↑μ s < ⊤
case hmg
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ Integrable fun x => g x₀
apply integrableOn_const.2
no goals
case hmg
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ g x₀ = 0 ∨ ↑↑μ s < ⊤
simp only [h's.lt_top, or_true_iff]
no goals
case h'g
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ h x₀ = 0
simp only [Pi.sub_apply, sub_self]
no goals
case hcg
α : Type u_1
E : Type u_3
ι : Type u_2
hm : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
inst✝ : CompleteSpace E
hs : MeasurableSet s
h's : ↑↑μ s ≠ ⊤
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), x ∈ s → 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : (fun i => ∫ (x : α) in s, φ i x ∂μ) =ᶠ[l] 1
hmg : IntegrableOn g s
hcg : ContinuousWithinAt g s x₀
h : α → E := g - fun x => g x₀
⊢ ContinuousWithinAt (fun x => h x) s x₀
exact hcg.sub continuousWithinAt_const